CentralExtensionSectionChange.lean

1 import PaperXI.CentralExtensionCocycle
2 import PaperXI.TwistedRescaling
3 import PaperXI.CentralCharacterAction
4 
5 /-! Independence of normalized quotient section for the actual cocycle and
6 twisted algebra of a central extension. The alternate defect is computed
7 in the middle group, then identified with the derived coboundary. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.CentralExtension
11 
12 open CocycleCommutator
13 variable {Z H A : Type*} [CommGroup Z] [Group H] [CommGroup A]
14 variable (D : Datum Z H A)
15 
16 omit [CommGroup Z] [Group H] in
17 /-- Cocycles with the same actual coefficients are equal. -/
18 theorem cocycle_eq_of_coeff_eq {C : Type*} [CommGroup C]
19     (c d : Cocycle A C) (h : ∀ a b, c.coeff a b = d.coeff a b) : c = d := by
20   cases c
21   cases d
22   congr
23   funext a b
24   exact h a b
25 
26 /-- The central factor relating an arbitrary section to the chosen section. -/
27 def sectionFactor (t : A → H) (a : A) : Z := coordinate D (t a)
28 
29 theorem section_factor (t : A → H) (ht : ∀ a, D.q (t a) = a) (a : A) :
30     t a = D.i (sectionFactor D t a) * sectionMap D a := by
31   simpa only [sectionFactor, ht] using normal_form D (t a)
32 
33 @[simp] theorem sectionFactor_one (t : A → H) (htOne : t 1 = 1) :
34     sectionFactor D t 1 = 1 := by
35   simp [sectionFactor, htOne]
36 
37 /-- The actual central coordinate of the alternate section's defect. -/
38 def sectionDefect (t : A → H) (a b : A) : Z :=
39   coordinate D (t a * t b * (t (a * b))⁻¹)
40 
41 theorem i_sectionDefect (t : A → H) (ht : ∀ a, D.q (t a) = a) (a b : A) :
42     D.i (sectionDefect D t a b) = t a * t b * (t (a * b))⁻¹ := by
43   simp only [sectionDefect, coordinate_spec, map_mul, map_inv, ht,
44     mul_inv_cancel, section_one, inv_one, mul_one]
45 
46 theorem sectionDefect_mul (t : A → H) (ht : ∀ a, D.q (t a) = a) (a b : A) :
47     t a * t b = D.i (sectionDefect D t a b) * t (a * b) := by
48   rw [i_sectionDefect D t ht, inv_mul_cancel_right]
49 
50 /-- The coboundary formula follows from the two actual section products. -/
51 theorem sectionDefect_eq_rescale (t : A → H) (ht : ∀ a, D.q (t a) = a)
52     (a b : A) :
53     sectionDefect D t a b =
54       (rescale (centralCocycle D) (sectionFactor D t)).coeff a b := by
55   apply D.i_injective
56   apply mul_right_cancel (b := t (a * b))
57   rw [← sectionDefect_mul D t ht]
58   calc
59     t a * t b = D.i (sectionFactor D t a * sectionFactor D t b * defect D a b) *
60         sectionMap D (a * b) := by
61       rw [section_factor D t ht a, section_factor D t ht b, normal_form_mul]
62     _ = D.i (((rescale (centralCocycle D) (sectionFactor D t)).coeff a b) *
63         sectionFactor D t (a * b)) * sectionMap D (a * b) := by
64       congr 2
65       simp [rescale, centralCocycle, div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm]
66     _ = _ := by
67       rw [map_mul, mul_assoc, ← section_factor D t ht (a * b)]
68 
69 /-- The alternate cocycle is built from its actual middle-group defect. -/
70 def sectionCocycle (t : A → H) (ht : ∀ a, D.q (t a) = a) : Cocycle A Z where
71   coeff := sectionDefect D t
72   assoc a b d := by
73     simp only [sectionDefect_eq_rescale D t ht]
74     exact (rescale (centralCocycle D) (sectionFactor D t)).assoc a b d
75 
76 theorem sectionCocycle_eq_rescale (t : A → H) (ht : ∀ a, D.q (t a) = a) :
77     sectionCocycle D t ht = rescale (centralCocycle D) (sectionFactor D t) := by
78   apply cocycle_eq_of_coeff_eq
79   exact sectionDefect_eq_rescale D t ht
80 
81 theorem normalized_sectionCocycle (t : A → H) (ht : ∀ a, D.q (t a) = a)
82     (htOne : t 1 = 1) : Normalized (sectionCocycle D t ht) := by
83   rw [sectionCocycle_eq_rescale]
84   exact normalized_rescale _ (normalized_centralCocycle D) _ (sectionFactor_one D t htOne)
85 
86 /-- The scalar cocycle of an arbitrary section applies the fixed central
87 character to that section's actual defect. -/
88 def sectionScalarCocycle (ζ : Z →* ℂˣ) (t : A → H) (ht : ∀ a, D.q (t a) = a) :
89     Cocycle A ℂˣ where
90   coeff a b := ζ (sectionDefect D t a b)
91   assoc a b d := by
92     simpa only [sectionCocycle, map_mul] using congrArg ζ ((sectionCocycle D t ht).assoc a b d)
93 
94 theorem sectionScalarCocycle_eq_rescale (ζ : Z →* ℂˣ) (t : A → H)
95     (ht : ∀ a, D.q (t a) = a) :
96     sectionScalarCocycle D ζ t ht =
97       rescale (scalarCocycle D ζ) (fun a => ζ (sectionFactor D t a)) := by
98   have hcoeff : ∀ a b, ζ (sectionDefect D t a b) =
99       (rescale (scalarCocycle D ζ) (fun a => ζ (sectionFactor D t a))).coeff a b := by
100     intro a b
101     rw [sectionDefect_eq_rescale D t ht]
102     simp only [rescale, centralCocycle, scalarCocycle_coeff, map_mul, map_div]
103   apply cocycle_eq_of_coeff_eq
104   exact hcoeff
105 
106 theorem normalized_sectionScalarCocycle (ζ : Z →* ℂˣ) (t : A → H)
107     (ht : ∀ a, D.q (t a) = a) (htOne : t 1 = 1) :
108     Normalized (sectionScalarCocycle D ζ t ht) := by
109   rw [sectionScalarCocycle_eq_rescale]
110   apply normalized_rescale _ (normalized_scalarCocycle D ζ)
111   simp [htOne]
112 
113 /-- Every normalized section has the same scalar commutator pairing. -/
114 theorem sectionScalarCocycle_commutator (ζ : Z →* ℂˣ) (t : A → H)
115     (ht : ∀ a, D.q (t a) = a) (a b : A) :
116     commutator (sectionScalarCocycle D ζ t ht) a b =
117       commutator (scalarCocycle D ζ) a b := by
118   rw [sectionScalarCocycle_eq_rescale, commutator_rescale]
119 
120 /-- In particular, the nondegeneracy condition does not depend on section. -/
121 theorem sectionScalarCocycle_radical (ζ : Z →* ℂˣ) (t : A → H)
122     (ht : ∀ a, D.q (t a) = a) :
123     radical (sectionScalarCocycle D ζ t ht) = radical (scalarCocycle D ζ) := by
124   rw [sectionScalarCocycle_eq_rescale, radical_rescale]
125 
126 variable [Fintype A]
127 
128 /-- The actual algebra equivalence from an arbitrary normalized section to
129 the chosen section, constructed through the proved coboundary identity. -/
130 def sectionAlgebraEquiv (ζ : Z →* ℂˣ) (t : A → H)
131     (ht : ∀ a, D.q (t a) = a) (htOne : t 1 = 1) :
132     TwistedAlgebra.Algebra (sectionScalarCocycle D ζ t ht)
133       (normalized_sectionScalarCocycle D ζ t ht htOne) ≃ₐ[ℂ]
134         TwistedAlgebra.Algebra (scalarCocycle D ζ) (normalized_scalarCocycle D ζ) :=
135   (TwistedRescaling.congrEquiv _ _ (normalized_sectionScalarCocycle D ζ t ht htOne)
136     (normalized_rescale _ (normalized_scalarCocycle D ζ)
137       (fun a => ζ (sectionFactor D t a)) (by simp [htOne]))
138     (sectionScalarCocycle_eq_rescale D ζ t ht)).trans
139       (TwistedRescaling.rescaleEquiv (scalarCocycle D ζ) (normalized_scalarCocycle D ζ)
140         (fun a => ζ (sectionFactor D t a)) (by simp [htOne]))
141 
142 @[simp] theorem sectionAlgebraEquiv_basis (ζ : Z →* ℂˣ) (t : A → H)
143     (ht : ∀ a, D.q (t a) = a) (htOne : t 1 = 1) (a : A) :
144     sectionAlgebraEquiv D ζ t ht htOne
145       (TwistedAlgebra.basis (sectionScalarCocycle D ζ t ht)
146         (normalized_sectionScalarCocycle D ζ t ht htOne) a) =
147       (ζ (sectionFactor D t a) : ℂ) •
148         TwistedAlgebra.basis (scalarCocycle D ζ) (normalized_scalarCocycle D ζ) a := by
149   simp only [sectionAlgebraEquiv, AlgEquiv.trans_apply,
150     TwistedRescaling.congrEquiv_basis, TwistedRescaling.rescaleEquiv_basis]
151 
152 @[simp] theorem sectionAlgebraEquiv_symm_basis (ζ : Z →* ℂˣ) (t : A → H)
153     (ht : ∀ a, D.q (t a) = a) (htOne : t 1 = 1) (a : A) :
154     (sectionAlgebraEquiv D ζ t ht htOne).symm
155       (TwistedAlgebra.basis (scalarCocycle D ζ) (normalized_scalarCocycle D ζ) a) =
156       ((ζ (sectionFactor D t a))⁻¹ : ℂˣ) •
157         TwistedAlgebra.basis (sectionScalarCocycle D ζ t ht)
158           (normalized_sectionScalarCocycle D ζ t ht htOne) a := by
159   apply (sectionAlgebraEquiv D ζ t ht htOne).injective
160   simp only [AlgEquiv.apply_symm_apply, Units.smul_def, map_smul,
161     sectionAlgebraEquiv_basis, smul_smul]
162   simp
163 
164 /-- Any two normalized sections give explicitly equivalent actual algebras. -/
165 def betweenSectionsEquiv (ζ : Z →* ℂˣ) (t u : A → H)
166     (ht : ∀ a, D.q (t a) = a) (hu : ∀ a, D.q (u a) = a)
167     (htOne : t 1 = 1) (huOne : u 1 = 1) :
168     TwistedAlgebra.Algebra (sectionScalarCocycle D ζ u hu)
169       (normalized_sectionScalarCocycle D ζ u hu huOne) ≃ₐ[ℂ]
170         TwistedAlgebra.Algebra (sectionScalarCocycle D ζ t ht)
171           (normalized_sectionScalarCocycle D ζ t ht htOne) :=
172   (sectionAlgebraEquiv D ζ u hu huOne).trans (sectionAlgebraEquiv D ζ t ht htOne).symm
173 
174 @[simp] theorem betweenSectionsEquiv_basis (ζ : Z →* ℂˣ) (t u : A → H)
175     (ht : ∀ a, D.q (t a) = a) (hu : ∀ a, D.q (u a) = a)
176     (htOne : t 1 = 1) (huOne : u 1 = 1) (a : A) :
177     betweenSectionsEquiv D ζ t u ht hu htOne huOne
178       (TwistedAlgebra.basis (sectionScalarCocycle D ζ u hu)
179         (normalized_sectionScalarCocycle D ζ u hu huOne) a) =
180       ((ζ (sectionFactor D u a) / ζ (sectionFactor D t a) : ℂˣ) : ℂ) •
181         TwistedAlgebra.basis (sectionScalarCocycle D ζ t ht)
182           (normalized_sectionScalarCocycle D ζ t ht htOne) a := by
183   simp only [betweenSectionsEquiv, AlgEquiv.trans_apply, sectionAlgebraEquiv_basis,
184     map_smul, sectionAlgebraEquiv_symm_basis, Units.smul_def, smul_smul,
185     div_eq_mul_inv, Units.val_mul]
186 
187 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
188 
189 omit [Fintype A] in
190 /-- The section change rescales the actual representation operators. -/
191 theorem sectionOperators_factor (ζ : Z →* ℂˣ) (t : A → H)
192     (ht : ∀ a, D.q (t a) = a) (σ : Representation ℂ H V)
193     (hcentral : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) (a : A) :
194     σ (t a) = (ζ (sectionFactor D t a) : ℂ) • σ (sectionMap D a) := by
195   rw [section_factor D t ht a, map_mul, hcentral]
196   change ((ζ (sectionFactor D t a) : ℂ) • (1 : Module.End ℂ V)) *
197     σ (sectionMap D a) = _
198   rw [smul_mul_assoc, one_mul]
199 
200 omit [Fintype A] in
201 /-- The alternate section operators have their actual alternate cocycle. -/
202 theorem sectionOperators_mul (ζ : Z →* ℂˣ) (t : A → H)
203     (ht : ∀ a, D.q (t a) = a) (σ : Representation ℂ H V)
204     (hcentral : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) (a b : A) :
205     σ (t a) * σ (t b) = ((sectionScalarCocycle D ζ t ht).coeff a b : ℂ) •
206       σ (t (a * b)) := by
207   rw [← map_mul, sectionDefect_mul D t ht, map_mul, hcentral]
208   change ((ζ (sectionDefect D t a b) : ℂ) • (1 : Module.End ℂ V)) *
209     σ (t (a * b)) = (ζ (sectionDefect D t a b) : ℂ) • σ (t (a * b))
210   rw [smul_mul_assoc, one_mul]
211 
212 /-- Extend the representation along the actual basis for any normalized
213 section, without assuming an algebra action for that section. -/
214 def sectionAction (ζ : Z →* ℂˣ) (t : A → H)
215     (ht : ∀ a, D.q (t a) = a) (htOne : t 1 = 1)
216     (σ : Representation ℂ H V)
217     (hcentral : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) :
218     TwistedAlgebra.Algebra (sectionScalarCocycle D ζ t ht)
219       (normalized_sectionScalarCocycle D ζ t ht htOne) →ₐ[ℂ] Module.End ℂ V :=
220   TwistedAction.action (sectionScalarCocycle D ζ t ht)
221     (normalized_sectionScalarCocycle D ζ t ht htOne) (fun a => σ (t a))
222     (by rw [htOne, map_one]) (sectionOperators_mul D ζ t ht σ hcentral)
223 
224 @[simp] theorem sectionAction_basis (ζ : Z →* ℂˣ) (t : A → H)
225     (ht : ∀ a, D.q (t a) = a) (htOne : t 1 = 1)
226     (σ : Representation ℂ H V)
227     (hcentral : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) (a : A) :
228     sectionAction D ζ t ht htOne σ hcentral
229       (TwistedAlgebra.basis (sectionScalarCocycle D ζ t ht)
230         (normalized_sectionScalarCocycle D ζ t ht htOne) a) = σ (t a) :=
231   TwistedAction.action_basis _ _ _ _ _ a
232 
233 /-- The algebra action from any normalized section is exactly the canonical
234 action transported through the constructed section-change equivalence. -/
235 theorem sectionAction_eq_transport (ζ : Z →* ℂˣ) (t : A → H)
236     (ht : ∀ a, D.q (t a) = a) (htOne : t 1 = 1)
237     (σ : Representation ℂ H V)
238     (hcentral : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) :
239     sectionAction D ζ t ht htOne σ hcentral =
240       (CentralCharacter.toAlgebraAction D ζ σ hcentral).comp
241         (sectionAlgebraEquiv D ζ t ht htOne).toAlgHom := by
242   apply AlgHom.toLinearMap_injective
243   apply (TwistedAlgebra.basis (sectionScalarCocycle D ζ t ht)
244     (normalized_sectionScalarCocycle D ζ t ht htOne)).ext
245   intro a
246   change sectionAction D ζ t ht htOne σ hcentral _ =
247     CentralCharacter.toAlgebraAction D ζ σ hcentral (sectionAlgebraEquiv D ζ t ht htOne _)
248   rw [sectionAction_basis, sectionAlgebraEquiv_basis, map_smul]
249   rw [CentralCharacter.toAlgebraAction_basis]
250   exact sectionOperators_factor D ζ t ht σ hcentral a
251 
252 /-- Two arbitrary section constructions give the same representation action
253 after the explicit section-change equivalence. -/
254 theorem sectionAction_betweenSections (ζ : Z →* ℂˣ) (t u : A → H)
255     (ht : ∀ a, D.q (t a) = a) (hu : ∀ a, D.q (u a) = a)
256     (htOne : t 1 = 1) (huOne : u 1 = 1) (σ : Representation ℂ H V)
257     (hcentral : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) :
258     sectionAction D ζ u hu huOne σ hcentral =
259       (sectionAction D ζ t ht htOne σ hcentral).comp
260         (betweenSectionsEquiv D ζ t u ht hu htOne huOne).toAlgHom := by
261   rw [sectionAction_eq_transport D ζ u hu huOne,
262     sectionAction_eq_transport D ζ t ht htOne]
263   ext x
264   simp only [AlgHom.comp_apply, AlgEquiv.coe_toAlgHom, betweenSectionsEquiv,
265     AlgEquiv.trans_apply, AlgEquiv.apply_symm_apply]
266 
267 end PaperXI.CentralExtension

Back to source controls