Module

AbTorsionFree.lean

Nyll.ProCGroups.FiniteStepSolvableQuotients.AbTorsionFree

3 declarations indexed from sourceView source ↗

Module documentation

Ab-torsion-freeness

The topological abelianization of every open subgroup is torsion-free. These are general topological-group definitions and consequences.

Imports2

Imported by3

def

IsAbTorsionFree

L26 ↗

ProCGroups.FiniteStepSolvableQuotients.IsAbTorsionFree

Documentation

Every open subgroup has torsion-free topological abelianization.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u

Lean source · statement

def IsAbTorsionFree
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Prop

theorem

isMulTorsionFree_topologicalAbelianization_of_isAbTorsionFree

L32 ↗

ProCGroups.FiniteStepSolvableQuotients.isMulTorsionFree_topologicalAbelianization_of_isAbTorsionFree

Documentation

Ab-torsion-freeness implies torsion-freeness of the ambient topological abelianization.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u

Lean source · statement

theorem isMulTorsionFree_topologicalAbelianization_of_isAbTorsionFree
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (hG : IsAbTorsionFree G) :
    IsMulTorsionFree (TopologicalAbelianization G)

theorem

isMulTorsionFree_of_isAbTorsionFree_commGroup

L43 ↗

ProCGroups.FiniteStepSolvableQuotients.isMulTorsionFree_of_isAbTorsionFree_commGroup

Documentation

For a commutative T₁ topological group, ab-torsion-freeness implies torsion-freeness of the group itself.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u

Lean source · statement

theorem isMulTorsionFree_of_isAbTorsionFree_commGroup
    {G : Type u} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G]
    (hG : IsAbTorsionFree G) :
    IsMulTorsionFree G

Module documentation

Ab-torsion-freeness

Declarations

IsAbTorsionFree

isMulTorsionFree_topologicalAbelianization_of_isAbTorsionFree

isMulTorsionFree_of_isAbTorsionFree_commGroup