CentralExtensionInducing.lean

1 import PaperXI.SmoothDegreeQuotient
2 import PaperXI.RepresentationStability
3 import Mathlib.Topology.Algebra.OpenSubgroup
4 import Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
5 
6 /-!
7 # Extending inducing data by a central infinite cyclic direction
8 
9 The extension is a representation of an actual subgroup of the ambient group.
10 Its hypotheses require that the adjoined central element has no nonzero power
11 in the original subgroup.  No assertion about simple types, intertwining, or
12 admissibility is supplied by this construction.
13 -/
14 set_option autoImplicit false
15 noncomputable section
16 namespace PaperXI.CentralExtensionInducing
17 
18 variable {G : Type*} [Group G]
19 
20 /-- A nonzero integer degree separates every nontrivial power from the degree kernel. -/
21 theorem hfree_from_degree (J : Subgroup G) (δ : G →* Multiplicative ℤ)
22     (hJ : J ≤ δ.ker) (z : G) (hz : δ z ≠ 1) :
23     ∀ n : ℤ, z ^ n ∈ J → n = 0 := by
24   intro n hn
25   have he : δ (z ^ n) = 1 := hJ hn
26   have he' : n * (δ z).toAdd = 0 := by
27     have h := congrArg Multiplicative.toAdd he
28     simpa [map_zpow, toAdd_zpow, zsmul_eq_mul] using h
29   exact (mul_eq_zero.mp he').resolve_right fun h => hz (congrArg Multiplicative.ofAdd h)
30 
31 /-- Normal forms map to the original ambient group. -/
32 def normalFormHom (J : Subgroup G) (z : G) (hz : ∀ g : G, Commute z g) :
33     J × Multiplicative ℤ →* G where
34   toFun p := (p.1 : G) * z ^ p.2.toAdd
35   map_one' := by simp
36   map_mul' := by
37     rintro ⟨j, n⟩ ⟨j', n'⟩
38     change ((j : G) * j') * z ^ (n.toAdd + n'.toAdd) =
39       ((j : G) * z ^ n.toAdd) * ((j' : G) * z ^ n'.toAdd)
40     rw [zpow_add]
41     calc
42       _ = (j : G) * ((j' : G) * z ^ n.toAdd) * z ^ n'.toAdd := by simp [mul_assoc]
43       _ = _ := by rw [← ((hz j').zpow_left n.toAdd).eq]; simp [mul_assoc]
44 
45 @[simp] theorem normalFormHom_apply (J : Subgroup G) (z : G)
46     (hz : ∀ g : G, Commute z g) (j : J) (n : Multiplicative ℤ) :
47     normalFormHom J z hz (j, n) = (j : G) * z ^ n.toAdd := rfl
48 
49 /-- The genuine ambient subgroup generated by the normal forms. -/
50 def extendedSubgroup (J : Subgroup G) (z : G) (hz : ∀ g : G, Commute z g) : Subgroup G :=
51   (normalFormHom J z hz).range
52 
53 theorem le_extendedSubgroup (J : Subgroup G) (z : G)
54     (hz : ∀ g : G, Commute z g) : J ≤ extendedSubgroup J z hz := by
55   intro j hj
56   exact ⟨(⟨j, hj⟩, 1), by simp⟩
57 
58 theorem central_mem_extendedSubgroup (J : Subgroup G) (z : G)
59     (hz : ∀ g : G, Commute z g) : z ∈ extendedSubgroup J z hz := by
60   exact ⟨(1, Multiplicative.ofAdd 1), by simp⟩
61 
62 /-- The range is exactly the join of the original subgroup and the central cyclic subgroup. -/
63 theorem extendedSubgroup_eq_sup (J : Subgroup G) (z : G)
64     (hz : ∀ g : G, Commute z g) :
65     extendedSubgroup J z hz = J ⊔ Subgroup.zpowers z := by
66   apply le_antisymm
67   · rintro g ⟨⟨j, n⟩, rfl⟩
68     exact Subgroup.mul_mem _ ((show J ≤ J ⊔ Subgroup.zpowers z from le_sup_left) j.property)
69       ((show Subgroup.zpowers z ≤ J ⊔ Subgroup.zpowers z from le_sup_right)
70         (Subgroup.zpow_mem _ (Subgroup.mem_zpowers z) n.toAdd))
71   · exact sup_le (le_extendedSubgroup J z hz)
72       (Subgroup.zpowers_le.mpr (central_mem_extendedSubgroup J z hz))
73 
74 /-- Absence of nonzero powers in the original subgroup gives unique normal forms. -/
75 theorem normalFormHom_injective (J : Subgroup G) (z : G)
76     (hz : ∀ g : G, Commute z g)
77     (hfree : ∀ n : ℤ, z ^ n ∈ J → n = 0) :
78     Function.Injective (normalFormHom J z hz) := by
79   apply (injective_iff_map_eq_one _).mpr
80   rintro ⟨j, n⟩ h
81   have hp : z ^ n.toAdd = (j : G)⁻¹ := by
82     have he := congrArg (fun a : G => (j : G)⁻¹ * a) h
83     simpa [normalFormHom, mul_assoc] using he
84   have hn : n.toAdd = 0 := hfree _ (hp ▸ J.inv_mem j.property)
85   have hn' : n = 1 := congrArg Multiplicative.ofAdd hn
86   subst n
87   have hj : j = 1 := Subtype.ext (by simpa using h)
88   simp [hj]
89 
90 /-- Explicit multiplicative coordinates for an actual subgroup of `G`. -/
91 def normalFormEquiv (J : Subgroup G) (z : G)
92     (hz : ∀ g : G, Commute z g)
93     (hfree : ∀ n : ℤ, z ^ n ∈ J → n = 0) :
94     J × Multiplicative ℤ ≃* extendedSubgroup J z hz :=
95   MonoidHom.ofInjective (normalFormHom_injective J z hz hfree)
96 
97 @[simp] theorem normalFormEquiv_coe (J : Subgroup G) (z : G)
98     (hz : ∀ g : G, Commute z g)
99     (hfree : ∀ n : ℤ, z ^ n ∈ J → n = 0) (p : J × Multiplicative ℤ) :
100     ((normalFormEquiv J z hz hfree p : extendedSubgroup J z hz) : G) =
101       (p.1 : G) * z ^ p.2.toAdd := rfl
102 
103 /-- The canonical inclusion of the original inducing subgroup. -/
104 def subgroupInclusion (J : Subgroup G) (z : G)
105     (hz : ∀ g : G, Commute z g) : J →* extendedSubgroup J z hz :=
106   Subgroup.inclusion (le_extendedSubgroup J z hz)
107 
108 /-- The adjoined element, viewed inside the enlarged subgroup. -/
109 def centralElement (J : Subgroup G) (z : G)
110     (hz : ∀ g : G, Commute z g) : extendedSubgroup J z hz :=
111   ⟨z, central_mem_extendedSubgroup J z hz⟩
112 
113 variable {k V : Type*} [Field k] [AddCommGroup V] [Module k V]
114 
115 /-- The prescribed scalar is a unit, so all integer powers act invertibly. -/
116 def productRepresentation (J : Subgroup G) (σ : Representation k J V) (c : kˣ) :
117     Representation k (J × Multiplicative ℤ) V where
118   toFun p := ((c ^ p.2.toAdd : kˣ) : k) • σ p.1
119   map_one' := by simp
120   map_mul' := by
121     rintro ⟨j, n⟩ ⟨j', n'⟩
122     ext v
123     simp [zpow_add, map_mul, Module.End.mul_apply, mul_smul]
124     exact smul_comm _ _ _
125 
126 /-- Extend the action to the literal subgroup `J ⊔ zpowers z` using unique normal forms. -/
127 def extendedRepresentation (J : Subgroup G) (z : G)
128     (hz : ∀ g : G, Commute z g)
129     (hfree : ∀ n : ℤ, z ^ n ∈ J → n = 0)
130     (σ : Representation k J V) (c : kˣ) :
131     Representation k (extendedSubgroup J z hz) V :=
132   (productRepresentation J σ c).comp (normalFormEquiv J z hz hfree).symm.toMonoidHom
133 
134 /-- The extension has the expected formula on every normal form. -/
135 @[simp] theorem extendedRepresentation_normalForm (J : Subgroup G) (z : G)
136     (hz : ∀ g : G, Commute z g)
137     (hfree : ∀ n : ℤ, z ^ n ∈ J → n = 0)
138     (σ : Representation k J V) (c : kˣ) (j : J) (n : Multiplicative ℤ) :
139     extendedRepresentation J z hz hfree σ c (normalFormEquiv J z hz hfree (j, n)) =
140       ((c ^ n.toAdd : kˣ) : k) • σ j := by
141   simp [extendedRepresentation, productRepresentation]
142 
143 @[simp] theorem extendedRepresentation_restrict (J : Subgroup G) (z : G)
144     (hz : ∀ g : G, Commute z g)
145     (hfree : ∀ n : ℤ, z ^ n ∈ J → n = 0)
146     (σ : Representation k J V) (c : kˣ) (j : J) :
147     extendedRepresentation J z hz hfree σ c (subgroupInclusion J z hz j) = σ j := by
148   have he : subgroupInclusion J z hz j = normalFormEquiv J z hz hfree (j, 1) :=
149     Subtype.ext (by simp [subgroupInclusion])
150   rw [he, extendedRepresentation_normalForm]
151   simp
152 
153 @[simp] theorem extendedRepresentation_central (J : Subgroup G) (z : G)
154     (hz : ∀ g : G, Commute z g)
155     (hfree : ∀ n : ℤ, z ^ n ∈ J → n = 0)
156     (σ : Representation k J V) (c : kˣ) :
157     extendedRepresentation J z hz hfree σ c (centralElement J z hz) =
158       (c : k) • (LinearMap.id : Module.End k V) := by
159   have he : centralElement J z hz =
160       normalFormEquiv J z hz hfree (1, Multiplicative.ofAdd 1) :=
161     Subtype.ext (by simp [centralElement])
162   rw [he, extendedRepresentation_normalForm]
163   simp
164   rfl
165 
166 /-- Irreducibility is inherited from the given action on the original subgroup. -/
167 theorem extendedRepresentation_irreducible (J : Subgroup G) (z : G)
168     (hz : ∀ g : G, Commute z g)
169     (hfree : ∀ n : ℤ, z ^ n ∈ J → n = 0)
170     (σ : Representation k J V) (c : kˣ) [Representation.IsIrreducible σ] :
171     Representation.IsIrreducible (extendedRepresentation J z hz hfree σ c) := by
172   let : Nontrivial V := GeneratedIrreducibility.nontrivial_space σ
173   apply RepresentationStability.irreducible_of_stable
174   intro S hS
175   apply RepresentationStability.eq_bot_or_top σ S
176   intro j v hv
177   simpa using hS (subgroupInclusion J z hz j) v hv
178 
179 section Topology
180 variable [TopologicalSpace G] [IsTopologicalGroup G]
181 
182 /-- Adjoining the central direction preserves openness of the inducing subgroup. -/
183 theorem extendedSubgroup_isOpen (J : Subgroup G) (z : G)
184     (hz : ∀ g : G, Commute z g) (hJ : IsOpen (J : Set G)) :
185     IsOpen (extendedSubgroup J z hz : Set G) :=
186   Subgroup.isOpen_mono (le_extendedSubgroup J z hz) hJ
187 
188 /-- Smoothness transfers because every extended stabilizer contains an open original stabilizer. -/
189 theorem extendedRepresentation_smooth (J : Subgroup G) (z : G)
190     (hz : ∀ g : G, Commute z g)
191     (hfree : ∀ n : ℤ, z ^ n ∈ J → n = 0)
192     (σ : Representation k J V) (c : kˣ)
193     (hJ : IsOpen (J : Set G)) (hσ : SmoothDegreeQuotient.IsSmooth σ) :
194     SmoothDegreeQuotient.IsSmooth (extendedRepresentation J z hz hfree σ c) := by
195   intro v
196   let K := (SmoothDegreeQuotient.vectorStabilizer σ v).map J.subtype
197   have hK : IsOpen (K : Set G) := hJ.isOpenMap_subtype_val _ (hσ v)
198   apply Subgroup.isOpen_mono (H₁ := K.subgroupOf (extendedSubgroup J z hz)) ?_
199     ((extendedSubgroup J z hz).subgroupOf_isOpen K hK)
200   intro x hx
201   obtain ⟨j, hj, he⟩ := hx
202   have hxe : x = subgroupInclusion J z hz j := Subtype.ext he.symm
203   change extendedRepresentation J z hz hfree σ c x v = v
204   rw [hxe, extendedRepresentation_restrict]
205   exact hj
206 
207 end Topology
208 end PaperXI.CentralExtensionInducing

Back to source controls