TypeSideDescent.lean

1 import PaperXI.QuotientRepresentation
2 import PaperXI.GeneratedIrreducibility
3 import Mathlib.Analysis.Complex.Basic
4 import Mathlib.GroupTheory.Index
5 import Mathlib.GroupTheory.Subgroup.Center
6 
7 /-! The actual type-side scalar restriction and quotient action. The source
8 input that an irreducible representation contains the invariant character
9 is used through its nonzero character eigenspace; scalar restriction on
10 the whole representation is a conclusion, not an additional assumption. -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.TypeSideDescent
14 
15 variable {G V : Type*} [Group G] [AddCommGroup V] [Module ℂ V]
16 
17 /-- Conjugation in a normal subgroup, retaining the actual subgroup element. -/
18 def conjugate (H : Subgroup G) [H.Normal] (g : G) (h : H) : H :=
19   ⟨g * h * g⁻¹, Subgroup.Normal.conj_mem (inferInstance : H.Normal) (h : G) h.property g⟩
20 
21 /-- The invariance of the actual character under the ambient group. -/
22 def Invariant (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ) : Prop :=
23   ∀ (g : G) (h : H), θ (conjugate H g h) = θ h
24 
25 /-- The simultaneous character eigenspace in the supplied representation. -/
26 def characterSpace (H : Subgroup G) (θ : H →* ℂˣ) (η : Representation ℂ G V) :
27     Submodule ℂ V where
28   carrier := {v | ∀ h : H, η h v = (θ h : ℂ) • v}
29   zero_mem' := by simp
30   add_mem' := by
31     intro v w hv hw h
32     simp only [map_add, hv h, hw h, smul_add]
33   smul_mem' := by
34     intro c v hv h
35     simp only [map_smul, hv h, smul_comm c (θ h : ℂ)]
36 
37 /-- Containment of a one-dimensional character, expressed by a nonzero
38 vector in the actual simultaneous eigenspace. -/
39 def Contains (H : Subgroup G) (θ : H →* ℂˣ) (η : Representation ℂ G V) : Prop :=
40   ∃ v : V, v ≠ 0 ∧ v ∈ characterSpace H θ η
41 
42 /-- The actual one-dimensional representation associated to the character. -/
43 def characterRepresentation (H : Subgroup G) (θ : H →* ℂˣ) : Representation ℂ H ℂ where
44   toFun h := (θ h : ℂ) • LinearMap.id
45   map_one' := by simp [Module.End.one_eq_id]
46   map_mul' a b := by
47     apply LinearMap.ext
48     intro z
49     simp [mul_smul, mul_left_comm]
50 
51 /-- The eigenspace formulation of containment is equivalent to an actual
52 nonzero intertwiner from the one-dimensional character representation. -/
53 theorem contains_iff_nonzero_intertwiner (H : Subgroup G) (θ : H →* ℂˣ)
54     (η : Representation ℂ G V) :
55     Contains H θ η ↔ ∃ F : Representation.IntertwiningMap (characterRepresentation H θ)
56       (η.comp H.subtype), F ≠ 0 := by
57   constructor
58   · rintro ⟨v, hv, hmem⟩
59     let F : Representation.IntertwiningMap (characterRepresentation H θ)
60         (η.comp H.subtype) :=
61       ⟨LinearMap.toSpanSingleton ℂ V v, fun h => by
62         apply LinearMap.ext
63         intro z
64         change ((θ h : ℂ) • z) • v = η (h : G) (z • v)
65         rw [map_smul, hmem h]
66         simp [smul_smul, mul_comm]⟩
67     refine ⟨F, ?_⟩
68     intro hF
69     have heq := congrArg (fun f : Representation.IntertwiningMap
70       (characterRepresentation H θ) (η.comp H.subtype) => f 1) hF
71     exact hv (by simpa [F] using heq)
72   · rintro ⟨F, hF⟩
73     refine ⟨F 1, ?_, ?_⟩
74     · intro hzero
75       apply hF
76       apply Representation.IntertwiningMap.ext
77       apply LinearMap.ext
78       intro z
79       have hz := F.map_smul z (1 : ℂ)
80       simpa [hzero] using hz
81     · intro h
82       have heq := (Representation.IntertwiningMap.isIntertwining
83         (characterRepresentation H θ) (η.comp H.subtype) F h 1).symm
84       exact heq.trans (F.map_smul (θ h : ℂ) 1)
85 
86 theorem characterSpace_stable (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
87     (hθ : Invariant H θ) (η : Representation ℂ G V) (g : G)
88     {v : V} (hv : v ∈ characterSpace H θ η) : η g v ∈ characterSpace H θ η := by
89   intro h
90   have hmul : η (h : G) * η g = η g * η (conjugate H g⁻¹ h : G) := by
91     rw [← map_mul, ← map_mul]
92     congr 1
93     simp [conjugate, mul_assoc]
94   change (η (h : G) * η g) v = (θ h : ℂ) • η g v
95   rw [hmul, Module.End.mul_apply, hv (conjugate H g⁻¹ h), hθ]
96   exact (η g).map_smul _ _
97 
98 /-- The character eigenspace is an actual subrepresentation by invariance. -/
99 def characterSubrepresentation (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
100     (hθ : Invariant H θ) (η : Representation ℂ G V) : Subrepresentation η :=
101   ⟨characterSpace H θ η, fun g _ hv => characterSpace_stable H θ hθ η g hv⟩
102 
103 /-- Irreducibility promotes containment of the invariant character to its
104 scalar action on every vector. -/
105 theorem scalar_restriction (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
106     (hθ : Invariant H θ) (η : Representation ℂ G V) [Representation.IsIrreducible η]
107     (hcontains : Contains H θ η) (h : H) : η (h : G) = (θ h : ℂ) • LinearMap.id := by
108   let S := characterSubrepresentation H θ hθ η
109   have hS : S ≠ ⊥ := by
110     intro hs
111     obtain ⟨v, hv, hmem⟩ := hcontains
112     have hz : v ∈ (⊥ : Subrepresentation η) := hs ▸ hmem
113     exact hv hz
114   have htop : S = ⊤ := (eq_bot_or_eq_top S).resolve_left hS
115   ext v
116   have hv : v ∈ S := htop ▸ (show v ∈ (⊤ : Subrepresentation η) from trivial)
117   exact hv h
118 
119 /-- The kernel of the character viewed as an actual subgroup of the ambient
120 group. Invariance is recorded so that its normality is available canonically. -/
121 def characterKernel (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
122     (_hθ : Invariant H θ) : Subgroup G := θ.ker.map H.subtype
123 
124 theorem characterKernel_le (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
125     (hθ : Invariant H θ) : characterKernel H θ hθ ≤ H := by
126   rintro g ⟨h, _, rfl⟩
127   exact h.property
128 
129 @[simp] theorem mem_characterKernel (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
130     (hθ : Invariant H θ) (h : H) :
131     (h : G) ∈ characterKernel H θ hθ ↔ θ h = 1 := by
132   constructor
133   · rintro ⟨h', hh', heq⟩
134     have : h' = h := Subtype.ext heq
135     simpa [this] using hh'
136   · intro hh
137     exact ⟨h, hh, rfl⟩
138 
139 instance characterKernel_normal (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
140     (hθ : Invariant H θ) : (characterKernel H θ hθ).Normal where
141   conj_mem := by
142     rintro g ⟨h, hh, rfl⟩ a
143     refine ⟨conjugate H a h, ?_, rfl⟩
144     exact (hθ a h).trans hh
145 
146 /-- The character kernel acts trivially, as a consequence of containment. -/
147 theorem characterKernel_le_ker (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
148     (hθ : Invariant H θ) (η : Representation ℂ G V) [Representation.IsIrreducible η]
149     (hcontains : Contains H θ η) : characterKernel H θ hθ ≤ η.ker := by
150   rintro g ⟨h, hh, rfl⟩
151   change η (h : G) = 1
152   rw [scalar_restriction H θ hθ η hcontains h]
153   have hh' : θ h = 1 := hh
154   simp [hh', Module.End.one_eq_id]
155 
156 /-- The actual action descended to `J¹ / ker θ`. -/
157 def representation (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
158     (hθ : Invariant H θ) (η : Representation ℂ G V) [Representation.IsIrreducible η]
159     (hcontains : Contains H θ η) : Representation ℂ (G ⧸ characterKernel H θ hθ) V :=
160   QuotientRepresentation.descend (characterKernel H θ hθ) η
161     (characterKernel_le_ker H θ hθ η hcontains)
162 
163 @[simp] theorem representation_apply (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
164     (hθ : Invariant H θ) (η : Representation ℂ G V) [Representation.IsIrreducible η]
165     (hcontains : Contains H θ η) (g : G) :
166     representation H θ hθ η hcontains (QuotientGroup.mk' (characterKernel H θ hθ) g) =
167       η g := rfl
168 
169 theorem representation_irreducible (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
170     (hθ : Invariant H θ) (η : Representation ℂ G V) [Representation.IsIrreducible η]
171     (hcontains : Contains H θ η) :
172     Representation.IsIrreducible (representation H θ hθ η hcontains) :=
173   QuotientRepresentation.descend_irreducible _ _ _
174 
175 /-- Finiteness of the central quotient follows from the actual finite
176 quotient and finite character image, without assuming the ambient group finite. -/
177 theorem finite_quotient (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
178     (hθ : Invariant H θ) [Finite (G ⧸ H)] [Finite θ.range] :
179     Finite (G ⧸ characterKernel H θ hθ) := by
180   let : H.FiniteIndex := Subgroup.finiteIndex_of_finite_quotient
181   have hindex : (characterKernel H θ hθ).FiniteIndex := by
182     constructor
183     rw [characterKernel, Subgroup.index_map_subtype]
184     exact mul_ne_zero Subgroup.FiniteIndex.index_ne_zero Subgroup.FiniteIndex.index_ne_zero
185   exact @Subgroup.finite_quotient_of_finiteIndex G _ (characterKernel H θ hθ) hindex
186 
187 /-- The actual quotient map onto the type-side symplectic quotient. -/
188 def quotientProjection (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
189     (hθ : Invariant H θ) : (G ⧸ characterKernel H θ hθ) →* (G ⧸ H) :=
190   QuotientGroup.lift (characterKernel H θ hθ) (QuotientGroup.mk' H) (by
191     simpa using characterKernel_le H θ hθ)
192 
193 @[simp] theorem quotientProjection_apply (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
194     (hθ : Invariant H θ) (g : G) :
195     quotientProjection H θ hθ (QuotientGroup.mk' (characterKernel H θ hθ) g) =
196       QuotientGroup.mk' H g := rfl
197 
198 theorem quotientProjection_surjective (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
199     (hθ : Invariant H θ) : Function.Surjective (quotientProjection H θ hθ) :=
200   QuotientGroup.lift_surjective_of_surjective _ _ QuotientGroup.mk_surjective _
201 
202 /-- Exactness identifies the kernel with the image of `H¹ / ker θ`. -/
203 theorem quotientProjection_ker (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
204     (hθ : Invariant H θ) :
205     (quotientProjection H θ hθ).ker = H.map (QuotientGroup.mk' (characterKernel H θ hθ)) := by
206   rw [quotientProjection, QuotientGroup.ker_lift, QuotientGroup.ker_mk']
207 
208 /-- Character invariance makes the distinguished subgroup central in the
209 actual quotient group. -/
210 theorem central_image (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
211     (hθ : Invariant H θ) :
212     H.map (QuotientGroup.mk' (characterKernel H θ hθ)) ≤
213       Subgroup.center (G ⧸ characterKernel H θ hθ) := by
214   rintro z ⟨h, hh, rfl⟩
215   rw [Subgroup.mem_center_iff]
216   intro a
217   obtain ⟨g, rfl⟩ := QuotientGroup.mk_surjective a
218   let hH : H := ⟨h, hh⟩
219   let q := QuotientGroup.mk' (characterKernel H θ hθ)
220   have heq : q (conjugate H g hH : G) = q h := by
221     apply QuotientGroup.eq.mpr
222     refine ⟨(conjugate H g hH)⁻¹ * hH, ?_, rfl⟩
223     change θ ((conjugate H g hH)⁻¹ * hH) = 1
224     simp [hθ g hH]
225   have heq' := congrArg (fun b => b * q g) heq
226   simpa [conjugate, hH, map_mul, mul_assoc, q] using heq'
227 
228 /-- The actual central quotient character. -/
229 def centralCharacter (H : Subgroup G) (θ : H →* ℂˣ) : (H ⧸ θ.ker) →* ℂˣ :=
230   QuotientGroup.lift θ.ker θ le_rfl
231 
232 @[simp] theorem centralCharacter_apply (H : Subgroup G) (θ : H →* ℂˣ) (h : H) :
233     centralCharacter H θ (QuotientGroup.mk' θ.ker h) = θ h := rfl
234 
235 theorem centralCharacter_injective (H : Subgroup G) (θ : H →* ℂˣ) :
236     Function.Injective (centralCharacter H θ) :=
237   (QuotientGroup.injective_lift_iff _ _ _).mpr rfl
238 
239 /-- Include `H¹ / ker θ` into the actual finite central quotient. -/
240 def centerInclusion (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
241     (hθ : Invariant H θ) : (H ⧸ θ.ker) →* (G ⧸ characterKernel H θ hθ) :=
242   QuotientGroup.lift θ.ker
243     ((QuotientGroup.mk' (characterKernel H θ hθ)).comp H.subtype) (by
244       intro h hh
245       change (h : G ⧸ characterKernel H θ hθ) = 1
246       exact (QuotientGroup.eq_one_iff (h : G)).mpr ⟨h, hh, rfl⟩)
247 
248 @[simp] theorem centerInclusion_apply (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
249     (hθ : Invariant H θ) (h : H) :
250     centerInclusion H θ hθ (QuotientGroup.mk' θ.ker h) =
251       QuotientGroup.mk' (characterKernel H θ hθ) (h : G) := rfl
252 
253 theorem centerInclusion_injective (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
254     (hθ : Invariant H θ) : Function.Injective (centerInclusion H θ hθ) := by
255   apply (QuotientGroup.injective_lift_iff _ _ _).mpr
256   ext h
257   change θ h = 1 ↔ (h : G ⧸ characterKernel H θ hθ) = 1
258   rw [QuotientGroup.eq_one_iff, mem_characterKernel]
259 
260 theorem centerInclusion_range (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
261     (hθ : Invariant H θ) :
262     (centerInclusion H θ hθ).range = H.map (QuotientGroup.mk' (characterKernel H θ hθ)) := by
263   ext a
264   constructor
265   · rintro ⟨z, rfl⟩
266     obtain ⟨h, rfl⟩ := QuotientGroup.mk_surjective z
267     exact ⟨h, h.property, rfl⟩
268   · rintro ⟨h, hh, rfl⟩
269     exact ⟨QuotientGroup.mk' θ.ker ⟨h, hh⟩, rfl⟩
270 
271 /-- The constructed center inclusion and quotient map form an exact sequence. -/
272 theorem exact_center_quotient (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
273     (hθ : Invariant H θ) :
274     (centerInclusion H θ hθ).range = (quotientProjection H θ hθ).ker := by
275   rw [centerInclusion_range, quotientProjection_ker]
276 
277 theorem centerInclusion_central (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
278     (hθ : Invariant H θ) :
279     (centerInclusion H θ hθ).range ≤ Subgroup.center (G ⧸ characterKernel H θ hθ) := by
280   rw [centerInclusion_range]
281   exact central_image H θ hθ
282 
283 /-- The descended action has precisely the character induced by `θ` on its
284 actual central subgroup, after proving scalar restriction from containment. -/
285 theorem central_action (H : Subgroup G) [H.Normal] (θ : H →* ℂˣ)
286     (hθ : Invariant H θ) (η : Representation ℂ G V) [Representation.IsIrreducible η]
287     (hcontains : Contains H θ η) (z : H ⧸ θ.ker) :
288     representation H θ hθ η hcontains (centerInclusion H θ hθ z) =
289       (centralCharacter H θ z : ℂ) • LinearMap.id := by
290   obtain ⟨h, rfl⟩ := QuotientGroup.mk_surjective z
291   exact scalar_restriction H θ hθ η hcontains h
292 
293 end PaperXI.TypeSideDescent

Back to source controls