DyadicHeisenbergLift.lean

1 import PaperXI.HeisenbergCochain
2 import PaperXI.SymplecticCoordinates
3 
4 /-! A given quadratic refinement on an intrinsic finite F2-space supplies an
5 actual bilinear factor set, hence a finite Heisenberg extension. Coordinates are
6 constructed from the form; its square profile is the given refinement, not erased. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.DyadicHeisenbergLift
10 open scoped BigOperators Classical
11 open PaperXI.Dyadic PaperXI.DyadicAffine PaperXI.DyadicCoordinates PaperXI.BilinearHeisenberg
12 variable {ι : Type*} [Fintype ι]
13 
14 /-- The standard factor set with declared squares on both axes of every plane. -/
15 def coordinateFactor (a : ι → F2 × F2) :
16     LinearMap.BilinForm F2 (ι → F2 × F2) where
17   toFun x :=
18     { toFun := fun y => ∑ i, ((x i).1 * (y i).2 +
19         (a i).1 * (x i).1 * (y i).1 + (a i).2 * (x i).2 * (y i).2)
20       map_add' := by
21         intro y z
22         simp only [Pi.add_apply, Prod.fst_add, Prod.snd_add]
23         rw [← Finset.sum_add_distrib]
24         apply Finset.sum_congr rfl
25         intro i hi
26         ring
27       map_smul' := by
28         intro r y
29         change (∑ i, ((x i).1 * (r * (y i).2) +
30           (a i).1 * (x i).1 * (r * (y i).1) + (a i).2 * (x i).2 * (r * (y i).2))) =
31           r * (∑ i, ((x i).1 * (y i).2 +
32           (a i).1 * (x i).1 * (y i).1 + (a i).2 * (x i).2 * (y i).2))
33         rw [Finset.mul_sum]
34         apply Finset.sum_congr rfl
35         intro i hi
36         ring }
37   map_add' := by
38     intro x z
39     apply LinearMap.ext
40     intro y
41     change (∑ i, (((x + z) i).1 * (y i).2 +
42       (a i).1 * ((x + z) i).1 * (y i).1 + (a i).2 * ((x + z) i).2 * (y i).2)) =
43       (∑ i, ((x i).1 * (y i).2 + (a i).1 * (x i).1 * (y i).1 +
44       (a i).2 * (x i).2 * (y i).2)) +
45       (∑ i, ((z i).1 * (y i).2 + (a i).1 * (z i).1 * (y i).1 +
46       (a i).2 * (z i).2 * (y i).2))
47     rw [← Finset.sum_add_distrib]
48     apply Finset.sum_congr rfl
49     intro i hi
50     simp only [Pi.add_apply, Prod.fst_add, Prod.snd_add]
51     ring
52   map_smul' := by
53     intro r x
54     apply LinearMap.ext
55     intro y
56     change (∑ i, ((r * (x i).1) * (y i).2 +
57       (a i).1 * (r * (x i).1) * (y i).1 + (a i).2 * (r * (x i).2) * (y i).2)) =
58       r * (∑ i, ((x i).1 * (y i).2 + (a i).1 * (x i).1 * (y i).1 +
59       (a i).2 * (x i).2 * (y i).2))
60     rw [Finset.mul_sum]
61     apply Finset.sum_congr rfl
62     intro i hi
63     ring
64 
65 @[simp] theorem coordinateFactor_apply (a x y : ι → F2 × F2) :
66     coordinateFactor a x y = ∑ i, ((x i).1 * (y i).2 +
67       (a i).1 * (x i).1 * (y i).1 + (a i).2 * (x i).2 * (y i).2) := rfl
68 
69 theorem coordinateFactor_commutator (a x y : ι → F2 × F2) :
70     coordinateFactor a x y - coordinateFactor a y x = symplectic x y := by
71   simp only [coordinateFactor_apply, symplectic_apply, ← Finset.sum_sub_distrib]
72   apply Finset.sum_congr rfl
73   intro i hi
74   rw [sub_eq_add_neg, CharTwo.neg_eq]
75   ring_nf
76   simp only [show (2 : F2) = 0 from rfl, mul_zero, add_zero]
77 
78 theorem coordinateFactor_diagonal (a x : ι → F2 × F2) :
79     coordinateFactor a x x = quadratic a x := by
80   simp only [coordinateFactor_apply, quadratic, plane]
81   apply Finset.sum_congr rfl
82   intro i hi
83   have hs (t : F2) : t * t = t := by fin_cases t <;> rfl
84   have hx := hs (x i).1
85   have hy := hs (x i).2
86   simp only [mul_assoc, hx, hy]
87 
88 variable {V : Type*} [AddCommGroup V] [Module F2 V]
89 
90 /-- Transport the actual quadratic refinement into the constructed coordinates. -/
91 def coordinateRefinementOf (b : LinearMap.BilinForm F2 V) (Q : Refinement b)
92     (e : V ≃ₗ[F2] (ι → F2 × F2))
93     (he : ∀ x y, b x y = symplectic (e x) (e y)) : Refinement (symplectic (ι := ι)) where
94   value x := Q.value (e.symm x)
95   polar x y := by
96     rw [map_add, Q.polar, he]
97     simp
98 
99 /-- Pull back the explicit factor set; no central extension is an input. -/
100 def factorOfCoordinates (b : LinearMap.BilinForm F2 V) (Q : Refinement b)
101     (e : V ≃ₗ[F2] (ι → F2 × F2))
102     (he : ∀ x y, b x y = symplectic (e x) (e y)) : LinearMap.BilinForm F2 V :=
103   (coordinateFactor (refinementCoefficients (coordinateRefinementOf b Q e he))).compl₁₂
104     e.toLinearMap e.toLinearMap
105 
106 theorem factorOfCoordinates_commutator (b : LinearMap.BilinForm F2 V) (Q : Refinement b)
107     (e : V ≃ₗ[F2] (ι → F2 × F2))
108     (he : ∀ x y, b x y = symplectic (e x) (e y)) (x y : V) :
109     factorOfCoordinates b Q e he x y - factorOfCoordinates b Q e he y x = b x y := by
110   change coordinateFactor _ (e x) (e y) - coordinateFactor _ (e y) (e x) = b x y
111   rw [coordinateFactor_commutator, ← he]
112 
113 theorem factorOfCoordinates_diagonal (b : LinearMap.BilinForm F2 V) (Q : Refinement b)
114     (e : V ≃ₗ[F2] (ι → F2 × F2))
115     (he : ∀ x y, b x y = symplectic (e x) (e y)) (x : V) :
116     factorOfCoordinates b Q e he x x = Q.value x := by
117   change coordinateFactor _ (e x) (e x) = Q.value x
118   rw [coordinateFactor_diagonal, ← refinement_coordinate_formula]
119   simp [coordinateRefinementOf]
120 
121 variable [FiniteDimensional F2 V]
122 
123 /-- Every refinement of a finite nondegenerate alternating F2-form has an actual
124 bilinear lift, including the supplied square data. A basis is constructed, not assumed. -/
125 theorem exists_factor (b : LinearMap.BilinForm F2 V) (ha : b.IsAlt)
126     (hb : b.SeparatingLeft) (Q : Refinement b) :
127     ∃ c : LinearMap.BilinForm F2 V,
128       (∀ x y, c x y - c y x = b x y) ∧ (∀ x, c x x = Q.value x) := by
129   obtain ⟨r, e, he⟩ := SymplecticCoordinates.exists_coordinates b ha hb
130   exact ⟨factorOfCoordinates b Q e he,
131     factorOfCoordinates_commutator b Q e he, factorOfCoordinates_diagonal b Q e he⟩
132 
133 /-- A deterministic-in-the-foundations choice of bilinear lift. It is not a
134 claim of canonical functoriality or a normalized symplectic-group action. -/
135 def factor (b : LinearMap.BilinForm F2 V) (ha : b.IsAlt)
136     (hb : b.SeparatingLeft) (Q : Refinement b) : LinearMap.BilinForm F2 V :=
137   Classical.choose (exists_factor b ha hb Q)
138 
139 theorem factor_commutator (b : LinearMap.BilinForm F2 V) (ha : b.IsAlt)
140     (hb : b.SeparatingLeft) (Q : Refinement b) (x y : V) :
141     factor b ha hb Q x y - factor b ha hb Q y x = b x y :=
142   (Classical.choose_spec (exists_factor b ha hb Q)).1 x y
143 
144 theorem factor_diagonal (b : LinearMap.BilinForm F2 V) (ha : b.IsAlt)
145     (hb : b.SeparatingLeft) (Q : Refinement b) (x : V) :
146     factor b ha hb Q x x = Q.value x :=
147   (Classical.choose_spec (exists_factor b ha hb Q)).2 x
148 
149 /-- The actual group constructed from Q has exactly Q as its lift-square map. -/
150 theorem square_profile (b : LinearMap.BilinForm F2 V) (ha : b.IsAlt)
151     (hb : b.SeparatingLeft) (Q : Refinement b) (h : Element (factor b ha hb Q)) :
152     h * h = i (factor b ha hb Q) (Multiplicative.ofAdd (Q.value h.vector)) := by
153   rw [HeisenbergCochain.square, factor_diagonal]
154 
155 end PaperXI.DyadicHeisenbergLift

Back to source controls