Module

ResidualQuotient.lean

Nyll.ProCGroups.ProC.MaximalQuotients.ResidualQuotient

1 declaration indexed from sourceView source ↗

Module documentation

The quotient by the pro-C residual core

For a formation C, the quotient by the intersection of all kernels with pro-C quotient is itself pro-C. The proof realizes the residual quotient as a subdirect product of all the pro-C quotients occurring in the definition of the residual core.

Imports3

Imported by12

theorem

proCResidualCoreQuotient_hasOpenNormalBasisInClass

L26 ↗

ProCGroups.ProC.proCResidualCoreQuotient_hasOpenNormalBasisInClass

Documentation

The quotient by the pro-C residual core has an open-normal quotient basis in C.

Source context 3 commands

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

open Set
namespace ProCGroups.ProC
universe u

Lean source · statement

theorem proCResidualCoreQuotient_hasOpenNormalBasisInClass
    {C : FiniteGroupClass.{u}}
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hForm : FiniteGroupClass.Formation C) :
    HasOpenNormalBasisInClass C (G ⧸ proCResidualCore C G)

Module documentation

The quotient by the pro-C residual core

Declarations

proCResidualCoreQuotient_hasOpenNormalBasisInClass