Module

SubgroupComparison.lean

Nyll.ProCGroups.ProC.MaximalQuotients.SubgroupComparison

5 declarations indexed from sourceView source ↗

Module documentation

Subgroups of maximal pro-C quotients

The kernel of a maximal pro-C quotient is the concrete residual core. For a closed subgroup of the quotient, its preimage has the same residual kernel. Consequently its residual quotient is continuously isomorphic to the chosen subgroup. In particular, this applies to open subgroups of maximal pro-p quotients without making any claim about arbitrary open subgroups of the source.

Imports3

Imported by3

theorem

ker_eq_proCResidualCore

L34 ↗

ProCGroups.ProC.IsMaximalProCQuotient.ker_eq_proCResidualCore

Documentation

The universal maximal quotient has exactly the residual core as its kernel.

Source context 6 commands

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

open scoped Topology
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]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
  [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]

Lean source · statement

theorem IsMaximalProCQuotient.ker_eq_proCResidualCore
    (hC : FiniteGroupClass.FullFormation C)
    (π : G →ₜ* Q) (hπ : IsMaximalProCQuotient C π.toMonoidHom) :
    π.toMonoidHom.ker = proCResidualCore C G

theorem

proCResidualCore_preimage_eq_ker

L59 ↗

ProCGroups.ProC.proCResidualCore_preimage_eq_ker

Documentation

The residual core of a closed subgroup preimage is the kernel of the restricted maximal quotient map.

Source context 6 commands

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

open scoped Topology
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]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
  [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]

Lean source · statement

theorem proCResidualCore_preimage_eq_ker
    (hC : FiniteGroupClass.FullFormation C)
    (π : G →ₜ* Q) (hπ : IsMaximalProCQuotient C π.toMonoidHom)
    (U : Subgroup Q) (hU : IsClosed (U : Set Q)) :
    proCResidualCore C (U.comap π.toMonoidHom) =
      (ContinuousMonoidHom.restrictPreimage π U).toMonoidHom.ker

def

residualQuotientPreimageContinuousMulEquiv

L85 ↗

ProCGroups.ProC.residualQuotientPreimageContinuousMulEquiv

Documentation

The residual quotient of the preimage of a closed subgroup of a maximal pro-C quotient is continuously isomorphic to that subgroup.

Source context 6 commands

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

open scoped Topology
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]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
  [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]

Lean source · statement

def residualQuotientPreimageContinuousMulEquiv
    (hC : FiniteGroupClass.FullFormation C)
    (π : G →ₜ* Q) (hπ : IsMaximalProCQuotient C π.toMonoidHom)
    (U : Subgroup Q) (hU : IsClosed (U : Set Q)) :
    (U.comap π.toMonoidHom) ⧸ proCResidualCore C (U.comap π.toMonoidHom) ≃ₜ* U

theorem

residualQuotientPreimageContinuousMulEquiv_apply_mk

L111 ↗

ProCGroups.ProC.residualQuotientPreimageContinuousMulEquiv_apply_mk

Documentation

The comparison is the restriction of the original quotient on representatives.

Source context 6 commands

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

open scoped Topology
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]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
  [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]

Lean source · statement

theorem residualQuotientPreimageContinuousMulEquiv_apply_mk
    (hC : FiniteGroupClass.FullFormation C)
    (π : G →ₜ* Q) (hπ : IsMaximalProCQuotient C π.toMonoidHom)
    (U : Subgroup Q) (hU : IsClosed (U : Set Q))
    (x : U.comap π.toMonoidHom) :
    residualQuotientPreimageContinuousMulEquiv hC π hπ U hU
        (QuotientGroup.mk' (proCResidualCore C (U.comap π.toMonoidHom)) x) =
      ContinuousMonoidHom.restrictPreimage π U x

theorem

restrictPreimage

L123 ↗

ProCGroups.ProC.IsMaximalProCQuotient.restrictPreimage

Documentation

Restricting a maximal quotient to the preimage of a closed subgroup again satisfies the full maximal-quotient universal property.

Source context 6 commands

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

open scoped Topology
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]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
  [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]

Lean source · statement

theorem IsMaximalProCQuotient.restrictPreimage
    (hC : FiniteGroupClass.FullFormation C)
    (π : G →ₜ* Q) (hπ : IsMaximalProCQuotient C π.toMonoidHom)
    (U : Subgroup Q) [CompactSpace U] :
    IsMaximalProCQuotient C (Q := U)
      (ContinuousMonoidHom.restrictPreimage π U).toMonoidHom

Module documentation

Subgroups of maximal pro-C quotients

Declarations

ker_eq_proCResidualCore

proCResidualCore_preimage_eq_ker

residualQuotientPreimageContinuousMulEquiv

residualQuotientPreimageContinuousMulEquiv_apply_mk

restrictPreimage