Module

Kernels.lean

Nyll.ProCGroups.ProC.Kernels

10 declarations indexed from sourceView source ↗

Module documentation

Profinite kernels and their abelianizations

This file equips kernels of continuous maps between profinite groups with their closed profinite topology and constructs the corresponding topological abelianization. It also transfers open-normal quotient bases in a finite-group class to these kernel constructions.

Imports3

Mathlib.GroupTheory.Abelianization.Defs
Nyll.ProCGroups.Abelian.TopologicalAbelianization
Nyll.ProCGroups.ProC.Subgroups.Closed

Imported by5

abbrev

ProfiniteKernelSubgroup

L31 ↗

ProCGroups.ProC.ProfiniteKernelSubgroup

Documentation

The kernel subgroup of a continuous homomorphism.

Source context 6 commands

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

namespace ProCGroups.ProC
noncomputable section
open scoped Pointwise
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

abbrev ProfiniteKernelSubgroup (psi : ContinuousMonoidHom G H) : Subgroup G

theorem

isClosed_profiniteKernelSubgroup

L36 ↗

ProCGroups.ProC.isClosed_profiniteKernelSubgroup

Documentation

The kernel of a continuous homomorphism into a \(T_1\) topological group is closed.

Source context 7 commands

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

namespace ProCGroups.ProC
noncomputable section
open scoped Pointwise
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in

Lean source · statement

theorem isClosed_profiniteKernelSubgroup [T1Space H] (psi : ContinuousMonoidHom G H) :
    IsClosed ((ProfiniteKernelSubgroup psi : Subgroup G) : Set G)

abbrev

ProfiniteKernelAbelianization

L42 ↗

ProCGroups.ProC.ProfiniteKernelAbelianization

Documentation

The topological kernel abelianization \(\ker \psi / \overline{[\ker \psi, \ker \psi]}\).

Source context 6 commands

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

namespace ProCGroups.ProC
noncomputable section
open scoped Pointwise
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

abbrev ProfiniteKernelAbelianization (psi : ContinuousMonoidHom G H) : Type u

abbrev

ProfiniteKernelAbelianizationAdd

L46 ↗

ProCGroups.ProC.ProfiniteKernelAbelianizationAdd

Documentation

Additive notation for the topological kernel abelianization.

Source context 6 commands

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

namespace ProCGroups.ProC
noncomputable section
open scoped Pointwise
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

abbrev ProfiniteKernelAbelianizationAdd (psi : ContinuousMonoidHom G H) : Type u

def

kernelAbelianizationToProfiniteKernelAbelianizationHom

L53 ↗

ProCGroups.ProC.kernelAbelianizationToProfiniteKernelAbelianizationHom

Documentation

The canonical quotient map from the algebraic kernel abelianization to the topological kernel abelianization.

Source context 6 commands

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

namespace ProCGroups.ProC
noncomputable section
open scoped Pointwise
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def kernelAbelianizationToProfiniteKernelAbelianizationHom
    (psi : ContinuousMonoidHom G H) :
    Abelianization (ProfiniteKernelSubgroup psi) →*
      ProfiniteKernelAbelianization psi

def

kernelAbelianizationToProfiniteKernelAbelianization

L72 ↗

ProCGroups.ProC.kernelAbelianizationToProfiniteKernelAbelianization

Documentation

Additive form of the quotient from \((\ker \psi)^{ab}\) to the topological kernel abelianization.

Source context 6 commands

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

namespace ProCGroups.ProC
noncomputable section
open scoped Pointwise
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def kernelAbelianizationToProfiniteKernelAbelianization
    (psi : ContinuousMonoidHom G H) :
    Additive (Abelianization (ProfiniteKernelSubgroup psi)) →+
      ProfiniteKernelAbelianizationAdd psi

theorem

kernelAbelianizationToProfiniteKernelAbelianization_of

L85 ↗

ProCGroups.ProC.kernelAbelianizationToProfiniteKernelAbelianization_of

Documentation

The canonical quotient map sends the class of a kernel element to its class modulo the topological closure of the commutator subgroup.

Source context 7 commands

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

namespace ProCGroups.ProC
noncomputable section
open scoped Pointwise
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in

Lean source · statement

theorem kernelAbelianizationToProfiniteKernelAbelianization_of
    (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi) :
    kernelAbelianizationToProfiniteKernelAbelianization
        (G := G) (H := H) psi (Additive.ofMul (Abelianization.of n)) =
      Additive.ofMul
        (QuotientGroup.mk'
          (Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) n)

theorem

kernelAbelianizationToProfiniteKernelAbelianization_surjective

L98 ↗

ProCGroups.ProC.kernelAbelianizationToProfiniteKernelAbelianization_surjective

Documentation

The canonical map from the algebraic kernel abelianization to the topological one is surjective.

Source context 7 commands

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

namespace ProCGroups.ProC
noncomputable section
open scoped Pointwise
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in

Lean source · statement

theorem kernelAbelianizationToProfiniteKernelAbelianization_surjective
    (psi : ContinuousMonoidHom G H) :
    Function.Surjective
      (kernelAbelianizationToProfiniteKernelAbelianization
        (G := G) (H := H) psi)

theorem

profiniteKernelSubgroup

L123 ↗

ProCGroups.ProC.HasOpenNormalBasisInClass.profiniteKernelSubgroup

Documentation

The closed kernel of a morphism out of a group with an open-normal \(C\)-basis again has such a basis.

Source context 7 commands

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

namespace ProCGroups.ProC
noncomputable section
open scoped Pointwise
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in

Lean source · statement

theorem HasOpenNormalBasisInClass.profiniteKernelSubgroup
    {C : FiniteGroupClass.{u}}
    (hHer : FiniteGroupClass.Hereditary C) (hG : HasOpenNormalBasisInClass C G)
    [T1Space H] (psi : ContinuousMonoidHom G H) :
    HasOpenNormalBasisInClass C (ProfiniteKernelSubgroup psi)

theorem

profiniteKernelAbelianization

L135 ↗

ProCGroups.ProC.HasOpenNormalBasisInClass.profiniteKernelAbelianization

Documentation

The topological kernel abelianization of a morphism out of a group with an open-normal \(C\)-basis again has such a basis.

Source context 7 commands

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

namespace ProCGroups.ProC
noncomputable section
open scoped Pointwise
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in

Lean source · statement

theorem HasOpenNormalBasisInClass.profiniteKernelAbelianization
    {C : FiniteGroupClass.{u}}
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hC : FiniteGroupClass.FullFormation C) (hG : HasOpenNormalBasisInClass C G)
    [T1Space H] (psi : ContinuousMonoidHom G H) :
    HasOpenNormalBasisInClass C (ProfiniteKernelAbelianization psi)

Module documentation

Profinite kernels and their abelianizations

Declarations