Yamaguchi Lean 4 Library
Source: ProCGroups.FiniteStepSolvableQuotients.Commutators.ClosureFromFiniteQuotients
ProCGroups/FiniteStepSolvableQuotients/Commutators/ClosureFromFiniteQuotients/Source

Source: ProCGroups.FiniteStepSolvableQuotients.Commutators.ClosureFromFiniteQuotients

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