ScalarRepresentation112.lean

1 import PaperXI.GlobalHeisenbergBridge112
2 import PaperXI.RepresentationStability
3 import PaperXI.ScalarCocycle112
4 
5 /-! Construct an action of the actual group from labelled packet operators
6 and an explicit scalar cochain. The section multiplication and original theta
7 restriction are derived from the literal quotient kernel, not supplied as
8 representation or lambda hypotheses. Existence of a compatible quotient map
9 and preservation of any required dyadic lift remain separate obligations. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.ScalarRepresentation112
13 open Representation
14 
15 section ActualSection
16 variable {G A : Type*} [Group G] [Group A]
17   (D : Subgroup G) [D.Normal] (θ : D →* ℂˣ)
18   (hinv : TypeSideDescent.Invariant D θ)
19   (q : G →* A) (hker : q.ker = D)
20   (t : A → G) (ht : ∀ a, q (t a) = a) (ht1 : t 1 = 1)
21 
22 /-- The literal normal-subgroup remainder of an actual group element. -/
23 def sectionResidue (g : G) : D :=
24   ⟨g * (t (q g))⁻¹, by
25     rw [← hker]
26     change q (g * (t (q g))⁻¹) = 1
27     simp only [map_mul, map_inv, ht, mul_inv_cancel]⟩
28 
29 /-- The scalar retained from the original theta on the actual remainder. -/
30 def sectionScalar (g : G) : ℂˣ := θ (sectionResidue D q hker t ht g)
31 
32 /-- The theta-valued factor set of the actual normalized quotient section. -/
33 def sectionCocycle (a b : A) : ℂˣ :=
34   sectionScalar D θ q hker t ht (t a * t b)
35 
36 theorem sectionResidue_mul (g h : G) :
37     sectionResidue D q hker t ht (g * h) =
38       sectionResidue D q hker t ht g *
39         TypeSideDescent.conjugate D (t (q g)) (sectionResidue D q hker t ht h) *
40           sectionResidue D q hker t ht (t (q g) * t (q h)) := by
41   apply Subtype.ext
42   simp only [sectionResidue, TypeSideDescent.conjugate, Subgroup.coe_mul,
43     map_mul, ht]
44   group
45 
46 include hinv in
47 theorem sectionScalar_mul (g h : G) :
48     sectionScalar D θ q hker t ht (g * h) =
49       sectionScalar D θ q hker t ht g * sectionScalar D θ q hker t ht h *
50         sectionCocycle D θ q hker t ht (q g) (q h) := by
51   change θ (sectionResidue D q hker t ht (g * h)) = _
52   rw [sectionResidue_mul, map_mul, map_mul, hinv]
53   rfl
54 
55 omit [D.Normal] in
56 theorem sectionResidue_section (a : A) : sectionResidue D q hker t ht (t a) = 1 := by
57   apply Subtype.ext
58   simp only [sectionResidue, ht, mul_inv_cancel, Subgroup.coe_one]
59 
60 omit [D.Normal] in
61 theorem sectionScalar_section (a : A) : sectionScalar D θ q hker t ht (t a) = 1 := by
62   rw [sectionScalar, sectionResidue_section, map_one]
63 
64 omit [D.Normal] in
65 include ht1 in
66 theorem sectionScalar_one : sectionScalar D θ q hker t ht 1 = 1 := by
67   simpa only [ht1] using sectionScalar_section D θ q hker t ht 1
68 
69 omit [D.Normal] in
70 include ht1 in
71 theorem sectionCocycle_one_left (a : A) : sectionCocycle D θ q hker t ht 1 a = 1 := by
72   simpa only [sectionCocycle, ht1, one_mul] using sectionScalar_section D θ q hker t ht a
73 
74 omit [D.Normal] in
75 include ht1 in
76 theorem sectionCocycle_one_right (a : A) : sectionCocycle D θ q hker t ht a 1 = 1 := by
77   simpa only [sectionCocycle, ht1, mul_one] using sectionScalar_section D θ q hker t ht a
78 
79 include hinv in
80 /-- Associativity of the scalar factor set is derived from actual group
81 associativity and invariance of the same original theta. -/
82 theorem sectionCocycle_assoc (a b c : A) :
83     sectionCocycle D θ q hker t ht a b * sectionCocycle D θ q hker t ht (a * b) c =
84       sectionCocycle D θ q hker t ht b c * sectionCocycle D θ q hker t ht a (b * c) := by
85   have h := congrArg (sectionScalar D θ q hker t ht) (mul_assoc (t a) (t b) (t c))
86   simpa only [sectionScalar_mul D θ hinv, sectionScalar_section, ht, map_mul,
87     one_mul, mul_one] using h
88 
89 omit [D.Normal] in
90 include ht1 in
91 theorem sectionScalar_on_subgroup (d : D) :
92     sectionScalar D θ q hker t ht (d : G) = θ d := by
93   have hd : q (d : G) = 1 := by
94     change (d : G) ∈ q.ker
95     rw [hker]
96     exact d.property
97   apply congrArg θ
98   apply Subtype.ext
99   simp only [sectionResidue, hd, ht1, inv_one, mul_one]
100 
101 end ActualSection
102 
103 section PacketOperators
104 variable {P A V : Type*} [Group P] [Group A] [AddCommGroup V] [Module ℂ V]
105   (H : Subgroup P) [H.Normal] (χ : H →* ℂˣ)
106   (q : P →* A) (hker : q.ker = H) (t : A → P) (ht : ∀ a, q (t a) = a)
107   (ρ : Representation ℂ P V)
108   (hρ : ∀ h : H, ρ h = (χ h : ℂ) • LinearMap.id)
109 
110 /-- The packet's operators retain their quotient labels. -/
111 def packetOperator (a : A) : Module.End ℂ V := ρ (t a)
112 
113 omit [H.Normal] in
114 include hρ in
115 /-- The projective multiplication coefficient is the literal scalar
116 character of the actual section remainder. -/
117 theorem packetOperator_mul (a b : A) :
118     packetOperator t ρ a * packetOperator t ρ b =
119       (sectionCocycle H χ q hker t ht a b : ℂ) • packetOperator t ρ (a * b) := by
120   have hg : t a * t b =
121       (sectionResidue H q hker t ht (t a * t b) : P) * t (a * b) := by
122     simp only [sectionResidue, map_mul, ht]
123     group
124   change ρ (t a) * ρ (t b) = _
125   rw [← map_mul, hg, map_mul, hρ]
126   ext v
127   simp only [Module.End.mul_apply, LinearMap.smul_apply, LinearMap.id_apply,
128     sectionCocycle, sectionScalar, packetOperator]
129 
130 end PacketOperators
131 
132 section ScalarTransport
133 variable {G P A V : Type*} [Group G] [Group P] [Group A]
134   [AddCommGroup V] [Module ℂ V]
135   (D : Subgroup G) [D.Normal] (θ : D →* ℂˣ)
136   (hinv : TypeSideDescent.Invariant D θ)
137   (q : G →* A) (hker : q.ker = D)
138   (t : A → G) (ht : ∀ a, q (t a) = a) (ht1 : t 1 = 1)
139   (H : Subgroup P) [H.Normal] (χ : H →* ℂˣ)
140   (r : P →* A) (hkerP : r.ker = H)
141   (u : A → P) (hu : ∀ a, r (u a) = a) (hu1 : u 1 = 1)
142   (ρ : Representation ℂ P V)
143   (hρ : ∀ h : H, ρ h = (χ h : ℂ) • LinearMap.id)
144   (s : A → ℂˣ) (hs1 : s 1 = 1)
145   (hc : ∀ a b, sectionCocycle D θ q hker t ht a b =
146     (s a * s b / s (a * b)) * sectionCocycle H χ r hkerP u hu a b)
147 
148 /-- A scalar cochain constructs an honest representation of the actual group,
149 even when the packet center and actual center have different orders. -/
150 def scalarTransport : Representation ℂ G V where
151   toFun g := ((sectionScalar D θ q hker t ht g * s (q g) : ℂˣ) : ℂ) • ρ (u (q g))
152   map_one' := by
153     simp only [map_one, sectionScalar_one D θ q hker t ht ht1, hs1,
154       hu1, mul_one, Units.val_one, one_smul]
155   map_mul' g h := by
156     have hcoeff :
157         sectionScalar D θ q hker t ht (g * h) * s (q (g * h)) =
158           (sectionScalar D θ q hker t ht g * s (q g)) *
159           (sectionScalar D θ q hker t ht h * s (q h)) *
160             sectionCocycle H χ r hkerP u hu (q g) (q h) := by
161       rw [sectionScalar_mul D θ hinv, hc, map_mul]
162       simp only [div_eq_mul_inv]
163       simp [mul_assoc, mul_comm, mul_left_comm]
164     ext v
165     rw [hcoeff, map_mul]
166     have hp := LinearMap.congr_fun (packetOperator_mul H χ r hkerP u hu ρ hρ (q g) (q h)) v
167     change ρ (u (q g)) (ρ (u (q h)) v) = _ at hp
168     simp only [LinearMap.smul_apply, Units.val_mul, Module.End.mul_apply,
169       map_smul, smul_smul]
170     rw [hp]
171     simp only [LinearMap.smul_apply, packetOperator, smul_smul]
172     congr 1
173     ring
174 
175 omit [H.Normal] in
176 /-- The constructed actual action contains precisely the original theta on
177 the original subgroup, rather than a replacement central character. -/
178 theorem scalarTransport_on_subgroup (d : D) :
179     scalarTransport D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc (d : G) =
180       (θ d : ℂ) • LinearMap.id := by
181   have hd : q (d : G) = 1 := by
182     change (d : G) ∈ q.ker
183     rw [hker]
184     exact d.property
185   change ((sectionScalar D θ q hker t ht (d : G) * s (q (d : G)) : ℂˣ) : ℂ) •
186     ρ (u (q (d : G))) = _
187   rw [sectionScalar_on_subgroup D θ q hker t ht ht1, hd, hs1, hu1, map_one, mul_one]
188   rfl
189 
190 omit [H.Normal] in
191 /-- On each actual quotient-section element the representation is the packet
192 operator with exactly its derived scalar-cochain correction. -/
193 theorem scalarTransport_section (a : A) :
194     scalarTransport D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc (t a) =
195       (s a : ℂ) • ρ (u a) := by
196   change ((sectionScalar D θ q hker t ht (t a) * s (q (t a)) : ℂˣ) : ℂ) •
197     ρ (u (q (t a))) = _
198   rw [sectionScalar_section, ht, one_mul]
199 
200 omit [H.Normal] in
201 include hρ in
202 /-- Every packet operator is its section-labelled operator times its original
203 scalar remainder. This is an actual group identity, not a dimension argument. -/
204 theorem packet_normalForm (p : P) :
205     ρ p = (sectionScalar H χ r hkerP u hu p : ℂ) • ρ (u (r p)) := by
206   have hp : p = (sectionResidue H r hkerP u hu p : P) * u (r p) := by
207     simp only [sectionResidue]
208     group
209   calc
210     ρ p = ρ ((sectionResidue H r hkerP u hu p : P) * u (r p)) := congrArg ρ hp
211     _ = _ := by
212       rw [map_mul, hρ]
213       ext v
214       simp only [Module.End.mul_apply, LinearMap.smul_apply, LinearMap.id_apply, sectionScalar]
215 
216 omit [H.Normal] in
217 /-- The rescaled actual action is irreducible because every original packet
218 operator preserves each of its stable subspaces. No target eta iso is used. -/
219 theorem scalarTransport_irreducible [IsIrreducible ρ] :
220     IsIrreducible (scalarTransport D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc) := by
221   let : Nontrivial V := GeneratedIrreducibility.nontrivial_space ρ
222   apply RepresentationStability.irreducible_of_stable
223   intro S hS
224   apply RepresentationStability.eq_bot_or_top ρ S
225   intro p v hv
226   have hRv : ρ (u (r p)) v ∈ S := by
227     have hx := hS (t (r p)) v hv
228     have hs := S.smul_mem (((s (r p))⁻¹ : ℂˣ) : ℂ) hx
229     rw [scalarTransport_section D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc] at hs
230     simpa only [LinearMap.smul_apply, smul_smul, ← Units.val_mul,
231       inv_mul_cancel, Units.val_one, one_smul] using hs
232   rw [packet_normalForm H χ r hkerP u hu ρ hρ]
233   exact S.smul_mem _ hRv
234 
235 omit [H.Normal] in
236 /-- The actual theta occurrence is a conclusion of the transport on the
237 nonzero original packet carrier. -/
238 theorem scalarTransport_contains [Nontrivial V] :
239     TypeSideDescent.Contains D θ
240       (scalarTransport D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc) := by
241   obtain ⟨v, hv⟩ := exists_ne (0 : V)
242   refine ⟨v, hv, fun d => ?_⟩
243   rw [scalarTransport_on_subgroup D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc]
244   rfl
245 
246 end ScalarTransport
247 
248 section CochainExistence
249 variable {G P A V : Type*} [Group G] [Group P] [CommGroup A]
250   [AddCommGroup V] [Module ℂ V]
251 
252 /-- The scalar cocycle is constructed from the original character and actual
253 section, with all cocycle laws proved above. -/
254 def actualScalarCocycle
255     (D : Subgroup G) [D.Normal] (θ : D →* ℂˣ)
256     (hinv : TypeSideDescent.Invariant D θ)
257     (q : G →* A) (hker : q.ker = D)
258     (t : A → G) (ht : ∀ a, q (t a) = a) (ht1 : t 1 = 1) :
259     ScalarCocycle112.Cocycle A ℂˣ where
260   coeff := sectionCocycle D θ q hker t ht
261   assoc := sectionCocycle_assoc D θ hinv q hker t ht
262   one_left := sectionCocycle_one_left D θ q hker t ht ht1
263   one_right := sectionCocycle_one_right D θ q hker t ht ht1
264 
265 /-- The actual character commutator with the quotient label retained. -/
266 def sectionCommutator
267     (D : Subgroup G) (q : G →* A) (hker : q.ker = D)
268     (t : A → G) (ht : ∀ a, q (t a) = a) (a b : A) : D :=
269   ⟨t a * t b * (t a)⁻¹ * (t b)⁻¹, by
270     rw [← hker]
271     change q (t a * t b * (t a)⁻¹ * (t b)⁻¹) = 1
272     simp only [map_mul, map_inv, ht]
273     simp [mul_assoc]⟩
274 
275 /-- The scalar cocycle commutator is the original theta of the literal group
276 commutator. This translates quotient-form matching into the cochain theorem. -/
277 theorem sectionCocycle_commutator
278     (D : Subgroup G) (θ : D →* ℂˣ)
279     (q : G →* A) (hker : q.ker = D)
280     (t : A → G) (ht : ∀ a, q (t a) = a) (a b : A) :
281     sectionCocycle D θ q hker t ht a b / sectionCocycle D θ q hker t ht b a =
282       θ (sectionCommutator D q hker t ht a b) := by
283   have hz : sectionResidue D q hker t ht (t a * t b) /
284       sectionResidue D q hker t ht (t b * t a) = sectionCommutator D q hker t ht a b := by
285     apply Subtype.ext
286     simp only [sectionResidue, sectionCommutator, Subgroup.coe_div, map_mul, ht]
287     rw [mul_comm b a]
288     simp only [div_eq_mul_inv]
289     group
290   change θ (sectionResidue D q hker t ht (t a * t b)) /
291     θ (sectionResidue D q hker t ht (t b * t a)) = _
292   rw [← map_div, hz]
293 
294 /-- Equal labelled scalar commutators construct an honest irreducible actual
295 group action containing the literal original theta. The packet and actual
296 central subgroups need not be isomorphic. -/
297 theorem exists_actual_action_of_equal_scalar_commutators
298     (D : Subgroup G) [D.Normal] (θ : D →* ℂˣ)
299     (hinv : TypeSideDescent.Invariant D θ)
300     (q : G →* A) (hker : q.ker = D)
301     (t : A → G) (ht : ∀ a, q (t a) = a) (ht1 : t 1 = 1)
302     (H : Subgroup P) [H.Normal] (χ : H →* ℂˣ)
303     (hχ : TypeSideDescent.Invariant H χ)
304     (r : P →* A) (hkerP : r.ker = H)
305     (u : A → P) (hu : ∀ a, r (u a) = a) (hu1 : u 1 = 1)
306     (ρ : Representation ℂ P V) [IsIrreducible ρ]
307     (hρ : ∀ h : H, ρ h = (χ h : ℂ) • LinearMap.id)
308     (hcomm : ∀ a b,
309       sectionCocycle D θ q hker t ht a b / sectionCocycle D θ q hker t ht b a =
310         sectionCocycle H χ r hkerP u hu a b / sectionCocycle H χ r hkerP u hu b a) :
311     ∃ Ξ : Representation ℂ G V,
312       IsIrreducible Ξ ∧ TypeSideDescent.Contains D θ Ξ ∧
313         (∀ d : D, Ξ d = (θ d : ℂ) • LinearMap.id) := by
314   let cθ := actualScalarCocycle D θ hinv q hker t ht ht1
315   let cP := actualScalarCocycle H χ hχ r hkerP u hu hu1
316   obtain ⟨s, hs1, hc⟩ := ScalarCocycle112.same_commutator_exists_cochain cθ cP hcomm
317   let Ξ := scalarTransport D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc
318   let : Nontrivial V := GeneratedIrreducibility.nontrivial_space ρ
319   exact ⟨Ξ, scalarTransport_irreducible D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc,
320     scalarTransport_contains D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc,
321     scalarTransport_on_subgroup D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc⟩
322 
323 end CochainExistence
324 
325 section PrescribedEta
326 variable {G P A V W k X : Type*} [Group G] [Finite G] [Group P] [CommGroup A]
327   [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
328   [Field k] [AddCommGroup X] [Module k X]
329 
330 /-- The constructed packet realization is identified with the prescribed
331 actual eta using nondegenerate original quotient data. Equality of commutator
332 characters replaces a literal central-extension group isomorphism. For an
333 infinite J¹ this theorem is used on its actual finite J¹/ker(theta) quotient. -/
334 theorem bridge_to_prescribed_eta_of_equal_commutators
335     (D : Subgroup G) [D.Normal] (θ : D →* ℂˣ)
336     (hinv : TypeSideDescent.Invariant D θ)
337     (q : G →* A) (hker : q.ker = D)
338     (t : A → G) (ht : ∀ a, q (t a) = a) (ht1 : t 1 = 1)
339     (H : Subgroup P) [H.Normal] (χ : H →* ℂˣ)
340     (hχ : TypeSideDescent.Invariant H χ)
341     (r : P →* A) (hkerP : r.ker = H)
342     (u : A → P) (hu : ∀ a, r (u a) = a) (hu1 : u 1 = 1)
343     (ρ : Representation ℂ P V) [IsIrreducible ρ]
344     (hρ : ∀ h : H, ρ h = (χ h : ℂ) • LinearMap.id)
345     (hcomm : ∀ a b, θ (sectionCommutator D q hker t ht a b) =
346       χ (sectionCommutator H r hkerP u hu a b))
347     (η : Representation ℂ G W) [IsIrreducible η]
348     (hcontains : TypeSideDescent.Contains D θ η)
349     (τ : (G ⧸ D) ≃* Multiplicative X)
350     (B : X →ₗ[k] X →ₗ[k] k) (ψ : AddChar k ℂˣ) (hψ : ψ ≠ 1)
351     (hnd : ∀ v : X, (∀ z : X, B z v = 0) → v = 0)
352     (hform : ∀ g h : G, ψ (B (HeisenbergCharacterProfile111.coordinate D τ g)
353       (HeisenbergCharacterProfile111.coordinate D τ h)) =
354         HeisenbergCharacterProfile111.characterCommutator D τ θ g h) :
355     ∃ Ξ : Representation ℂ G V,
356       IsIrreducible Ξ ∧ TypeSideDescent.Contains D θ Ξ ∧
357         Nonempty (Representation.Equiv Ξ η) := by
358   have hc : ∀ a b,
359       sectionCocycle D θ q hker t ht a b / sectionCocycle D θ q hker t ht b a =
360         sectionCocycle H χ r hkerP u hu a b / sectionCocycle H χ r hkerP u hu b a := by
361     intro a b
362     rw [sectionCocycle_commutator, sectionCocycle_commutator, hcomm]
363   obtain ⟨Ξ, hΞ, hcontainsΞ, hscalarΞ⟩ :=
364     exists_actual_action_of_equal_scalar_commutators D θ hinv q hker t ht ht1
365       H χ hχ r hkerP u hu hu1 ρ hρ hc
366   let : IsIrreducible Ξ := hΞ
367   exact ⟨Ξ, hΞ, hcontainsΞ,
368     GlobalHeisenbergBridge112.equiv_of_common_quotient_form D θ τ B ψ hψ hnd hform
369       Ξ η hscalarΞ (TypeSideDescent.scalar_restriction D θ hinv η hcontains)⟩
370 
371 end PrescribedEta
372 
373 end PaperXI.ScalarRepresentation112

Back to source controls