Module

ClosedCommutator.lean

Nyll.ProCGroups.ProC.OpenNormalSubgroups.ClosedCommutator

8 declarations indexed from sourceView source ↗

Module documentation

Detecting the closed commutator subgroup in finite quotients

Membership in the topological closure of the commutator subgroup is characterized by the images in open-normal pro-\(C\) quotients. Equivalent formulations use quotient commutators and cofinal families of open normal subgroups.

Imports3

Imported by4

def

FiniteDiscreteAbelianMapsKillKernel

L31 ↗

ProCGroups.ProC.FiniteDiscreteAbelianMapsKillKernel

Documentation

Every continuous homomorphism from the source to a finite discrete abelian group kills the kernel of f.

Source context 6 commands

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

namespace ProCGroups.ProC
open scoped Topology
universe u
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G]

Lean source · statement

def FiniteDiscreteAbelianMapsKillKernel
    {Q : Type u} [Group Q] [TopologicalSpace Q]
    (f : G →ₜ* Q) : Prop

theorem

ker_le_closedCommutator_of_finiteDiscreteAbelianMapsKillKernel

L42 ↗

ProCGroups.ProC.ker_le_closedCommutator_of_finiteDiscreteAbelianMapsKillKernel

Documentation

For a profinite source, finite discrete abelian targets detect the closed commutator subgroup. Consequently, if all such homomorphisms kill the kernel of f, then that kernel is contained in the closed commutator subgroup.

Source context 6 commands

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

namespace ProCGroups.ProC
open scoped Topology
universe u
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G]

Lean source · statement

theorem ker_le_closedCommutator_of_finiteDiscreteAbelianMapsKillKernel
    [TotallyDisconnectedSpace G]
    {Q : Type u} [Group Q] [TopologicalSpace Q]
    (f : G →ₜ* Q) (hkill : FiniteDiscreteAbelianMapsKillKernel f) :
    f.ker ≤ Subgroup.closedCommutator G

theorem

quotient_mk_mem_commutator_of_surjective_image_mem_commutator

L82 ↗

ProCGroups.ProC.quotient_mk_mem_commutator_of_surjective_image_mem_commutator

Documentation

A quotient-level commutator descent along a surjective homomorphism. If \(f: N \to K\) is onto, f n is in the ordinary commutator subgroup of K, and the kernel of f dies in the quotient \(N/U\), then the image of n in \(N/U\) is in the ordinary commutator subgroup.

Source context 6 commands

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

namespace ProCGroups.ProC
open scoped Topology
universe u
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G]

Lean source · statement

theorem quotient_mk_mem_commutator_of_surjective_image_mem_commutator
    {N K : Type u} [Group N] [Group K]
    (f : N →* K) (hf : Function.Surjective f)
    (U : Subgroup N) [U.Normal] (hkerU : f.ker ≤ U)
    {n : N} (hn : f n ∈ commutator K) :
    QuotientGroup.mk' U n ∈ commutator (N ⧸ U)

theorem

mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient

L126 ↗

ProCGroups.ProC.HasOpenNormalBasisInClass.mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient

Documentation

Membership in the closed commutator subgroup of a pro-\(C\) group is detected on every open-normal quotient whose quotient lies in \(C\).

Source context 7 commands

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

namespace ProCGroups.ProC
open scoped Topology
universe u
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G]
namespace HasOpenNormalBasisInClass

Lean source · statement

theorem mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient
    (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) {x : G}
    (hx : ∀ U : OpenNormalSubgroupInClass C G,
      QuotientGroup.mk' (U.1 : Subgroup G) x ∈
        Subgroup.closedCommutator (G ⧸ (U.1 : Subgroup G))) :
    x ∈ Subgroup.closedCommutator G

theorem

mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient

L180 ↗

ProCGroups.ProC.HasOpenNormalBasisInClass.mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient

Documentation

Closed-commutator membership in a pro-\(C\) group is equivalent to closed-commutator membership after every open-normal quotient whose quotient lies in \(C\).

Source context 7 commands

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

namespace ProCGroups.ProC
open scoped Topology
universe u
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G]
namespace HasOpenNormalBasisInClass

Lean source · statement

theorem mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient
    (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) {x : G} :
    x ∈ Subgroup.closedCommutator G ↔
      ∀ U : OpenNormalSubgroupInClass C G,
        QuotientGroup.mk' (U.1 : Subgroup G) x ∈
          Subgroup.closedCommutator (G ⧸ (U.1 : Subgroup G))

theorem

mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient_commutator

L196 ↗

ProCGroups.ProC.HasOpenNormalBasisInClass.mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient_commutator

Documentation

An element belongs to the closed commutator subgroup of a pro-\(C\) group when its image belongs to the ordinary commutator subgroup in every finite open-normal quotient in \(C\).

Source context 7 commands

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

namespace ProCGroups.ProC
open scoped Topology
universe u
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G]
namespace HasOpenNormalBasisInClass

Lean source · statement

theorem mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient_commutator
    (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) {x : G}
    (hx : ∀ U : OpenNormalSubgroupInClass C G,
      QuotientGroup.mk' (U.1 : Subgroup G) x ∈
        commutator (G ⧸ (U.1 : Subgroup G))) :
    x ∈ Subgroup.closedCommutator G

theorem

mem_closedCommutator_of_forall_exists_openNormalSubgroupInClass_le_quotient_commutator

L212 ↗

ProCGroups.ProC.HasOpenNormalBasisInClass.mem_closedCommutator_of_forall_exists_openNormalSubgroupInClass_le_quotient_commutator

Documentation

An element belongs to the closed commutator subgroup when, below every open-normal quotient in \(C\), its image belongs to the ordinary commutator subgroup in some smaller open-normal quotient in \(C\).

Source context 7 commands

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

namespace ProCGroups.ProC
open scoped Topology
universe u
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G]
namespace HasOpenNormalBasisInClass

Lean source · statement

theorem mem_closedCommutator_of_forall_exists_openNormalSubgroupInClass_le_quotient_commutator
    (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) {x : G}
    (hx : ∀ U : OpenNormalSubgroupInClass C G,
      ∃ V : OpenNormalSubgroupInClass C G,
        (V.1 : Subgroup G) ≤ (U.1 : Subgroup G) ∧
          QuotientGroup.mk' (V.1 : Subgroup G) x ∈
            commutator (G ⧸ (V.1 : Subgroup G))) :
    x ∈ Subgroup.closedCommutator G

theorem

mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient_commutator

L253 ↗

ProCGroups.ProC.HasOpenNormalBasisInClass.mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient_commutator

Documentation

Closed-commutator membership in a pro-\(C\) group is equivalent to ordinary commutator membership after every finite open-normal quotient in \(C\).

Source context 7 commands

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

namespace ProCGroups.ProC
open scoped Topology
universe u
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G]
namespace HasOpenNormalBasisInClass

Lean source · statement

theorem mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient_commutator
    (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) {x : G} :
    x ∈ Subgroup.closedCommutator G ↔
      ∀ U : OpenNormalSubgroupInClass C G,
        QuotientGroup.mk' (U.1 : Subgroup G) x ∈
          commutator (G ⧸ (U.1 : Subgroup G))

Module documentation

Detecting the closed commutator subgroup in finite quotients

Declarations