Module

ResidualCore.lean

Nyll.ProCGroups.ProC.MaximalQuotients.ResidualCore

4 declarations indexed from sourceView source ↗

Module documentation

Closed kernels and the pro-\(C\) residual core

ProCQuotientKernel C G bundles a closed normal subgroup together with an open-normal quotient-in-\(C\) basis on its quotient. The residual core is their intersection; closedness and normality therefore follow directly from the stored kernel data, without reconstructing separation axioms from the basis property.

Imports2

Mathlib.Topology.Algebra.Group.Quotient
Nyll.ProCGroups.ProC.OpenNormalSubgroups.ProCGroup

Imported by15

structure

ProCQuotientKernel

L26 ↗

ProCGroups.ProC.ProCQuotientKernel

Documentation

Bundled closed normal kernels whose quotient has an open-normal quotient-in-\(C\) basis.

Source context 3 commands

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

open Set
namespace ProCGroups.ProC
universe u

Lean source · full declaration

structure ProCQuotientKernel
    (C : FiniteGroupClass)
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    extends ClosedSubgroup G where
  /-- The underlying closed subgroup is normal in \(G\). -/
  normal : toSubgroup.Normal
  /-- The quotient by the kernel has an open-normal basis of finite quotients in \(C\). -/
  quotient_hasOpenNormalBasisInClass : letI := normal; HasOpenNormalBasisInClass C (G ⧸ toSubgroup)

def

proCResidualCore

L39 ↗

ProCGroups.ProC.proCResidualCore

Documentation

The residual core \(R_C(G)\), defined as the intersection of all closed normal kernels whose quotient has an open-normal quotient-in-\(C\) basis.

Source context 4 commands

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

open Set
namespace ProCGroups.ProC
universe u
attribute [instance] ProCQuotientKernel.normal

Lean source · statement

def proCResidualCore
    (C : FiniteGroupClass)
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Subgroup G

theorem

proCResidualCore_normal

L46 ↗

ProCGroups.ProC.proCResidualCore_normal

Documentation

The residual core is a normal subgroup.

Source context 4 commands

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

open Set
namespace ProCGroups.ProC
universe u
attribute [instance] ProCQuotientKernel.normal

Lean source · statement

theorem proCResidualCore_normal
    (C : FiniteGroupClass)
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    (proCResidualCore C G).Normal

theorem

proCResidualCore_isClosed

L58 ↗

ProCGroups.ProC.proCResidualCore_isClosed

Documentation

The residual core is closed.

Source context 4 commands

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

open Set
namespace ProCGroups.ProC
universe u
attribute [instance] ProCQuotientKernel.normal

Lean source · statement

theorem proCResidualCore_isClosed
    (C : FiniteGroupClass)
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    IsClosed ((proCResidualCore C G : Subgroup G) : Set G)

Module documentation

Closed kernels and the pro-\(C\) residual core

Declarations

ProCQuotientKernel

proCResidualCore

proCResidualCore_normal

proCResidualCore_isClosed