Module

ResidualUniversalProperty.lean

Nyll.ProCGroups.ProC.MaximalQuotients.ResidualUniversalProperty

2 declarations indexed from sourceView source ↗

Module documentation

The canonical residual quotient is maximal pro-C

The actual residual quotient has the required pro-C basis. Every continuous map to a pro-C group factors through its residual core, and surjectivity of the quotient projection gives uniqueness of this factorization.

Imports5

Imported by2

theorem

residualQuotient_totallyDisconnectedSpace

L27 ↗

ProCGroups.ProC.residualQuotient_totallyDisconnectedSpace

Source context 3 commands

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

namespace ProCGroups.ProC
universe u
attribute [local instance] proCResidualCore_isClosed

Lean source · statement

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

theorem

isMaximalProCQuotient_residualCore

L40 ↗

ProCGroups.ProC.isMaximalProCQuotient_residualCore

Documentation

The canonical residual-core projection satisfies the maximal pro-C universal property. The quotient's separation properties are supplied from closedness of the actual core, rather than assumed.

Source context 4 commands