NormalizerExtensionInducing58.lean

1 import PaperXI.CentralExtensionInducing
2 import PaperXI.QuotientRepresentation
3 import Mathlib.GroupTheory.SemidirectProduct
4 import Mathlib.Tactic.Group
5 import Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
6 
7 /-!
8 # Extension across a noncentral normalizing cyclic direction
9 
10 A single conjugation intertwiner propagates to all integer powers. Unique
11 semidirect coordinates then define an action on the literal generated subgroup.
12 No centrality assumption is made on the adjoined ambient group element.
13 -/
14 set_option autoImplicit false
15 noncomputable section
16 namespace PaperXI.NormalizerExtensionInducing58
17 
18 section Covariance
19 variable {N H : Type*} [Group N] [Group H]
20 
21 /-- Compatible automorphism/operator pairs form a group, including inverses. -/
22 def compatiblePairs (f : N →* H) : Subgroup (MulAut N × H) where
23   carrier := {p | ∀ x, f (p.1 x) = p.2 * f x * p.2⁻¹}
24   one_mem' := by simp
25   mul_mem' := by
26     intro a b ha hb x
27     change f (a.1 (b.1 x)) = (a.2 * b.2) * f x * (a.2 * b.2)⁻¹
28     rw [ha, hb]
29     group
30   inv_mem' := by
31     intro a ha x
32     change f (a.1⁻¹ x) = a.2⁻¹ * f x * (a.2⁻¹)⁻¹
33     have he := ha (a.1⁻¹ x)
34     have he' : f x = a.2 * f (a.1⁻¹ x) * a.2⁻¹ := by simpa using he
35     calc
36       f (a.1⁻¹ x) = a.2⁻¹ * (a.2 * f (a.1⁻¹ x) * a.2⁻¹) * a.2 := by group
37       _ = a.2⁻¹ * f x * (a.2⁻¹)⁻¹ := by rw [← he']; simp
38 
39 /-- One generator covariance identity implies every positive and negative power. -/
40 theorem covariance_zpow (f : N →* H) (α : MulAut N) (A : H)
41     (h : ∀ x, f (α x) = A * f x * A⁻¹) (r : ℤ) (x : N) :
42     f ((α ^ r) x) = A ^ r * f x * (A ^ r)⁻¹ := by
43   have hp : (α, A) ∈ compatiblePairs f := h
44   have hh := (compatiblePairs f).zpow_mem hp r
45   exact hh x
46 end Covariance
47 
48 section Coordinates
49 variable {G : Type*} [Group G]
50 variable (J : Subgroup G) (t : G) (ht : t ∈ Subgroup.normalizer (J : Set G))
51 
52 /-- The actual conjugation automorphism of the original subgroup. -/
53 def conjugation : MulAut J := J.normalizerMonoidHom ⟨t, ht⟩
54 
55 /-- Integer powers act by actual conjugation inside the ambient group. -/
56 def conjugationAction : Multiplicative ℤ →* MulAut J :=
57   zpowersHom (MulAut J) (conjugation J t ht)
58 
59 @[simp] theorem conjugation_coe (j : J) :
60     ((conjugation J t ht j : J) : G) = t * (j : G) * t⁻¹ := rfl
61 
62 @[simp] theorem conjugationAction_coe (r : Multiplicative ℤ) (j : J) :
63     ((conjugationAction J t ht r j : J) : G) =
64       t ^ r.toAdd * (j : G) * (t ^ r.toAdd)⁻¹ := by
65   exact covariance_zpow J.subtype (conjugation J t ht) t
66     (fun x => conjugation_coe J t ht x) r.toAdd j
67 
68 /-- Actual normal forms multiply by the semidirect rule. -/
69 def normalFormHom : SemidirectProduct J (Multiplicative ℤ) (conjugationAction J t ht) →* G :=
70   SemidirectProduct.lift J.subtype (zpowersHom G t) (by
71     intro r
72     ext j
73     exact conjugationAction_coe J t ht r j)
74 
75 @[simp] theorem normalFormHom_apply
76     (p : SemidirectProduct J (Multiplicative ℤ) (conjugationAction J t ht)) :
77     normalFormHom J t ht p = (p.left : G) * t ^ p.right.toAdd := rfl
78 
79 /-- The literal subgroup generated by the original subgroup and t. -/
80 def extendedSubgroup : Subgroup G := (normalFormHom J t ht).range
81 
82 theorem le_extendedSubgroup : J ≤ extendedSubgroup J t ht := by
83   intro j hj
84   exact ⟨SemidirectProduct.inl ⟨j, hj⟩, by simp⟩
85 
86 theorem generator_mem : t ∈ extendedSubgroup J t ht := by
87   exact ⟨SemidirectProduct.inr (Multiplicative.ofAdd 1), by simp⟩
88 
89 theorem extendedSubgroup_eq_sup : extendedSubgroup J t ht = J ⊔ Subgroup.zpowers t := by
90   apply le_antisymm
91   · rintro g ⟨p, rfl⟩
92     exact Subgroup.mul_mem _ ((show J ≤ J ⊔ Subgroup.zpowers t from le_sup_left) p.left.property)
93       ((show Subgroup.zpowers t ≤ J ⊔ Subgroup.zpowers t from le_sup_right)
94         (Subgroup.zpow_mem _ (Subgroup.mem_zpowers t) p.right.toAdd))
95   · exact sup_le (le_extendedSubgroup J t ht) (Subgroup.zpowers_le.mpr (generator_mem J t ht))
96 
97 theorem normalFormHom_injective (hfree : ∀ r : ℤ, t ^ r ∈ J → r = 0) :
98     Function.Injective (normalFormHom J t ht) := by
99   apply (injective_iff_map_eq_one _).mpr
100   intro p hp
101   have he : t ^ p.right.toAdd = (p.left : G)⁻¹ := by
102     have hh := congrArg (fun x : G => (p.left : G)⁻¹ * x) hp
103     simpa [mul_assoc] using hh
104   have hr : p.right.toAdd = 0 := hfree _ (he ▸ J.inv_mem p.left.property)
105   have hr' : p.right = 1 := congrArg Multiplicative.ofAdd hr
106   have hj : p.left = 1 := Subtype.ext (by simpa [hr'] using hp)
107   apply SemidirectProduct.ext
108   · exact hj
109   · exact hr'
110 
111 /-- Unique noncentral semidirect coordinates on an actual subgroup of G. -/
112 def normalFormEquiv (hfree : ∀ r : ℤ, t ^ r ∈ J → r = 0) :
113     SemidirectProduct J (Multiplicative ℤ) (conjugationAction J t ht) ≃*
114       extendedSubgroup J t ht := MonoidHom.ofInjective (normalFormHom_injective J t ht hfree)
115 @[simp] theorem normalFormEquiv_coe
116     (hfree : ∀ r : ℤ, t ^ r ∈ J → r = 0)
117     (p : SemidirectProduct J (Multiplicative ℤ) (conjugationAction J t ht)) :
118     ((normalFormEquiv J t ht hfree p : extendedSubgroup J t ht) : G) =
119       (p.left : G) * t ^ p.right.toAdd := rfl
120 
121 /-- The original subgroup inside its actual generated extension. -/
122 def subgroupInclusion : J →* extendedSubgroup J t ht :=
123   Subgroup.inclusion (le_extendedSubgroup J t ht)
124 
125 /-- The normalizing generator as an element of the actual extended subgroup. -/
126 def generator : extendedSubgroup J t ht := ⟨t, generator_mem J t ht⟩
127 
128 variable {k V : Type*} [Field k] [AddCommGroup V] [Module k V]
129 variable (σ : Representation k J V) (A : Units (Module.End k V))
130 variable (hA : ∀ j, σ.asGroupHom (conjugation J t ht j) = A * σ.asGroupHom j * A⁻¹)
131 
132 /-- The action on semidirect coordinates, derived from one generator covariance. -/
133 def semidirectRepresentation :
134     Representation k (SemidirectProduct J (Multiplicative ℤ) (conjugationAction J t ht)) V :=
135   (Units.coeHom (Module.End k V)).comp
136     (SemidirectProduct.lift σ.asGroupHom (zpowersHom (Units (Module.End k V)) A) (by
137       intro r
138       apply MonoidHom.ext
139       intro j
140       exact covariance_zpow σ.asGroupHom (conjugation J t ht) A hA r.toAdd j))
141 
142 /-- Extend the given action to the literal subgroup generated by J and t. -/
143 def extendedRepresentation (hfree : ∀ r : ℤ, t ^ r ∈ J → r = 0) :
144     Representation k (extendedSubgroup J t ht) V :=
145   (semidirectRepresentation J t ht σ A hA).comp (normalFormEquiv J t ht hfree).symm.toMonoidHom
146 
147 @[simp] theorem extendedRepresentation_normalForm
148     (hfree : ∀ r : ℤ, t ^ r ∈ J → r = 0)
149     (p : SemidirectProduct J (Multiplicative ℤ) (conjugationAction J t ht)) :
150     extendedRepresentation J t ht σ A hA hfree (normalFormEquiv J t ht hfree p) =
151       σ p.left * (A ^ p.right.toAdd : Units (Module.End k V)) := by
152   simp [extendedRepresentation, semidirectRepresentation, SemidirectProduct.lift,
153     Representation.asGroupHom_apply]
154 
155 @[simp] theorem extendedRepresentation_restrict
156     (hfree : ∀ r : ℤ, t ^ r ∈ J → r = 0) (j : J) :
157     extendedRepresentation J t ht σ A hA hfree (subgroupInclusion J t ht j) = σ j := by
158   have he : subgroupInclusion J t ht j =
159       normalFormEquiv J t ht hfree (SemidirectProduct.inl j) := Subtype.ext (by simp [subgroupInclusion])
160   rw [he, extendedRepresentation_normalForm]
161   simp
162 
163 @[simp] theorem extendedRepresentation_generator
164     (hfree : ∀ r : ℤ, t ^ r ∈ J → r = 0) :
165     extendedRepresentation J t ht σ A hA hfree (generator J t ht) = (A : Module.End k V) := by
166   have he : generator J t ht = normalFormEquiv J t ht hfree
167       (SemidirectProduct.inr (Multiplicative.ofAdd 1)) := Subtype.ext (by simp [generator])
168   rw [he, extendedRepresentation_normalForm]
169   simp
170 
171 /-- Extending a genuine irreducible action preserves irreducibility. -/
172 theorem extendedRepresentation_irreducible
173     (hfree : ∀ r : ℤ, t ^ r ∈ J → r = 0) [Representation.IsIrreducible σ] :
174     Representation.IsIrreducible (extendedRepresentation J t ht σ A hA hfree) := by
175   let : Nontrivial V := GeneratedIrreducibility.nontrivial_space σ
176   apply RepresentationStability.irreducible_of_stable
177   intro S hS
178   apply RepresentationStability.eq_bot_or_top σ S
179   intro j v hv
180   simpa using hS (subgroupInclusion J t ht j) v hv
181 
182 /-- An actual intertwining equivalence supplies the generator covariance. -/
183 theorem equiv_unit_covariance
184     (e : Representation.Equiv σ (σ.comp (conjugation J t ht).toMonoidHom)) (j : J) :
185     σ.asGroupHom (conjugation J t ht j) =
186       LinearMap.GeneralLinearGroup.ofLinearEquiv e.toLinearEquiv * σ.asGroupHom j *
187         (LinearMap.GeneralLinearGroup.ofLinearEquiv e.toLinearEquiv)⁻¹ := by
188   apply Units.ext
189   apply LinearMap.ext
190   intro v
191   change σ (conjugation J t ht j) v =
192     e.toLinearEquiv (σ j (e.toLinearEquiv.symm v))
193   have he := LinearMap.congr_fun (e.isIntertwining' j) (e.toLinearEquiv.symm v)
194   change e.toLinearEquiv (σ j (e.toLinearEquiv.symm v)) =
195     σ (conjugation J t ht j) (e.toLinearEquiv (e.toLinearEquiv.symm v)) at he
196   rw [e.toLinearEquiv.apply_symm_apply] at he
197   exact he.symm
198 
199 /-- A single nonzero normalizer intertwiner is invertible by actual irreducibility. -/
200 theorem intertwiner_bijective [Representation.IsIrreducible σ]
201     (F : Representation.IntertwiningMap σ (σ.comp (conjugation J t ht).toMonoidHom))
202     (hF : F ≠ 0) : Function.Bijective F := by
203   let : Representation.IsIrreducible (σ.comp (conjugation J t ht).toMonoidHom) :=
204     (QuotientRepresentation.irreducible_comp_iff (conjugation J t ht).toMonoidHom
205       (conjugation J t ht).surjective σ).mpr inferInstance
206   exact (Representation.IsIrreducible.bijective_or_eq_zero F).resolve_right hF
207 
208 /-- Extend from one genuine intertwining equivalence, with no scalar action requirement. -/
209 def extensionOfEquiv
210     (e : Representation.Equiv σ (σ.comp (conjugation J t ht).toMonoidHom))
211     (hfree : ∀ r : ℤ, t ^ r ∈ J → r = 0) :
212     Representation k (extendedSubgroup J t ht) V :=
213   extendedRepresentation J t ht σ (LinearMap.GeneralLinearGroup.ofLinearEquiv e.toLinearEquiv)
214     (equiv_unit_covariance J t ht σ e) hfree
215 
216 @[simp] theorem extensionOfEquiv_restrict
217     (e : Representation.Equiv σ (σ.comp (conjugation J t ht).toMonoidHom))
218     (hfree : ∀ r : ℤ, t ^ r ∈ J → r = 0) (j : J) :
219     extensionOfEquiv J t ht σ e hfree (subgroupInclusion J t ht j) = σ j := by
220   simp [extensionOfEquiv]
221 
222 @[simp] theorem extensionOfEquiv_generator
223     (e : Representation.Equiv σ (σ.comp (conjugation J t ht).toMonoidHom))
224     (hfree : ∀ r : ℤ, t ^ r ∈ J → r = 0) :
225     extensionOfEquiv J t ht σ e hfree (generator J t ht) = e.toLinearMap := by
226   simp [extensionOfEquiv]
227   rfl
228 
229 /-- A nonzero normalizer Hom supplies an actual irreducible extension to the
230 literal generated subgroup; its generator action is the supplied Hom operator. -/
231 theorem exists_extension_of_nonzero [Representation.IsIrreducible σ]
232     (hfree : ∀ r : ℤ, t ^ r ∈ J → r = 0)
233     (F : Representation.IntertwiningMap σ (σ.comp (conjugation J t ht).toMonoidHom))
234     (hF : F ≠ 0) :
235     ∃ Λ : Representation k (extendedSubgroup J t ht) V,
236       (∀ j : J, Λ (subgroupInclusion J t ht j) = σ j) ∧
237       Λ (generator J t ht) = F.toLinearMap ∧ Representation.IsIrreducible Λ := by
238   let e := F.ofBijective (intertwiner_bijective J t ht σ F hF)
239   refine ⟨extensionOfEquiv J t ht σ e hfree, ?_, ?_, ?_⟩
240   · intro j
241     exact extensionOfEquiv_restrict J t ht σ e hfree j
242   · exact extensionOfEquiv_generator J t ht σ e hfree
243   · exact extendedRepresentation_irreducible J t ht σ _ _ hfree
244 
245 section Topology
246 variable [TopologicalSpace G] [IsTopologicalGroup G]
247 
248 /-- The actual noncentral extension subgroup is open when J is open. -/
249 theorem extendedSubgroup_isOpen (hJ : IsOpen (J : Set G)) :
250     IsOpen (extendedSubgroup J t ht : Set G) :=
251   Subgroup.isOpen_mono (le_extendedSubgroup J t ht) hJ
252 
253 /-- Every extended vector stabilizer contains its open original stabilizer. -/
254 theorem extendedRepresentation_smooth
255     (hfree : ∀ r : ℤ, t ^ r ∈ J → r = 0)
256     (hJ : IsOpen (J : Set G)) (hσ : SmoothDegreeQuotient.IsSmooth σ) :
257     SmoothDegreeQuotient.IsSmooth (extendedRepresentation J t ht σ A hA hfree) := by
258   intro v
259   let B := (SmoothDegreeQuotient.vectorStabilizer σ v).map J.subtype
260   have hB : IsOpen (B : Set G) := hJ.isOpenMap_subtype_val _ (hσ v)
261   apply Subgroup.isOpen_mono (H₁ := B.subgroupOf (extendedSubgroup J t ht)) ?_
262     ((extendedSubgroup J t ht).subgroupOf_isOpen B hB)
263   intro x hx
264   obtain ⟨j, hj, he⟩ := hx
265   have hxe : x = subgroupInclusion J t ht j := Subtype.ext he.symm
266   change extendedRepresentation J t ht σ A hA hfree x v = v
267   rw [hxe, extendedRepresentation_restrict]
268   exact hj
269 end Topology
270 end Coordinates
271 
272 end PaperXI.NormalizerExtensionInducing58

Back to source controls