Module

ClosureFromFiniteQuotients.lean

Nyll.ProCGroups.FiniteStepSolvableQuotients.Commutators.ClosureFromFiniteQuotients

5 declarations indexed from sourceView source ↗

Module documentation

Detecting closed commutator subgroups in finite quotients

This module relates bounded commutator width to bounded word products and lifts uniform finite-quotient bounds to closedness of the commutator subgroup.

Imports3

Imported by1

Nyll.ProCGroups.FiniteStepSolvableQuotients.Commutators.All

def

HasCommutatorWidthAtMost

L25 ↗

ProCGroups.FiniteStepSolvableQuotients.HasCommutatorWidthAtMost

Documentation

Every element of the commutator subgroup is a product of at most \(n\) commutators.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology Pointwise commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

def HasCommutatorWidthAtMost
    {G : Type u} [Group G] (n : ℕ) : Prop

theorem

mono

L30 ↗

ProCGroups.FiniteStepSolvableQuotients.HasCommutatorWidthAtMost.mono

Documentation

A product of at most \(m\) commutators is also a product of at most any larger bound \(n\).

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology Pointwise commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem HasCommutatorWidthAtMost.mono
    {G : Type u} [Group G]
    {m n : ℕ}
    (h : HasCommutatorWidthAtMost (G := G) m)
    (hmn : m ≤ n) :
    HasCommutatorWidthAtMost (G := G) n

theorem

mem_wordProducts_commutatorSet_of_isProductOfCommutatorsLE

L44 ↗

ProCGroups.FiniteStepSolvableQuotients.mem_wordProducts_commutatorSet_of_isProductOfCommutatorsLE

Documentation

Products of boundedly many commutators lie in the bounded word-product set generated by individual commutators.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology Pointwise commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem mem_wordProducts_commutatorSet_of_isProductOfCommutatorsLE
    {G : Type u} [Group G] {n : ℕ} {g : G}
    (hg : IsProductOfCommutatorsLE n g) :
    g ∈ ProCGroups.Generation.wordProducts (commutatorSet G) n

theorem

exists_lift_wordProducts_commutatorSet_of_quotient_isProductOfCommutatorsLE

L93 ↗

ProCGroups.FiniteStepSolvableQuotients.exists_lift_wordProducts_commutatorSet_of_quotient_isProductOfCommutatorsLE

Documentation

A bounded product of commutators in a quotient lifts to a bounded word product of commutators upstairs.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology Pointwise commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

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 = x

theorem

isClosed_commutator_of_uniformFiniteQuotientCommutatorWidth

L137 ↗

ProCGroups.FiniteStepSolvableQuotients.isClosed_commutator_of_uniformFiniteQuotientCommutatorWidth

Documentation

A uniform finite-quotient commutator-width bound forces the commutator subgroup of a profinite group to be closed.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology Pointwise commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

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)

Module documentation

Detecting closed commutator subgroups in finite quotients

Declarations

HasCommutatorWidthAtMost

mono

mem_wordProducts_commutatorSet_of_isProductOfCommutatorsLE

exists_lift_wordProducts_commutatorSet_of_quotient_isProductOfCommutatorsLE

isClosed_commutator_of_uniformFiniteQuotientCommutatorWidth