Yamaguchi Lean 4 Library
Source: ProCGroups.FiniteStepSolvableQuotients.Abelianization
ProCGroups/FiniteStepSolvableQuotients/Abelianization/Source

Source: ProCGroups.FiniteStepSolvableQuotients.Abelianization

1import ProCGroups.Abelian.TopologicalAbelianizationFunctoriality
2import ProCGroups.FiniteStepSolvableQuotients.Commutators.Basic
3import ProCGroups.ProC.Kernels
5/-!
6# Abelianizations inside finite-step solvable quotients
8This module studies the last closed-derived subgroup of a maximal solvable quotient and formulates
9torsion-freeness and containment conditions using abelianizations of its open subgroups.
10-/
12open scoped Topology
14namespace ProCGroups.FiniteStepSolvableQuotients
16open ProCGroups.Abelian
18universe u
20/-- Every open subgroup has torsion-free topological abelianization. -/
21def IsAbTorsionFree
22 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Prop :=
23 ∀ H : OpenSubgroup G, IsMulTorsionFree (TopologicalAbelianization ↥(H : Subgroup G))
25/-- The last nontrivial closed derived term inside the maximal \(m\)-step solvable quotient. -/
26def lastDerivedSubgroup
27 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
28 (m : ℕ) : Subgroup (MaxSolvQuot G m) :=
29 topDerivedTop (MaxSolvQuot G m) (m - 1)
31/-- An open subgroup of the maximal \(m\)-step solvable quotient contains the last derived term. -/
32def aboveLastDerived
33 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
34 (m : ℕ) (H : OpenSubgroup (MaxSolvQuot G m)) : Prop :=
35 lastDerivedSubgroup (G := G) m ≤ (H : Subgroup (MaxSolvQuot G m))
37/--
38An open normal subgroup inside an open subgroup of the maximal \(m\)-step solvable quotient
39contains the last derived term.
40-/
41def containsLastDerived
42 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
43 (m : ℕ)
44 (H : OpenSubgroup (MaxSolvQuot G m))
45 (N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m))) : Prop :=
46 ∀ x : MaxSolvQuot G m, x ∈ lastDerivedSubgroup (G := G) m →
47 ∃ hxH : x ∈ H, (⟨x, hxH⟩ : H) ∈ N
49/--
50\(\mathrm{ContainsLastDerived}\) is the intrinsic form of saying that the ambient image of \(N\)
51contains the last derived subgroup.
52-/
53theorem containsLastDerived_iff_lastDerivedSubgroup_le_map_subtype
54 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
55 {m : ℕ}
56 {H : OpenSubgroup (MaxSolvQuot G m)}
57 {N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m))} :
58 containsLastDerived (G := G) m H N ↔
59 lastDerivedSubgroup (G := G) m ≤
60 (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m))).map
61 ((H : Subgroup (MaxSolvQuot G m)).subtype) := by
62 constructor
63 · intro h x hx
64 rcases h x hx with ⟨hxH, hxN⟩
65 exact ⟨⟨x, hxH⟩, hxN, rfl⟩
66 · intro h x hx
67 rcases h hx with ⟨y, hyN, hyx⟩
68 refine ⟨by simp only [← hyx, Subgroup.subtype_apply, SetLike.coe_mem], ?_⟩
69 have hy : (⟨x, by simp only [← hyx, Subgroup.subtype_apply, y.2]⟩ :
70 ↥(H : Subgroup (MaxSolvQuot G m))) = y := by
71 exact Subtype.ext hyx.symm
72 change
73 (⟨x, by simp only [← hyx, Subgroup.subtype_apply, y.2]⟩ :
74 ↥(H : Subgroup (MaxSolvQuot G m))) ∈
75 (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m)))
76 rw [hy]
77 exact hyN
79/--
80The quotient contains the last derived subgroup under the stated map-subtype containment
81hypothesis.
82-/
83theorem containsLastDerived_of_lastDerivedSubgroup_le_map_subtype
84 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
85 {m : ℕ}
86 {H : OpenSubgroup (MaxSolvQuot G m)}
87 {N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m))}
88 (hN :
89 lastDerivedSubgroup (G := G) m ≤
90 (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m))).map
91 ((H : Subgroup (MaxSolvQuot G m)).subtype)) :
92 containsLastDerived (G := G) m H N :=
93 (containsLastDerived_iff_lastDerivedSubgroup_le_map_subtype
94 (G := G) (m := m) (H := H) (N := N)).2 hN
97/--
98If every open subgroup has torsion-free topological abelianization, then so does the ambient
99group.
100-/
101theorem isMulTorsionFree_topologicalAbelianization_of_isAbTorsionFree
102 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
103 (hG : IsAbTorsionFree G) :
104 IsMulTorsionFree (TopologicalAbelianization G) := by
105 let e := topologicalAbelianizationTopMulEquiv (G := G)
106 letI :
107 IsMulTorsionFree (TopologicalAbelianization ↥((⊤ : OpenSubgroup G) : Subgroup G)) := hG ⊤
108 exact e.isMulTorsionFree
110/--
111For a commutative \(T_1\) topological group, torsion-freeness of open-subgroup abelianizations
112implies torsion-freeness of the group itself.
113-/
114theorem isMulTorsionFree_of_isAbTorsionFree_commGroup
115 {G : Type u} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G]
116 (hG : IsAbTorsionFree G) :
117 IsMulTorsionFree G := by
118 letI : IsMulTorsionFree (TopologicalAbelianization G) :=
119 isMulTorsionFree_topologicalAbelianization_of_isAbTorsionFree (G := G) hG
120 exact (TopologicalAbelianization.continuousMulEquivOfCommGroup G).isMulTorsionFree
122/--
123Trivial closed commutator subgroup makes the natural map to topological abelianization
124injective.
125-/
126theorem injective_topologicalAbelianizationMk_of_topologicalCommutator_eq_bot
127 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
128 (hcomm : topologicalCommutator G = ⊥) :
129 Function.Injective (TopologicalAbelianization.mk G) := by
130 rw [← MonoidHom.ker_eq_bot_iff, TopologicalAbelianization.ker_mk]
131 simpa [topologicalCommutator] using hcomm
133/--
134Trivial first closed derived subgroup makes the natural map to topological abelianization
135injective.
136-/
137theorem injective_topologicalAbelianizationMk_of_topDerivedTop_one_eq_bot
138 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
139 (hder : topDerivedTop G 1 = ⊥) :
140 Function.Injective (TopologicalAbelianization.mk G) :=
141 injective_topologicalAbelianizationMk_of_topologicalCommutator_eq_bot (G := G) <| by
142 simpa using hder
144/--
145If the first closed derived subgroup of a closed subgroup vanishes in the ambient group, then
146the subgroup has trivial first closed derived subgroup internally as well.
147-/
148theorem topDerivedTop_one_eq_bot_of_closedDerivedSeries_eq_bot
149 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
150 {K : Subgroup Q} (hKClosed : IsClosed (K : Set Q))
151 (hstep : closedDerivedSeries (G := Q) K 1 = ⊥) :
152 topDerivedTop K 1 = ⊥ := by
153 have hmapTop : (⊤ : Subgroup K).map K.subtype = K := by
154 ext x
155 constructor
156 · rintro ⟨y, -, rfl⟩
157 exact y.2
158 · intro hx
159 exact ⟨⟨x, hx⟩, by simp only [Subgroup.coe_top, Set.mem_univ], rfl⟩
160 have hmap :
161 (topDerivedTop K 1).map K.subtype = closedDerivedSeries (G := Q) K 1 := by
162 calc
163 (topDerivedTop K 1).map K.subtype =
164 closedDerivedSeries (G := Q) ((⊤ : Subgroup K).map K.subtype) 1 := by
165 simpa [topDerivedTop] using
166 (topDerived_one_map_subtype_eq_of_isClosed_subgroup
167 (G := Q) (H := K) (K := (⊤ : Subgroup K)) hKClosed)
168 _ = closedDerivedSeries (G := Q) K 1 := by simp only [hmapTop, closedDerivedSeries_succ,
169 closedDerivedSeries_zero]
170 have hstep' : closedCommutator K K = ⊥ := by
171 simpa [closedDerivedSeries] using hstep
172 have hmapbot : (topDerivedTop K 1).map K.subtype = ⊥ := by
173 simpa [hstep'] using hmap
174 exact
175 (Subgroup.map_eq_bot_iff_of_injective
176 (H := topDerivedTop K 1)
177 (f := K.subtype)
178 (by
179 intro x y hxy
180 exact Subtype.ext hxy)).1 hmapbot
182/--
183The kernel of the canonical topological abelianization map is the first closed derived subgroup.
184-/
185theorem topologicalAbelianization_profiniteKernelSubgroup_eq_topDerivedTop_one
186 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
188 (TopologicalAbelianization.mkₜ G) =
189 topDerivedTop G 1 := by
190 ext y
191 change TopologicalAbelianization.mk G y = 1 ↔ y ∈ topDerivedTop G 1
192 rw [TopologicalAbelianization.mk_eq_one_iff]
193 simp only [Subgroup.closedCommutator, topologicalCommutator_eq_closedCommutator_top_top,
194 closedCommutator, topDerivedTop, closedDerivedSeries]
196/--
197Mapping the first closed derived subgroup of the topological abelianization kernel back into the
198ambient group gives the second closed derived subgroup.
199-/
200theorem topologicalAbelianization_kernel_closedDerivedSeries_one_map_subtype_eq_topDerivedTop_two
201 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
202 let N : Subgroup G :=
203 ProCGroups.ProC.ProfiniteKernelSubgroup (TopologicalAbelianization.mkₜ G)
204 (closedDerivedSeries (G := N) (⊤ : Subgroup N) 1).map N.subtype =
205 topDerivedTop G 2 := by
206 let N : Subgroup G :=
207 ProCGroups.ProC.ProfiniteKernelSubgroup (TopologicalAbelianization.mkₜ G)
208 have hN_eq : N = topDerivedTop G 1 :=
209 topologicalAbelianization_profiniteKernelSubgroup_eq_topDerivedTop_one G
210 have hNmap : (⊤ : Subgroup N).map N.subtype = topDerivedTop G 1 := by
211 ext y
212 constructor
213 · rintro ⟨z, -, rfl⟩
214 change (z : G) ∈ topDerivedTop G 1
215 exact hN_eq ▸ z.2
216 · intro hy
217 refine ⟨⟨y, hN_eq.symm ▸ hy⟩, by simp only [Subgroup.coe_top, Set.mem_univ], rfl⟩
218 have hmap :
219 (closedDerivedSeries (G := N) (⊤ : Subgroup N) 1).map N.subtype =
220 closedDerivedSeries (G := G) ((⊤ : Subgroup N).map N.subtype) 1 := by
221 exact
222 topDerived_one_map_subtype_eq_of_isClosed_subgroup
223 (G := G) (H := N) (K := (⊤ : Subgroup N))
224 (by
225 simpa [N] using
227 (TopologicalAbelianization.mkₜ G))
228 calc
229 (closedDerivedSeries (G := N) (⊤ : Subgroup N) 1).map N.subtype =
230 closedDerivedSeries (G := G) ((⊤ : Subgroup N).map N.subtype) 1 := hmap
231 _ = closedDerivedSeries (G := G) (topDerivedTop G 1) 1 := by rw [hNmap]
232 _ = topDerivedTop G 2 := by
233 change closedDerivedSeries (G := G) (topDerivedTop G 1) 1 = topDerivedTop G (1 + 1)
234 exact topDerived_add (G := G) (m := 1) (n := 1)
236/--
237Membership in the second closed derived subgroup is equivalent to membership in the closed
238commutator of the canonical topological abelianization kernel.
239-/
240theorem mem_topDerivedTop_two_iff_mem_closedCommutator_topologicalAbelianizationKernel
241 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
242 {a : G}
243 (haψ : TopologicalAbelianization.mkₜ G a = 1) :
244 a ∈ topDerivedTop G 2 ↔
246 (TopologicalAbelianization.mkₜ G)) ∈
249 (TopologicalAbelianization.mkₜ G)) := by
250 let N : Subgroup G :=
251 ProCGroups.ProC.ProfiniteKernelSubgroup (TopologicalAbelianization.mkₜ G)
252 have hmap :
253 (closedDerivedSeries (G := N) (⊤ : Subgroup N) 1).map N.subtype =
254 topDerivedTop G 2 :=
255 topologicalAbelianization_kernel_closedDerivedSeries_one_map_subtype_eq_topDerivedTop_two G
256 have hclosed :
257 closedDerivedSeries (G := N) (⊤ : Subgroup N) 1 =
259 closedDerivedSeries_top_one_eq_closedCommutator N
260 constructor
261 · intro ha
262 have ha_map :
263 a ∈ (closedDerivedSeries (G := N) (⊤ : Subgroup N) 1).map N.subtype := by
264 rwa [hmap]
265 rcases ha_map with ⟨z, hz, hza⟩
266 have hz_eq : z = (⟨a, haψ⟩ : N) := by
267 apply Subtype.ext
268 simpa using hza
269 rw [hclosed] at hz
270 change (⟨a, haψ⟩ : N) ∈ Subgroup.closedCommutator N
271 rw [← hz_eq]
272 exact hz
273 · intro ha
274 have ha_map :
275 a ∈ (closedDerivedSeries (G := N) (⊤ : Subgroup N) 1).map N.subtype := by
276 refine ⟨(⟨a, haψ⟩ : N), ?_, rfl⟩
277 rw [hclosed]
278 change (⟨a, haψ⟩ : N) ∈ Subgroup.closedCommutator N at ha
279 exact ha
280 rwa [hmap] at ha_map
282end ProCGroups.FiniteStepSolvableQuotients