DyadicExtensionClass.lean

1 import PaperXI.DyadicHeisenbergLift
2 import Mathlib.LinearAlgebra.Basis.Defs
3 
4 /-! A prescribed square profile determines the bilinear F2-extension up to an
5 actual center- and quotient-preserving isomorphism. We construct the coboundary
6 with the upper-triangular part in an ordinary basis. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.DyadicExtensionClass
10 open BilinearHeisenberg
11 variable {V : Type*} [AddCommGroup V] [Module (ZMod 2) V]
12 
13 /-- Upper-triangular half of an alternating F2-bilinear form in a chosen basis. -/
14 def upper {n : ℕ} (e : Module.Basis (Fin n) (ZMod 2) V)
15     (d : LinearMap.BilinForm (ZMod 2) V) : LinearMap.BilinForm (ZMod 2) V :=
16   e.constr (ZMod 2) (fun i => e.constr (ZMod 2) (fun j => if i < j then d (e i) (e j) else 0))
17 
18 @[simp] theorem upper_basis {n : ℕ} (e : Module.Basis (Fin n) (ZMod 2) V)
19     (d : LinearMap.BilinForm (ZMod 2) V) (i j : Fin n) :
20     upper e d (e i) (e j) = if i < j then d (e i) (e j) else 0 := by
21   simp only [upper, Module.Basis.constr_basis]
22 
23 /-- The triangular construction recovers the entire alternating form. -/
24 theorem upper_symmetrization {n : ℕ} (e : Module.Basis (Fin n) (ZMod 2) V)
25     (d : LinearMap.BilinForm (ZMod 2) V) (ha : d.IsAlt) :
26     upper e d + (upper e d).flip = d := by
27   apply e.ext
28   intro i
29   apply e.ext
30   intro j
31   change upper e d (e i) (e j) + upper e d (e j) (e i) = d (e i) (e j)
32   rw [upper_basis, upper_basis]
33   rcases lt_trichotomy i j with h | h | h
34   · rw [ite_eq_left h, ite_eq_right (not_lt_of_ge (le_of_lt h)), add_zero]
35   · subst j
36     simp only [lt_irrefl, ite_false, zero_add]
37     exact (ha (e i)).symm
38   · rw [ite_eq_right (not_lt_of_ge (le_of_lt h)), ite_eq_left h, zero_add]
39     exact SymplecticSplit.alternating_symmetric d ha (e j) (e i)
40 
41 variable [FiniteDimensional (ZMod 2) V]
42 
43 /-- Every alternating bilinear form, even degenerate, is a normalized
44 quadratic coboundary. This is constructed rather than supplied as extension data. -/
45 theorem exists_coboundary (d : LinearMap.BilinForm (ZMod 2) V) (ha : d.IsAlt) :
46     ∃ f : V → ZMod 2, f 0 = 0 ∧
47       ∀ x y, d x y = f (x + y) - f x - f y := by
48   let e := Module.finBasis (ZMod 2) V
49   let u := upper e d
50   have hu : u + u.flip = d := upper_symmetrization e d ha
51   refine ⟨fun x => u x x, by simp, ?_⟩
52   intro x y
53   have hxy := LinearMap.congr_fun (LinearMap.congr_fun hu x) y
54   change u x y + u y x = d x y at hxy
55   simp only [map_add, LinearMap.add_apply]
56   linear_combination -hxy
57 
58 /-- Matching diagonal factor sets give a genuine isomorphism over both the
59 central group and the quotient, without an isomorphism/coboundary hypothesis. -/
60 theorem exists_equiv_of_diagonal (c d : LinearMap.BilinForm (ZMod 2) V)
61     (hd : ∀ v, c v v = d v v) :
62     ∃ e : Element c ≃* Element d,
63       (∀ z, e (i c z) = i d z) ∧ (∀ h, (e h).vector = h.vector) := by
64   have ha : (d - c).IsAlt := by
65     intro v
66     change d v v - c v v = 0
67     rw [hd, sub_self]
68   obtain ⟨f, h0, hf⟩ := exists_coboundary (d - c) ha
69   exact ⟨HeisenbergCochain.equiv c d f h0 hf,
70     HeisenbergCochain.equiv_center c d f h0 hf,
71     HeisenbergCochain.equiv_vector c d f h0 hf⟩
72 
73 /-- Complete equivalence criterion for these actual bilinear F2-extensions. -/
74 theorem exists_equiv_iff_diagonal (c d : LinearMap.BilinForm (ZMod 2) V) :
75     (∃ e : Element c ≃* Element d,
76       (∀ z, e (i c z) = i d z) ∧ (∀ h, (e h).vector = h.vector)) ↔
77       ∀ v, c v v = d v v := by
78   constructor
79   · rintro ⟨e, he, hq⟩ v
80     exact HeisenbergCochain.diagonal_preserved c d e he hq v
81   · exact exists_equiv_of_diagonal c d
82 
83 /-- Different coordinate constructions for the same declared refinement give
84 isomorphic middle groups. No arbitrary form-preserving map is assumed to lift. -/
85 theorem refinement_model_independent
86     (b : LinearMap.BilinForm (ZMod 2) V) (Q : DyadicAffine.Refinement b)
87     (c d : LinearMap.BilinForm (ZMod 2) V)
88     (hc : ∀ v, c v v = Q.value v) (hd : ∀ v, d v v = Q.value v) :
89     ∃ e : Element c ≃* Element d,
90       (∀ z, e (i c z) = i d z) ∧ (∀ h, (e h).vector = h.vector) :=
91   exists_equiv_of_diagonal c d (fun v => (hc v).trans (hd v).symm)
92 
93 end PaperXI.DyadicExtensionClass

Back to source controls