Module

ResidualIdempotence.lean

Nyll.ProCGroups.ProC.MaximalQuotients.ResidualIdempotence

3 declarations indexed from sourceView source ↗

Module documentation

The residual core has no further pro-C quotient

For a full formation, taking the residual core inside the residual core gives the whole subgroup. The proof uses closure under extensions and continuous conjugation; no finite generation or abstract characteristic-subgroup hypothesis is required.

Imports3

Imported by2

theorem

proCResidualCore_self_eq_top

L28 ↗

ProCGroups.ProC.proCResidualCore_self_eq_top

Documentation

The residual core of a profinite group's residual core is the whole subgroup.

Source context 4 commands

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

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

Lean source · statement

theorem proCResidualCore_self_eq_top
    (hC : FiniteGroupClass.FullFormation C) :
    proCResidualCore C (proCResidualCore C G) = ⊤

theorem

continuousHom_from_proCResidualCore_eq_one

L111 ↗

ProCGroups.ProC.continuousHom_from_proCResidualCore_eq_one

Documentation

Every continuous homomorphism from the residual core to a Hausdorff pro-C target is trivial.

Source context 4 commands

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

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

Lean source · statement

theorem continuousHom_from_proCResidualCore_eq_one
    (hC : FiniteGroupClass.FullFormation C)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
    (f : proCResidualCore C G →ₜ* H) (hH : HasOpenNormalBasisInClass C H)
    (r : proCResidualCore C G) : f r = 1

theorem

proCResidualCore_eq_comap_of_le

L126 ↗

ProCGroups.ProC.proCResidualCore_eq_comap_of_le

Documentation

A closed subgroup containing the ambient residual core has that same residual core, viewed as a subgroup of the smaller group.

Source context 4 commands

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

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

Lean source · statement

theorem proCResidualCore_eq_comap_of_le
    (hC : FiniteGroupClass.FullFormation C)
    (J : Subgroup G) (hJclosed : IsClosed (J : Set G))
    (hRJ : proCResidualCore C G ≤ J) :
    proCResidualCore C J = (proCResidualCore C G).comap J.subtype

Module documentation

The residual core has no further pro-C quotient

Declarations

proCResidualCore_self_eq_top

continuousHom_from_proCResidualCore_eq_one

proCResidualCore_eq_comap_of_le