Module

Basic.lean

Nyll.ProCGroups.FiniteStepSolvableQuotients.Commutators.Basic

17 declarations indexed from sourceView source ↗

Module documentation

The topological commutator subgroup

This module identifies the first closed-derived term with the closure of the abstract commutator subgroup and records closedness and finite-width consequences.

Imports2

Imported by5

abbrev

topologicalCommutator

L24 ↗

ProCGroups.FiniteStepSolvableQuotients.topologicalCommutator

Documentation

The topological closure of the abstract commutator subgroup.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

abbrev topologicalCommutator
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Subgroup G

theorem

topologicalCommutator_eq_closedCommutator_top_top

L32 ↗

ProCGroups.FiniteStepSolvableQuotients.topologicalCommutator_eq_closedCommutator_top_top

Documentation

The topological commutator subgroup agrees with the closed commutator of the top subgroup with itself.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem topologicalCommutator_eq_closedCommutator_top_top
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    topologicalCommutator G = closedCommutator (⊤ : Subgroup G) ⊤

theorem

topDerivedTop_one_eq_topologicalCommutator

L38 ↗

ProCGroups.FiniteStepSolvableQuotients.topDerivedTop_one_eq_topologicalCommutator

Documentation

The first top-derived subgroup is the topological commutator subgroup.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem topDerivedTop_one_eq_topologicalCommutator
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    topDerivedTop G 1 = topologicalCommutator G

theorem

closedDerivedSeries_top_one_eq_closedCommutator

L45 ↗

ProCGroups.FiniteStepSolvableQuotients.closedDerivedSeries_top_one_eq_closedCommutator

Documentation

The first closed derived subgroup of the whole group is the closed commutator subgroup.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem closedDerivedSeries_top_one_eq_closedCommutator
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    closedDerivedSeries (G := G) (⊤ : Subgroup G) 1 =
      Subgroup.closedCommutator G

theorem

topologicalCommutator_eq_commutator_of_isClosed

L58 ↗

ProCGroups.FiniteStepSolvableQuotients.topologicalCommutator_eq_commutator_of_isClosed

Documentation

When the ordinary commutator subgroup is closed, it agrees with the topological commutator subgroup.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

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 G

theorem

isClosed_commutatorSet

L67 ↗

ProCGroups.FiniteStepSolvableQuotients.isClosed_commutatorSet

Documentation

In a compact Hausdorff topological group, the set of individual commutators is closed.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem isClosed_commutatorSet
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] :
    IsClosed (commutatorSet G : Set G)

theorem

commutator_subset_topologicalCommutator

L86 ↗

ProCGroups.FiniteStepSolvableQuotients.commutator_subset_topologicalCommutator

Documentation

Every algebraic commutator lies in the topological commutator subgroup.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem commutator_subset_topologicalCommutator
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    commutator G ≤ topologicalCommutator G

theorem

topologicalCommutator_eq_bot_of_commGroup

L92 ↗

ProCGroups.FiniteStepSolvableQuotients.topologicalCommutator_eq_bot_of_commGroup

Documentation

The topological commutator subgroup of a commutative group is trivial.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem topologicalCommutator_eq_bot_of_commGroup
    (G : Type u) [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :
    topologicalCommutator G = ⊥

theorem

topDerivedTop_eq_bot_of_commGroup

L104 ↗

ProCGroups.FiniteStepSolvableQuotients.topDerivedTop_eq_bot_of_commGroup

Documentation

A commutative topological group has trivial positive closed derived stages.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem topDerivedTop_eq_bot_of_commGroup
    {G : Type u} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G]
    {m : ℕ} (hm : 1 ≤ m) :
    topDerivedTop G m = ⊥

theorem

topDerivedTop_eq_bot_of_procyclic

L119 ↗

ProCGroups.FiniteStepSolvableQuotients.topDerivedTop_eq_bot_of_procyclic

Documentation

A procyclic group has trivial positive closed derived stages.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem topDerivedTop_eq_bot_of_procyclic
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProCGroups.ProC.HasCyclicOpenNormalBasis G) {m : ℕ} (hm : 1 ≤ m) :
    topDerivedTop G m = ⊥

theorem

maxSolvQuot_leftFactor_image_mem_zpowers

L134 ↗

ProCGroups.FiniteStepSolvableQuotients.maxSolvQuot_leftFactor_image_mem_zpowers

Documentation

Images of a topologically cyclic source in a discrete quotient of a maximal solvable quotient are algebraic powers of the image of the chosen generator.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

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)))

def

IsProductOfCommutatorsLE

L153 ↗

ProCGroups.FiniteStepSolvableQuotients.IsProductOfCommutatorsLE

Documentation

\(G\) can be written as a product of at most \(n\) commutators.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

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

theorem

isProductOfCommutatorsLE_one

L158 ↗

ProCGroups.FiniteStepSolvableQuotients.isProductOfCommutatorsLE_one

Documentation

The identity element gives a product-of-commutators witness of width zero.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem isProductOfCommutatorsLE_one
    {G : Type u} [Group G] (n : ℕ) :
    IsProductOfCommutatorsLE n (1 : G)

theorem

isProductOfCommutatorsLE_commutatorElement

L165 ↗

ProCGroups.FiniteStepSolvableQuotients.isProductOfCommutatorsLE_commutatorElement

Documentation

A single commutator gives a product-of-commutators witness of width one.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem isProductOfCommutatorsLE_commutatorElement
    {G : Type u} [Group G] (x y : G) :
    IsProductOfCommutatorsLE 1 ⁅x, y⁆

theorem

mul

L175 ↗

ProCGroups.FiniteStepSolvableQuotients.IsProductOfCommutatorsLE.mul

Documentation

Multiplying two bounded commutator-product witnesses gives a witness with the sum of the allowed widths.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

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)

theorem

mono

L187 ↗

ProCGroups.FiniteStepSolvableQuotients.IsProductOfCommutatorsLE.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 commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem IsProductOfCommutatorsLE.mono
    {G : Type u} [Group G]
    {m n : ℕ} {g : G}
    (hg : IsProductOfCommutatorsLE m g)
    (hmn : m ≤ n) :
    IsProductOfCommutatorsLE n g

theorem

mem_commutator_of_isProductOfCommutatorsLE

L197 ↗

ProCGroups.FiniteStepSolvableQuotients.mem_commutator_of_isProductOfCommutatorsLE

Documentation

A product of commutators lying in the given subgroup belongs to the commutator subgroup.

Source context 3 commands

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

open scoped Topology commutatorElement
namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem mem_commutator_of_isProductOfCommutatorsLE
    {G : Type u} [Group G]
    {n : ℕ} {g : G}
    (hg : IsProductOfCommutatorsLE n g) :
    g ∈ commutator G

Module documentation

The topological commutator subgroup

Declarations