ProCGroups/FiniteStepSolvableQuotients/Commutators/ClosureFromFiniteQuotients.lean
1import ProCGroups.FiniteStepSolvableQuotients.Commutators.Basic
2import ProCGroups.Generation.WordProductsAndClosure
3import ProCGroups.ProC.OpenNormalSubgroups.Separation
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/FiniteStepSolvableQuotients/Commutators/ClosureFromFiniteQuotients.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 Pointwise
21namespace ProCGroups.FiniteStepSolvableQuotients
23universe u
25/-- Every element of the commutator subgroup is a product of at most `n` commutators. -/
27 {G : Type u} [Group G] (n : ℕ) : Prop :=
28 ∀ g ∈ commutator G, IsProductOfCommutatorsLE n g
30/-- A product of at most `m` commutators is also a product of at most any larger bound `n`. -/
31theorem HasCommutatorWidthAtMost.mono
32 {G : Type u} [Group G]
33 {m n : ℕ}
34 (h : HasCommutatorWidthAtMost (G := G) m)
35 (hmn : m ≤ n) :
36 HasCommutatorWidthAtMost (G := G) n := by
37 intro g hg
38 rcases h g hg with ⟨l, hl, rfl⟩
39 exact ⟨l, le_trans hl hmn, rfl⟩
41/-- Products of boundedly many commutators lie in the bounded word-product set generated by
42individual commutators. -/
44 {G : Type u} [Group G] {n : ℕ} {g : G}
45 (hg : IsProductOfCommutatorsLE n g) :
46 g ∈ ProCGroups.Generation.wordProducts (commutatorSet G) n := by
47 rcases hg with ⟨l, hl, hprod⟩
48 have hlenAux :
49 ∀ l : List (G × G),
50 (l.map fun p : G × G => ⁅p.1, p.2⁆).prod ∈
51 ProCGroups.Generation.wordProducts (commutatorSet G) l.length := by
52 intro l
53 induction l with
54 | nil =>
55 simp only [List.length_nil, Generation.wordProducts, List.map_nil, List.prod_nil, Set.mem_singleton_iff]
56 | cons a t ih =>
57 have hhead :
58 ⁅a.1, a.2⁆ ∈ ProCGroups.Generation.wordProducts (commutatorSet G) 1 := by
59 simpa [ProCGroups.Generation.wordProducts_one] using
60 (commutator_mem_commutatorSet (g₁ := a.1) (g₂ := a.2))
61 have hmul :
62 ⁅a.1, a.2⁆ * (t.map fun p : G × G => ⁅p.1, p.2⁆).prod ∈
63 ProCGroups.Generation.wordProducts (commutatorSet G) 1 *
64 ProCGroups.Generation.wordProducts (commutatorSet G) t.length := by
65 exact ⟨⁅a.1, a.2⁆, hhead,
66 (t.map fun p : G × G => ⁅p.1, p.2⁆).prod, ih, rfl⟩
67 have hEq :
68 ProCGroups.Generation.wordProducts (commutatorSet G) 1 *
69 ProCGroups.Generation.wordProducts (commutatorSet G) t.length =
70 ProCGroups.Generation.wordProducts (commutatorSet G) (1 + t.length) := by
71 simpa using
72 (ProCGroups.Generation.wordProducts_mul_wordProducts (G := G) (commutatorSet G)
73 1 t.length)
74 have hmem' :
75 ⁅a.1, a.2⁆ * (t.map fun p : G × G => ⁅p.1, p.2⁆).prod ∈
76 ProCGroups.Generation.wordProducts (commutatorSet G) (1 + t.length) := by
77 rw [← hEq]
78 simpa [ProCGroups.Generation.wordProducts_one] using hmul
79 simpa [Nat.add_comm] using hmem'
80 have hlen :
81 (l.map fun p : G × G => ⁅p.1, p.2⁆).prod ∈
82 ProCGroups.Generation.wordProducts (commutatorSet G) l.length :=
83 hlenAux l
85 (G := G) (X := commutatorSet G) (one_mem_commutatorSet G) hl (by simpa [hprod] using hlen)
87/-- Lift a bounded product of commutators in a quotient to a bounded word product of commutators
88upstairs. -/
90 {G : Type u} [Group G] {N : Subgroup G} [N.Normal] {n : ℕ} {x : G ⧸ N}
91 (hx : IsProductOfCommutatorsLE n x) :
92 ∃ y ∈ ProCGroups.Generation.wordProducts (commutatorSet G) n,
93 QuotientGroup.mk' N y = x := by
94 classical
95 rcases hx with ⟨l, hl, hprod⟩
96 let q : G →* G ⧸ N := QuotientGroup.mk' N
97 let lift : G ⧸ N → G := fun z => Classical.choose (QuotientGroup.mk'_surjective N z)
98 have hlift : ∀ z : G ⧸ N, q (lift z) = z := fun z =>
99 Classical.choose_spec (QuotientGroup.mk'_surjective N z)
100 let L : List (G × G) := l.map fun p => (lift p.1, lift p.2)
101 let y : G := (L.map fun p : G × G => ⁅p.1, p.2⁆).prod
102 have hyword : y ∈ ProCGroups.Generation.wordProducts (commutatorSet G) n := by
104 (G := G) (n := n) (g := y) ?_
105 exact ⟨L, by simpa [L] using hl, rfl⟩
106 have hmapList :
107 ∀ l : List ((G ⧸ N) × (G ⧸ N)),
108 q ((l.map fun p => ⁅lift p.1, lift p.2⁆).prod) =
109 (l.map fun p => ⁅p.1, p.2⁆).prod := by
110 intro l
111 induction l with
112 | nil =>
113 simp only [List.map_nil, List.prod_nil, QuotientGroup.mk'_apply, QuotientGroup.mk_one, q]
114 | cons a t ih =>
116 have hmap :
117 q y = (l.map fun p : (G ⧸ N) × (G ⧸ N) => ⁅p.1, p.2⁆).prod := by
118 simpa [y, L, List.map_map] using hmapList l
119 exact ⟨y, hyword, hmap.trans hprod⟩
121/-- A uniform finite-quotient commutator-width bound forces the commutator subgroup of a
122profinite group to be closed. -/
124 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
125 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
126 (n : ℕ)
127 (hwidth :
128 ∀ U : OpenNormalSubgroup G,
129 HasCommutatorWidthAtMost (G := G ⧸ (U : Subgroup G)) n) :
130 IsClosed ((commutator G : Subgroup G) : Set G) := by
131 let X : Set G := commutatorSet G
132 let S : Set G := ProCGroups.Generation.wordProducts X n
133 have hXclosed : IsClosed X := by
134 simpa [X] using isClosed_commutatorSet (G := G)
135 have hSclosed : IsClosed S := by
136 simpa [S] using
137 (ProCGroups.Generation.wordProducts_isClosed (G := G) (X := X) hXclosed n)
138 have hSsubset :
139 S ⊆ ((commutator G : Subgroup G) : Set G) := by
140 intro x hx
141 have hxcl :
142 x ∈ ((Subgroup.closure X : Subgroup G) : Set G) :=
143 ProCGroups.Generation.wordProducts_subset_closure (G := G) X n hx
144 simpa [X, commutator_eq_closure] using hxcl
145 have hclosure_subset :
146 closure (((commutator G : Subgroup G) : Set G)) ⊆ S := by
147 intro x hxcl
148 let hG : IsProfiniteGroup G := ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
149 refine (IsProfiniteGroup.mem_closed_iff_forall_openNormal_quotient
150 (G := G) hG (S := S) hSclosed).2 ?_
151 intro U
152 let Q : Type u := G ⧸ (U : Subgroup G)
153 let q : G →* Q := QuotientGroup.mk' (U : Subgroup G)
154 have hpreClosed :
155 IsClosed (q ⁻¹' (((commutator Q : Subgroup Q) : Set Q))) := by
156 letI : DiscreteTopology Q :=
157 QuotientGroup.discreteTopology (ProCGroups.openNormalSubgroup_isOpen (G := G) U)
158 exact (isClosed_discrete _).preimage QuotientGroup.continuous_mk
159 have hcomm_pre :
160 ((commutator G : Subgroup G) : Set G) ⊆
161 q ⁻¹' (((commutator Q : Subgroup Q) : Set Q)) := by
162 intro y hy
163 have hle : commutator G ≤ (commutator Q).comap q := by
164 rw [commutator_eq_closure]
165 refine (Subgroup.closure_le (K := (commutator Q).comap q)).2 ?_
166 intro z hz
167 rcases mem_commutatorSet_iff.mp hz with ⟨a, b, rfl⟩
168 change q ⁅a, b⁆ ∈ commutator Q
169 rw [map_commutatorElement]
170 rw [commutator_eq_closure]
171 exact Subgroup.subset_closure
172 (commutator_mem_commutatorSet (g₁ := q a) (g₂ := q b))
173 exact hle hy
174 have hxq : q x ∈ commutator Q :=
175 (closure_minimal hcomm_pre hpreClosed) hxcl
177 (G := G) (N := (U : Subgroup G)) (n := n) (x := q x)
178 (hwidth U (q x) hxq) with
179 ⟨y, hyS, hyq⟩
180 exact ⟨y, hyS, hyq⟩
181 have hclosure_subset_comm :
182 closure (((commutator G : Subgroup G) : Set G)) ⊆
183 ((commutator G : Subgroup G) : Set G) := fun x hx => hSsubset (hclosure_subset hx)
184 exact closure_eq_iff_isClosed.mp (subset_antisymm hclosure_subset_comm subset_closure)
186end ProCGroups.FiniteStepSolvableQuotients