ProCGroups/FiniteStepSolvableQuotients/Abelianization.lean
1import ProCGroups.Abelian.TopologicalAbelianizationFunctoriality
2import ProCGroups.FiniteStepSolvableQuotients.Commutators.Basic
3import ProCGroups.ProC.Kernels
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/FiniteStepSolvableQuotients/Abelianization.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
16Develops topological derived series, maximal solvable quotients of bounded derived length, commutator closure formulas, and abelian-action consequences.
17-/
19open scoped Topology
21namespace ProCGroups.FiniteStepSolvableQuotients
23open ProCGroups.Abelian
25universe u
27/-- Every open subgroup has torsion-free topological abelianization. -/
29 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Prop :=
30 ∀ H : OpenSubgroup G, IsMulTorsionFree (TopologicalAbelianization ↥(H : Subgroup G))
32/-- The last nontrivial closed derived term inside the maximal `m`-step solvable quotient. -/
34 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
35 (m : ℕ) : Subgroup (MaxSolvQuot G m) :=
36 topDerivedTop (MaxSolvQuot G m) (m - 1)
38/-- An open subgroup of the maximal `m`-step solvable quotient contains the last derived term. -/
40 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
41 (m : ℕ) (H : OpenSubgroup (MaxSolvQuot G m)) : Prop :=
42 lastDerivedSubgroup (G := G) m ≤ (H : Subgroup (MaxSolvQuot G m))
44/-- An open normal subgroup inside an open subgroup of the maximal `m`-step solvable quotient
45contains the last derived term. -/
47 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
48 (m : ℕ)
49 (H : OpenSubgroup (MaxSolvQuot G m))
50 (N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m))) : Prop :=
51 ∀ x : MaxSolvQuot G m, x ∈ lastDerivedSubgroup (G := G) m →
52 ∃ hxH : x ∈ H, (⟨x, hxH⟩ : H) ∈ N
54/-- `containsLastDerived` is the intrinsic form of saying that the ambient image of `N`
55contains the last derived subgroup. -/
57 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
58 (m : ℕ)
59 (H : OpenSubgroup (MaxSolvQuot G m))
60 (N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m))) :
61 containsLastDerived (G := G) m H N ↔
62 lastDerivedSubgroup (G := G) m ≤
63 (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m))).map
64 ((H : Subgroup (MaxSolvQuot G m)).subtype) := by
65 constructor
66 · intro h x hx
67 rcases h x hx with ⟨hxH, hxN⟩
68 exact ⟨⟨x, hxH⟩, hxN, rfl⟩
69 · intro h x hx
70 rcases h hx with ⟨y, hyN, hyx⟩
71 refine ⟨by simp only [← hyx, Subgroup.subtype_apply, SetLike.coe_mem], ?_⟩
72 have hy : (⟨x, by simp only [← hyx, Subgroup.subtype_apply, y.2]⟩ :
73 ↥(H : Subgroup (MaxSolvQuot G m))) = y := by
74 exact Subtype.ext hyx.symm
75 simpa [hy] using hyN
77/-- Ambient image containment form of `containsLastDerived`. -/
79 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
80 {m : ℕ}
81 {H : OpenSubgroup (MaxSolvQuot G m)}
82 {N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m))}
83 (hN :
84 lastDerivedSubgroup (G := G) m ≤
85 (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m))).map
86 ((H : Subgroup (MaxSolvQuot G m)).subtype)) :
87 containsLastDerived (G := G) m H N :=
89 (G := G) m H N).2 hN
92/-- If every open subgroup has torsion-free topological abelianization, then so does the ambient
93group. -/
95 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
96 (hG : IsAbTorsionFree G) :
97 IsMulTorsionFree (TopologicalAbelianization G) := by
98 let e := topologicalAbelianizationTopMulEquiv (G := G)
99 letI :
100 IsMulTorsionFree (TopologicalAbelianization ↥((⊤ : OpenSubgroup G) : Subgroup G)) := hG ⊤
101 exact e.isMulTorsionFree
103/-- For a commutative `T1` topological group, torsion-freeness of open-subgroup abelianizations
104implies torsion-freeness of the group itself. -/
106 {G : Type u} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G]
107 (hG : IsAbTorsionFree G) :
108 IsMulTorsionFree G := by
109 letI : IsMulTorsionFree (TopologicalAbelianization G) :=
111 exact (TopologicalAbelianization.continuousMulEquivOfCommGroup G).isMulTorsionFree
113/-- Trivial closed commutator subgroup makes the natural map to topological abelianization
114injective. -/
116 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
117 (hcomm : topologicalCommutator G = ⊥) :
118 Function.Injective (TopologicalAbelianization.mk G) := by
119 rw [← MonoidHom.ker_eq_bot_iff, TopologicalAbelianization.ker_mk]
120 simpa [topologicalCommutator] using hcomm
122/-- Trivial first closed derived subgroup makes the natural map to topological abelianization
123injective. -/
125 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
126 (hder : topDerivedTop G 1 = ⊥) :
127 Function.Injective (TopologicalAbelianization.mk G) :=
129 simpa using hder
131/-- If the first closed derived subgroup of a closed subgroup vanishes in the ambient group, then
132the subgroup has trivial first closed derived subgroup internally as well. -/
134 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
135 {K : Subgroup Q} (hKClosed : IsClosed (K : Set Q))
136 (hstep : closedDerivedSeries (G := Q) K 1 = ⊥) :
137 topDerivedTop K 1 = ⊥ := by
138 have hmapTop : (⊤ : Subgroup K).map K.subtype = K := by
139 ext x
140 constructor
141 · rintro ⟨y, -, rfl⟩
142 exact y.2
143 · intro hx
144 exact ⟨⟨x, hx⟩, by simp only [Subgroup.coe_top, Set.mem_univ], rfl⟩
145 have hmap :
146 (topDerivedTop K 1).map K.subtype = closedDerivedSeries (G := Q) K 1 := by
147 calc
148 (topDerivedTop K 1).map K.subtype =
149 closedDerivedSeries (G := Q) ((⊤ : Subgroup K).map K.subtype) 1 := by
150 simpa [topDerivedTop] using
152 (G := Q) (H := K) (K := (⊤ : Subgroup K)) hKClosed)
153 _ = closedDerivedSeries (G := Q) K 1 := by simp only [hmapTop, closedDerivedSeries_succ, closedDerivedSeries_zero]
154 have hstep' : closedCommutator K K = ⊥ := by
155 simpa [closedDerivedSeries] using hstep
156 have hmapbot : (topDerivedTop K 1).map K.subtype = ⊥ := by
157 simpa [hstep'] using hmap
158 exact
159 (Subgroup.map_eq_bot_iff_of_injective
160 (H := topDerivedTop K 1)
161 (f := K.subtype)
162 (by
163 intro x y hxy
164 exact Subtype.ext hxy)).1 hmapbot
166/-- The kernel of the canonical topological abelianization map is the first closed derived
167subgroup. -/
169 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
171 (TopologicalAbelianization.mkₜ G) =
172 topDerivedTop G 1 := by
173 ext y
174 change TopologicalAbelianization.mk G y = 1 ↔ y ∈ topDerivedTop G 1
175 rw [TopologicalAbelianization.mk_eq_one_iff]
177 closedCommutator, topDerivedTop, closedDerivedSeries]
179/-- Mapping the first closed derived subgroup of the topological abelianization kernel back into
180the ambient group gives the second closed derived subgroup. -/
181theorem topologicalAbelianization_kernel_closedDerivedSeries_one_map_subtype_eq_topDerivedTop_two
182 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
183 let N : Subgroup G :=
184 ProCGroups.ProC.ProfiniteKernelSubgroup (TopologicalAbelianization.mkₜ G)
185 (closedDerivedSeries (G := N) (⊤ : Subgroup N) 1).map N.subtype =
186 topDerivedTop G 2 := by
187 let N : Subgroup G :=
188 ProCGroups.ProC.ProfiniteKernelSubgroup (TopologicalAbelianization.mkₜ G)
189 have hN_eq : N = topDerivedTop G 1 :=
191 have hNmap : (⊤ : Subgroup N).map N.subtype = topDerivedTop G 1 := by
192 ext y
193 constructor
194 · rintro ⟨z, -, rfl⟩
195 change (z : G) ∈ topDerivedTop G 1
196 exact hN_eq ▸ z.2
197 · intro hy
198 refine ⟨⟨y, hN_eq.symm ▸ hy⟩, by simp only [Subgroup.coe_top, Set.mem_univ], rfl⟩
199 have hmap :
200 (closedDerivedSeries (G := N) (⊤ : Subgroup N) 1).map N.subtype =
201 closedDerivedSeries (G := G) ((⊤ : Subgroup N).map N.subtype) 1 := by
202 exact
204 (G := G) (H := N) (K := (⊤ : Subgroup N))
205 (by
206 simpa [N] using
208 (TopologicalAbelianization.mkₜ G))
209 calc
210 (closedDerivedSeries (G := N) (⊤ : Subgroup N) 1).map N.subtype =
211 closedDerivedSeries (G := G) ((⊤ : Subgroup N).map N.subtype) 1 := hmap
212 _ = closedDerivedSeries (G := G) (topDerivedTop G 1) 1 := by rw [hNmap]
213 _ = topDerivedTop G 2 := by
214 change closedDerivedSeries (G := G) (topDerivedTop G 1) 1 = topDerivedTop G (1 + 1)
215 exact topDerived_add (G := G) (m := 1) (n := 1)
217/-- Membership in the second closed derived subgroup is equivalent to membership in the closed
218commutator of the canonical topological abelianization kernel. -/
220 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
221 {a : G}
222 (haψ : TopologicalAbelianization.mkₜ G a = 1) :
223 a ∈ topDerivedTop G 2 ↔
224 (⟨a, haψ⟩ : ProCGroups.ProC.ProfiniteKernelSubgroup
225 (TopologicalAbelianization.mkₜ G)) ∈
228 (TopologicalAbelianization.mkₜ G)) := by
229 let N : Subgroup G :=
230 ProCGroups.ProC.ProfiniteKernelSubgroup (TopologicalAbelianization.mkₜ G)
231 have hmap :
232 (closedDerivedSeries (G := N) (⊤ : Subgroup N) 1).map N.subtype =
233 topDerivedTop G 2 :=
235 have hclosed :
236 closedDerivedSeries (G := N) (⊤ : Subgroup N) 1 =
239 constructor
240 · intro ha
241 have ha_map :
242 a ∈ (closedDerivedSeries (G := N) (⊤ : Subgroup N) 1).map N.subtype := by
243 rwa [hmap]
244 rcases ha_map with ⟨z, hz, hza⟩
245 have hz_eq : z = (⟨a, haψ⟩ : N) := by
246 apply Subtype.ext
247 simpa using hza
248 rw [hclosed] at hz
249 simpa only [hz_eq] using hz
250 · intro ha
251 have ha_map :
252 a ∈ (closedDerivedSeries (G := N) (⊤ : Subgroup N) 1).map N.subtype := by
253 refine ⟨(⟨a, haψ⟩ : N), ?_, rfl⟩
254 rw [hclosed]
255 exact ha
256 rwa [hmap] at ha_map
258end ProCGroups.FiniteStepSolvableQuotients