ProCGroups.FiniteStepSolvableQuotients.Commutators.Basic
This module studies basic for pro cgroups. The topological closure of the abstract commutator subgroup. The topological commutator subgroup agrees with the closed commutator of the top subgroup with itself.
import
abbrev topologicalCommutator
(G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Subgroup G :=
(commutator G).topologicalClosureThe topological closure of the abstract commutator subgroup.
@[simp] theorem topologicalCommutator_eq_closedCommutator_top_top
(G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
topologicalCommutator G = closedCommutator (⊤ : Subgroup G) ⊤The topological commutator subgroup agrees with the closed commutator of the top subgroup with itself.
Show proof
by
simp only [topologicalCommutator, commutator, closedCommutator]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.
□@[simp] theorem topDerivedTop_one_eq_topologicalCommutator
(G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
topDerivedTop G 1 = topologicalCommutator GThe first top-derived subgroup is the topological commutator subgroup.
Show proof
by
simp only [topDerivedTop, closedDerivedSeries, closedCommutator, topologicalCommutator, commutator]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 closedDerivedSeries_top_one_eq_closedCommutator
(G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
closedDerivedSeries (G := G) (⊤ : Subgroup G) 1 =
Subgroup.closedCommutator GThe first closed derived subgroup of the whole group is the closed commutator subgroup.
Show proof
by
calc
closedDerivedSeries (G := G) (⊤ : Subgroup G) 1 = topDerivedTop G 1 := rfl
_ = topologicalCommutator G := topDerivedTop_one_eq_topologicalCommutator G
_ = Subgroup.closedCommutator G := rflProof. 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.
□@[simp] theorem topologicalCommutator_eq_commutator_of_isClosed
(G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
(hclosed : IsClosed ((commutator G : Subgroup G) : Set G)) :
topologicalCommutator G = commutator GWhen the ordinary commutator subgroup is closed, it agrees with the topological commutator subgroup.
Show proof
by
ext x
change x ∈ closure ((commutator G : Set G)) ↔ x ∈ (commutator G : Set G)
rw [closure_eq_iff_isClosed.mpr hclosed]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_commutatorSet
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [T2Space G] :
IsClosed (commutatorSet G : Set G)In a compact Hausdorff topological group, the set of individual commutators is closed.
Show proof
by
let f : G × G → G := fun p => ⁅p.1, p.2⁆
have hf : Continuous f := by
have hfst : Continuous fun p : G × G => p.1 := continuous_fst
have hsnd : Continuous fun p : G × G => p.2 := continuous_snd
simpa [f, commutatorElement_def, mul_assoc] using
(((hfst.mul hsnd).mul hfst.inv).mul hsnd.inv)
have himage : f '' (Set.univ : Set (G × G)) = commutatorSet G := by
ext z
constructor
· rintro ⟨p, -, rfl⟩
exact commutator_mem_commutatorSet (g₁ := p.1) (g₂ := p.2)
· intro hz
rcases mem_commutatorSet_iff.mp hz with ⟨x, y, rfl⟩
exact ⟨(x, y), by simp only [Set.mem_univ], rfl⟩
simpa [himage] using (isCompact_univ.image hf).isClosedProof. 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 commutator_subset_topologicalCommutator
(G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
commutator G ≤ topologicalCommutator GEvery algebraic commutator lies in the topological commutator subgroup.
Show proof
Subgroup.le_topologicalClosure _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.
□@[simp] theorem topologicalCommutator_eq_bot_of_commGroup
(G : Type u) [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :
topologicalCommutator G = ⊥The topological commutator subgroup of a commutative group is trivial.
Show proof
by
have hcomm : commutator G = ⊥ := by
rw [commutator_eq_bot_iff_center_eq_top, CommGroup.center_eq_top]
rw [topologicalCommutator, hcomm]
ext x
change x ∈ closure ({(1 : G)} : Set G) ↔ x ∈ (⊥ : Subgroup G)
rw [closure_singleton]
simp only [Set.mem_singleton_iff, Subgroup.mem_bot]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 topDerivedTop_eq_bot_of_commGroup
{G : Type u} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G]
{m : ℕ} (hm : 1 ≤ m) :
topDerivedTop G m = ⊥A commutative topological group has trivial positive closed derived stages.
Show proof
by
have h1 : topDerivedTop G 1 = (⊥ : Subgroup G) := by
rw [topDerivedTop_one_eq_topologicalCommutator]
exact topologicalCommutator_eq_bot_of_commGroup G
have hle : topDerivedTop G m ≤ topDerivedTop G 1 :=
(topDerivedTop_antitone (G := G)) hm
have hlebot : topDerivedTop G m ≤ (⊥ : Subgroup G) := by
rw [← h1]
exact hle
exact le_antisymm hlebot bot_leProof. 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 topDerivedTop_eq_bot_of_procyclic
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
(hG : ProCGroups.ProC.IsProcyclicGroup G) {m : ℕ} (hm : 1 ≤ m) :
topDerivedTop G m = ⊥A procyclic group has trivial positive closed derived stages.
Show proof
by
letI : T2Space G := hG.t2Space
have hcomm : ∀ a b : G, a * b = b * a :=
ProCGroups.ProC.IsProabelianGroup.isAbelian (G := G)
(ProCGroups.ProC.IsProcyclicGroup.isProabelianGroup (G := G) hG)
let base : Group G := inferInstance
letI : CommGroup G := { base with mul_comm := hcomm }
exact topDerivedTop_eq_bot_of_commGroup hmProof. 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 maxSolvQuot_leftFactor_image_mem_zpowers
{Ω A B : Type u}
[TopologicalSpace Ω] [Group Ω] [IsTopologicalGroup Ω]
[TopologicalSpace A] [Group A] [IsTopologicalGroup A]
[TopologicalSpace B] [Group B] [IsTopologicalGroup B] [DiscreteTopology B]
{m : ℕ}
(q : MaxSolvQuot Ω m →* B) (hq : Continuous q)
(ιC : A →ₜ* Ω) {x a : A}
(hxgen : ProCGroups.Generation.TopologicallyGenerates (G := A) ({x} : Set A)) :
q (continuousToMaxSolvQuot Ω m (ιC a)) ∈
Subgroup.zpowers (q (continuousToMaxSolvQuot Ω m (ιC x)))Show proof
by
let f : A →* B := (q.comp (continuousToMaxSolvQuot Ω m : Ω →* MaxSolvQuot Ω m)).comp ιC
have hf : Continuous f := by
exact hq.comp ((continuousToMaxSolvQuot Ω m).continuous_toFun.comp ιC.continuous_toFun)
simpa [f] using
ProCGroups.Generation.monoidHom_map_mem_zpowers_of_topologicallyGenerates_singleton
(A := A) f hf hxgen (a := a)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.
□def IsProductOfCommutatorsLE
{G : Type u} [Group G] (n : ℕ) (g : G) : Prop :=
∃ l : List (G × G), l.length ≤ n ∧ (l.map fun p => ⁅p.1, p.2⁆).prod = g\(G\) can be written as a product of at most \(n\) commutators.
theorem isProductOfCommutatorsLE_one
{G : Type u} [Group G] (n : ℕ) :
IsProductOfCommutatorsLE n (1 : G)The identity element gives a product-of-commutators witness of width zero.
Show proof
by
refine ⟨[], Nat.zero_le _, ?_⟩
simp only [List.map_nil, List.prod_nil]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 isProductOfCommutatorsLE_commutatorElement
{G : Type u} [Group G] (x y : G) :
IsProductOfCommutatorsLE 1 ⁅x, y⁆A single commutator gives a product-of-commutators witness of width one.
Show proof
by
refine ⟨[(x, y)], by simp only [List.length_cons, List.length_nil, zero_add, le_refl], ?_⟩
simp only [List.map_cons, List.map_nil, List.prod_cons, List.prod_nil, mul_one]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 IsProductOfCommutatorsLE.mul
{G : Type u} [Group G]
{m n : ℕ} {g h : G}
(hg : IsProductOfCommutatorsLE m g)
(hh : IsProductOfCommutatorsLE n h) :
IsProductOfCommutatorsLE (m + n) (g * h)Multiplying two bounded commutator-product witnesses gives a witness with the sum of the allowed widths.
Show proof
by
rcases hg with ⟨lg, hlg, rfl⟩
rcases hh with ⟨lh, hlh, rfl⟩
refine ⟨lg ++ lh, by simpa using Nat.add_le_add hlg hlh, ?_⟩
simp only [List.map_append, List.prod_append]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 IsProductOfCommutatorsLE.mono
{G : Type u} [Group G]
{m n : ℕ} {g : G}
(hg : IsProductOfCommutatorsLE m g)
(hmn : m ≤ n) :
IsProductOfCommutatorsLE n gA product of at most \(m\) commutators is also a product of at most any larger bound \(n\).
Show proof
by
rcases hg with ⟨l, hl, hprod⟩
exact ⟨l, le_trans hl hmn, 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 mem_commutator_of_isProductOfCommutatorsLE
{G : Type u} [Group G]
{n : ℕ} {g : G}
(hg : IsProductOfCommutatorsLE n g) :
g ∈ commutator GA product of commutators lying in the given subgroup belongs to the commutator subgroup.
Show proof
by
rcases hg with ⟨l, -, rfl⟩
induction l with
| nil =>
simp only [commutator, List.map_nil, List.prod_nil, one_mem]
| cons a t ih =>
have ha : ⁅a.1, a.2⁆ ∈ commutator G := by
rw [commutator_eq_closure]
exact Subgroup.subset_closure (commutator_mem_commutatorSet (g₁ := a.1) (g₂ := a.2))
exact Subgroup.mul_mem _ ha ihProof. 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.
□