Module

ResidualMonotonicity.lean

Nyll.ProCGroups.ProC.MaximalQuotients.ResidualMonotonicity

4 declarations indexed from sourceView source ↗

Module documentation

Residual quotients under inclusion of finite-group classes

Enlarging the finite-group class decreases its residual core. The identity on the original group therefore induces a continuous surjection from the larger-class residual quotient onto the smaller-class residual quotient. This follows directly from the defining families of kernels and requires neither a formation hypothesis nor compactness.

Imports5

Nyll.ProCGroups.ProC.MaximalQuotients.ResidualCore
Nyll.ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
Nyll.ProCGroups.Topologies.QuotientMaps
Mathlib.GroupTheory.QuotientGroup.Basic
Mathlib.Topology.Algebra.ContinuousMonoidHom

Imported by2

theorem

proCResidualCore_antitone

L31 ↗

ProCGroups.ProC.proCResidualCore_antitone

Documentation

Inclusion of finite-group classes reverses inclusion of residual cores.

Source context 4 commands

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

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

Lean source · statement

theorem proCResidualCore_antitone
    (hCD : ∀ {Q : Type u} [Group Q], C Q → D Q) :
    proCResidualCore D G ≤ proCResidualCore C G

def

residualQuotientMapOfClassInclusion

L50 ↗

ProCGroups.ProC.residualQuotientMapOfClassInclusion

Documentation

The identity on the group induces the actual quotient map for an inclusion of finite-group classes.

Source context 4 commands

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

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

Lean source · statement

def residualQuotientMapOfClassInclusion
    (hCD : ∀ {Q : Type u} [Group Q], C Q → D Q) :
    G ⧸ proCResidualCore D G →ₜ* G ⧸ proCResidualCore C G

theorem

residualQuotientMapOfClassInclusion_apply_mk

L59 ↗

ProCGroups.ProC.residualQuotientMapOfClassInclusion_apply_mk

Documentation

The class-inclusion map retains the original group representative.

Source context 4 commands

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

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

Lean source · statement

theorem residualQuotientMapOfClassInclusion_apply_mk
    (hCD : ∀ {Q : Type u} [Group Q], C Q → D Q) (x : G) :
    residualQuotientMapOfClassInclusion hCD
        (QuotientGroup.mk' (proCResidualCore D G) x) =
      QuotientGroup.mk' (proCResidualCore C G) x

theorem

residualQuotientMapOfClassInclusion_surjective

L67 ↗

ProCGroups.ProC.residualQuotientMapOfClassInclusion_surjective

Documentation

Every class in the smaller-class quotient has the same representative in the larger-class quotient.

Source context 4 commands

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

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

Lean source · statement

theorem residualQuotientMapOfClassInclusion_surjective
    (hCD : ∀ {Q : Type u} [Group Q], C Q → D Q) :
    Function.Surjective (residualQuotientMapOfClassInclusion (G := G) hCD)

Module documentation

Residual quotients under inclusion of finite-group classes

Declarations

proCResidualCore_antitone

residualQuotientMapOfClassInclusion

residualQuotientMapOfClassInclusion_apply_mk

residualQuotientMapOfClassInclusion_surjective