AbstractHeisenberg.lean

1 import PaperXI.CentralExtension
2 import Mathlib.LinearAlgebra.BilinearForm.Properties
3 import Mathlib.RingTheory.Finiteness.Cardinality
4 import Mathlib.Algebra.Group.TypeTags.Basic
5 import Mathlib.Tactic
6 
7 /-! Actual Heisenberg groups on abstract bilinear spaces, their central extensions,
8 and center-preserving lifts of arbitrary form-preserving linear equivalences.
9 No choice of symplectic coordinates is used. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.AbstractHeisenberg
13 
14 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
15 
16 /-- The actual group space attached to a bilinear form. -/
17 @[ext]
18 structure Element (b : LinearMap.BilinForm K V) where
19   vector : V
20   central : K
21 
22 variable (b : LinearMap.BilinForm K V)
23 
24 instance instMul : Mul (Element b) where
25   mul h k := ⟨h.vector + k.vector,
26     h.central + k.central + (2 : K)⁻¹ * b h.vector k.vector⟩
27 
28 instance instOne : One (Element b) where
29   one := ⟨0, 0⟩
30 
31 /-- The correction allows the group construction for every bilinear form.
32 For an alternating form the correction vanishes. -/
33 instance instInv : Inv (Element b) where
34   inv h := ⟨-h.vector, -h.central + (2 : K)⁻¹ * b h.vector h.vector⟩
35 
36 @[simp] theorem mul_vector (h k : Element b) : (h * k).vector = h.vector + k.vector := rfl
37 @[simp] theorem mul_central (h k : Element b) :
38     (h * k).central = h.central + k.central + (2 : K)⁻¹ * b h.vector k.vector := rfl
39 @[simp] theorem one_vector : (1 : Element b).vector = 0 := rfl
40 @[simp] theorem one_central : (1 : Element b).central = 0 := rfl
41 @[simp] theorem inv_vector (h : Element b) : h⁻¹.vector = -h.vector := rfl
42 @[simp] theorem inv_central (h : Element b) :
43     h⁻¹.central = -h.central + (2 : K)⁻¹ * b h.vector h.vector := rfl
44 
45 instance instGroup : Group (Element b) where
46   mul_assoc h k l := by
47     ext <;> simp [map_add, add_assoc]
48     ring
49   one_mul h := by ext <;> simp
50   mul_one h := by ext <;> simp
51   inv_mul_cancel h := by
52     ext <;> simp
53 
54 /-- The group is literally a copy of the abstract vector space times the center. -/
55 def coordinates : Element b ≃ V × K where
56   toFun h := (h.vector, h.central)
57   invFun h := ⟨h.1, h.2⟩
58   left_inv h := by cases h; rfl
59   right_inv h := by cases h; rfl
60 
61 instance instFinite [Finite V] [Finite K] : Finite (Element b) :=
62   Finite.of_injective (coordinates b) (coordinates b).injective
63 
64 /-- Over a finite field, a finite-dimensional abstract space gives a finite actual group. -/
65 theorem finite_of_finite_field [Finite K] [FiniteDimensional K V] : Finite (Element b) := by
66   let : Finite V := Module.finite_of_finite K
67   infer_instance
68 
69 /-- The distinguished central element with scalar coordinate `z`. -/
70 def centralElement (z : K) : Element b := ⟨0, z⟩
71 
72 @[simp] theorem centralElement_vector (z : K) : (centralElement b z).vector = 0 := rfl
73 @[simp] theorem centralElement_central (z : K) : (centralElement b z).central = z := rfl
74 @[simp] theorem centralElement_zero : centralElement b 0 = 1 := rfl
75 @[simp] theorem centralElement_mul (z t : K) :
76     centralElement b z * centralElement b t = centralElement b (z + t) := by
77   ext <;> simp
78 
79 theorem centralElement_commute (z : K) (h : Element b) :
80     centralElement b z * h = h * centralElement b z := by
81   ext <;> simp [add_comm]
82 
83 /-- The actual central inclusion, using multiplicative notation for the additive field. -/
84 def inclusion : Multiplicative K →* Element b where
85   toFun z := centralElement b z.toAdd
86   map_one' := rfl
87   map_mul' z t := (centralElement_mul b z.toAdd t.toAdd).symm
88 
89 /-- The actual quotient homomorphism onto the additive abstract vector space. -/
90 def quotient : Element b →* Multiplicative V where
91   toFun h := Multiplicative.ofAdd h.vector
92   map_one' := rfl
93   map_mul' _ _ := rfl
94 
95 @[simp] theorem inclusion_apply (z : Multiplicative K) :
96     inclusion b z = centralElement b z.toAdd := rfl
97 @[simp] theorem quotient_apply (h : Element b) :
98     quotient b h = Multiplicative.ofAdd h.vector := rfl
99 
100 /-- The abstract group gives an actual central extension with all exactness proofs. -/
101 def datum : CentralExtension.Datum (Multiplicative K) (Element b) (Multiplicative V) where
102   i := inclusion b
103   q := quotient b
104   i_injective := by
105     intro z t h
106     exact congrArg (fun h : Element b => Multiplicative.ofAdd h.central) h
107   q_surjective a := ⟨⟨a.toAdd, 0⟩, rfl⟩
108   range_i_eq_ker_q := by
109     ext h
110     constructor
111     · rintro ⟨z, rfl⟩
112       rfl
113     · intro hh
114       change h.vector = 0 at hh
115       refine ⟨Multiplicative.ofAdd h.central, ?_⟩
116       ext
117       · exact hh.symm
118       · rfl
119   central z h := centralElement_commute b z.toAdd h
120 
121 @[simp] theorem datum_i (z : Multiplicative K) : (datum b).i z = centralElement b z.toAdd := rfl
122 @[simp] theorem datum_q (h : Element b) : (datum b).q h = Multiplicative.ofAdd h.vector := rfl
123 
124 /-- For an alternating form the inverse has the expected negated coordinates. -/
125 theorem inv_central_of_isAlt (hb : b.IsAlt) (h : Element b) :
126     h⁻¹.central = -h.central := by simp [hb h.vector]
127 
128 /-- The actual group commutation law has the bilinear scalar in odd characteristic. -/
129 theorem mul_swap (hb : b.IsAlt) (h2 : (2 : K) ≠ 0) (h k : Element b) :
130     h * k = centralElement b (b h.vector k.vector) * (k * h) := by
131   ext
132   · simp [add_comm]
133   · simp only [mul_central, centralElement_central, centralElement_vector, map_zero,
134       LinearMap.zero_apply, mul_zero, add_zero]
135     rw [← hb.neg_eq h.vector k.vector]
136     field_simp
137     ring
138 
139 /-- The commutator is proved on actual abstract group elements, without a coordinate model. -/
140 theorem commutator (hb : b.IsAlt) (h2 : (2 : K) ≠ 0) (h k : Element b) :
141     h * k * h⁻¹ * k⁻¹ = centralElement b (b h.vector k.vector) := by
142   rw [mul_swap b hb h2 h k]
143   group
144 
145 section Lift
146 
147 variable {V' : Type*} [AddCommGroup V'] [Module K V']
148 variable (b' : LinearMap.BilinForm K V')
149 
150 /-- A form-preserving map of arbitrary abstract spaces lifts by its literal action on vectors. -/
151 def lift (e : V ≃ₗ[K] V') (he : ∀ v w, b' (e v) (e w) = b v w) :
152     Element b ≃* Element b' where
153   toFun h := ⟨e h.vector, h.central⟩
154   invFun h := ⟨e.symm h.vector, h.central⟩
155   left_inv h := by ext <;> simp
156   right_inv h := by ext <;> simp
157   map_mul' h k := by
158     ext
159     · exact e.map_add h.vector k.vector
160     · simp only [mul_central]
161       rw [he]
162 
163 @[simp] theorem lift_vector (e : V ≃ₗ[K] V')
164     (he : ∀ v w, b' (e v) (e w) = b v w) (h : Element b) :
165     (lift b b' e he h).vector = e h.vector := rfl
166 
167 @[simp] theorem lift_central (e : V ≃ₗ[K] V')
168     (he : ∀ v w, b' (e v) (e w) = b v w) (h : Element b) :
169     (lift b b' e he h).central = h.central := rfl
170 
171 @[simp] theorem lift_inclusion (e : V ≃ₗ[K] V')
172     (he : ∀ v w, b' (e v) (e w) = b v w) (z : Multiplicative K) :
173     lift b b' e he ((datum b).i z) = (datum b').i z := by
174   ext <;> simp [lift]
175 
176 /-- The lift induces the supplied abstract linear equivalence on the actual quotients. -/
177 theorem lift_quotient (e : V ≃ₗ[K] V')
178     (he : ∀ v w, b' (e v) (e w) = b v w) (h : Element b) :
179     (datum b').q (lift b b' e he h) =
180       Multiplicative.ofAdd (e ((datum b).q h).toAdd) := rfl
181 
182 end Lift
183 
184 end PaperXI.AbstractHeisenberg

Back to source controls