ProCGroups.FiniteStepSolvableQuotients.Commutators.ClosureFromFiniteQuotients
This module studies closure from finite quotients for pro cgroups. Every element of the commutator subgroup is a product of at most \(n\) commutators. A product of at most \(m\) commutators is also a product of at most any larger bound \(n\).
import
def HasCommutatorWidthAtMost
{G : Type u} [Group G] (n : ℕ) : Prop :=
∀ g ∈ commutator G, IsProductOfCommutatorsLE n gEvery element of the commutator subgroup is a product of at most \(n\) commutators.
theorem HasCommutatorWidthAtMost.mono
{G : Type u} [Group G]
{m n : ℕ}
(h : HasCommutatorWidthAtMost (G := G) m)
(hmn : m ≤ n) :
HasCommutatorWidthAtMost (G := G) nA product of at most \(m\) commutators is also a product of at most any larger bound \(n\).
Show proof
by
intro g hg
rcases h g hg with ⟨l, hl, rfl⟩
exact ⟨l, le_trans hl hmn, rfl⟩Proof. Work with the closed derived series and the maximal \(m\)-step solvable quotient. The quotient map kills exactly the relevant closed derived term, and statements about abelianization, torsion-freeness, faithful conjugation actions, centers, and centralizers are reduced to the induced maps on open subgroups and their topological abelianizations. Closure and functoriality are checked by monotonicity of closed commutators, compatibility of quotient maps, and passage to the corresponding quotient or open subgroup.
□theorem mem_wordProducts_commutatorSet_of_isProductOfCommutatorsLE
{G : Type u} [Group G] {n : ℕ} {g : G}
(hg : IsProductOfCommutatorsLE n g) :
g ∈ ProCGroups.Generation.wordProducts (commutatorSet G) nProducts of boundedly many commutators lie in the bounded word-product set generated by individual commutators.
Show proof
by
rcases hg with ⟨l, hl, hprod⟩
have hlenAux :
∀ l : List (G × G),
(l.map fun p : G × G => ⁅p.1, p.2⁆).prod ∈
ProCGroups.Generation.wordProducts (commutatorSet G) l.length := by
intro l
induction l with
| nil =>
simp only [List.length_nil, Generation.wordProducts, List.map_nil, List.prod_nil, Set.mem_singleton_iff]
| cons a t ih =>
have hhead :
⁅a.1, a.2⁆ ∈ ProCGroups.Generation.wordProducts (commutatorSet G) 1 := by
simpa [ProCGroups.Generation.wordProducts_one] using
(commutator_mem_commutatorSet (g₁ := a.1) (g₂ := a.2))
have hmul :
⁅a.1, a.2⁆ * (t.map fun p : G × G => ⁅p.1, p.2⁆).prod ∈
ProCGroups.Generation.wordProducts (commutatorSet G) 1 *
ProCGroups.Generation.wordProducts (commutatorSet G) t.length := by
exact ⟨⁅a.1, a.2⁆, hhead,
(t.map fun p : G × G => ⁅p.1, p.2⁆).prod, ih, rfl⟩
have hEq :
ProCGroups.Generation.wordProducts (commutatorSet G) 1 *
ProCGroups.Generation.wordProducts (commutatorSet G) t.length =
ProCGroups.Generation.wordProducts (commutatorSet G) (1 + t.length) := by
simpa using
(ProCGroups.Generation.wordProducts_mul_wordProducts (G := G) (commutatorSet G)
1 t.length)
have hmem' :
⁅a.1, a.2⁆ * (t.map fun p : G × G => ⁅p.1, p.2⁆).prod ∈
ProCGroups.Generation.wordProducts (commutatorSet G) (1 + t.length) := by
rw [← hEq]
simpa [ProCGroups.Generation.wordProducts_one] using hmul
simpa [Nat.add_comm] using hmem'
have hlen :
(l.map fun p : G × G => ⁅p.1, p.2⁆).prod ∈
ProCGroups.Generation.wordProducts (commutatorSet G) l.length :=
hlenAux l
exact ProCGroups.Generation.wordProducts_mono_len
(G := G) (X := commutatorSet G) (one_mem_commutatorSet G) hl (by simpa [hprod] using hlen)Proof. Work with the closed derived series and the maximal \(m\)-step solvable quotient. The quotient map kills exactly the relevant closed derived term, and statements about abelianization, torsion-freeness, faithful conjugation actions, centers, and centralizers are reduced to the induced maps on open subgroups and their topological abelianizations. Closure and functoriality are checked by monotonicity of closed commutators, compatibility of quotient maps, and passage to the corresponding quotient or open subgroup.
□theorem exists_lift_wordProducts_commutatorSet_of_quotient_isProductOfCommutatorsLE
{G : Type u} [Group G] {N : Subgroup G} [N.Normal] {n : ℕ} {x : G ⧸ N}
(hx : IsProductOfCommutatorsLE n x) :
∃ y ∈ ProCGroups.Generation.wordProducts (commutatorSet G) n,
QuotientGroup.mk' N y = xA bounded product of commutators in a quotient lifts to a bounded word product of commutators upstairs.
Show proof
by
classical
rcases hx with ⟨l, hl, hprod⟩
let q : G →* G ⧸ N := QuotientGroup.mk' N
let lift : G ⧸ N → G := fun z => Classical.choose (QuotientGroup.mk'_surjective N z)
have hlift : ∀ z : G ⧸ N, q (lift z) = z := fun z =>
Classical.choose_spec (QuotientGroup.mk'_surjective N z)
let L : List (G × G) := l.map fun p => (lift p.1, lift p.2)
let y : G := (L.map fun p : G × G => ⁅p.1, p.2⁆).prod
have hyword : y ∈ ProCGroups.Generation.wordProducts (commutatorSet G) n := by
refine mem_wordProducts_commutatorSet_of_isProductOfCommutatorsLE
(G := G) (n := n) (g := y) ?_
exact ⟨L, by simpa [L] using hl, rfl⟩
have hmapList :
∀ l : List ((G ⧸ N) × (G ⧸ N)),
q ((l.map fun p => ⁅lift p.1, lift p.2⁆).prod) =
(l.map fun p => ⁅p.1, p.2⁆).prod := by
intro l
induction l with
| nil =>
simp only [List.map_nil, List.prod_nil, QuotientGroup.mk'_apply, QuotientGroup.mk_one, q]
| cons a t ih =>
simp only [List.map_cons, List.prod_cons, map_mul, map_commutatorElement, hlift, ih, q]
have hmap :
q y = (l.map fun p : (G ⧸ N) × (G ⧸ N) => ⁅p.1, p.2⁆).prod := by
simpa [y, L, List.map_map] using hmapList l
exact ⟨y, hyword, hmap.trans hprod⟩Proof. Work with the closed derived series and the maximal \(m\)-step solvable quotient. The quotient map kills exactly the relevant closed derived term, and statements about abelianization, torsion-freeness, faithful conjugation actions, centers, and centralizers are reduced to the induced maps on open subgroups and their topological abelianizations. Closure and functoriality are checked by monotonicity of closed commutators, compatibility of quotient maps, and passage to the corresponding quotient or open subgroup.
□theorem isClosed_commutator_of_uniformFiniteQuotientCommutatorWidth
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(n : ℕ)
(hwidth :
∀ U : OpenNormalSubgroup G,
HasCommutatorWidthAtMost (G := G ⧸ (U : Subgroup G)) n) :
IsClosed ((commutator G : Subgroup G) : Set G)A uniform finite-quotient commutator-width bound forces the commutator subgroup of a profinite group to be closed.
Show proof
by
let X : Set G := commutatorSet G
let S : Set G := ProCGroups.Generation.wordProducts X n
have hXclosed : IsClosed X := by
simpa [X] using isClosed_commutatorSet (G := G)
have hSclosed : IsClosed S := by
simpa [S] using
(ProCGroups.Generation.wordProducts_isClosed (G := G) (X := X) hXclosed n)
have hSsubset :
S ⊆ ((commutator G : Subgroup G) : Set G) := by
intro x hx
have hxcl :
x ∈ ((Subgroup.closure X : Subgroup G) : Set G) :=
ProCGroups.Generation.wordProducts_subset_closure (G := G) X n hx
simpa [X, commutator_eq_closure] using hxcl
have hclosure_subset :
closure (((commutator G : Subgroup G) : Set G)) ⊆ S := by
intro x hxcl
let hG : IsProfiniteGroup G := ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
refine (IsProfiniteGroup.mem_closed_iff_forall_openNormal_quotient
(G := G) hG (S := S) hSclosed).2 ?_
intro U
let Q : Type u := G ⧸ (U : Subgroup G)
let q : G →* Q := QuotientGroup.mk' (U : Subgroup G)
have hpreClosed :
IsClosed (q ⁻¹' (((commutator Q : Subgroup Q) : Set Q))) := by
letI : DiscreteTopology Q :=
QuotientGroup.discreteTopology (ProCGroups.openNormalSubgroup_isOpen (G := G) U)
exact (isClosed_discrete _).preimage QuotientGroup.continuous_mk
have hcomm_pre :
((commutator G : Subgroup G) : Set G) ⊆
q ⁻¹' (((commutator Q : Subgroup Q) : Set Q)) := by
intro y hy
have hle : commutator G ≤ (commutator Q).comap q := by
rw [commutator_eq_closure]
refine (Subgroup.closure_le (K := (commutator Q).comap q)).2 ?_
intro z hz
rcases mem_commutatorSet_iff.mp hz with ⟨a, b, rfl⟩
change q ⁅a, b⁆ ∈ commutator Q
rw [map_commutatorElement]
rw [commutator_eq_closure]
exact Subgroup.subset_closure
(commutator_mem_commutatorSet (g₁ := q a) (g₂ := q b))
exact hle hy
have hxq : q x ∈ commutator Q :=
(closure_minimal hcomm_pre hpreClosed) hxcl
rcases exists_lift_wordProducts_commutatorSet_of_quotient_isProductOfCommutatorsLE
(G := G) (N := (U : Subgroup G)) (n := n) (x := q x)
(hwidth U (q x) hxq) with
⟨y, hyS, hyq⟩
exact ⟨y, hyS, hyq⟩
have hclosure_subset_comm :
closure (((commutator G : Subgroup G) : Set G)) ⊆
((commutator G : Subgroup G) : Set G) := fun x hx => hSsubset (hclosure_subset hx)
exact closure_eq_iff_isClosed.mp (subset_antisymm hclosure_subset_comm subset_closure)Proof. Work with the closed derived series and the maximal \(m\)-step solvable quotient. The quotient map kills exactly the relevant closed derived term, and statements about abelianization, torsion-freeness, faithful conjugation actions, centers, and centralizers are reduced to the induced maps on open subgroups and their topological abelianizations. Closure and functoriality are checked by monotonicity of closed commutators, compatibility of quotient maps, and passage to the corresponding quotient or open subgroup.
□