NYLL
Module

ResidualAbelianizationMonotonicity.lean

Nyll.ProCGroups.ProC.MaximalQuotients.ResidualAbelianizationMonotonicity
5 declarations indexed from sourceView source ↗

Module documentation

Class inclusion and faithful residual abelianization actions

The actual quotient map induced by an inclusion of finite-group classes remains surjective after topological abelianization. It intertwines the same ambient conjugation on both residual quotients. Consequently an action detected by the smaller class is also detected by the larger class.

Imports7
Imported by3

Declarations

def

residualAbelianizationMapOfClassInclusion

L35 ↗
ProCGroups.ProC.residualAbelianizationMapOfClassInclusion
Documentation

Inclusion of finite-group classes induces the actual continuous map between the abelianized residual quotients.

Source context 5 commands

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

namespace ProCGroups.ProC
open ProCGroups.Abelian
universe u
variable {C D : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def residualAbelianizationMapOfClassInclusion
    (hCD : ∀ {Q : Type u} [Group Q], C Q → D Q) :
    TopologicalAbelianization (G ⧸ proCResidualCore D G) →ₜ*
      TopologicalAbelianization (G ⧸ proCResidualCore C G)
theorem

residualAbelianizationMapOfClassInclusion_apply_mk

L42 ↗
ProCGroups.ProC.residualAbelianizationMapOfClassInclusion_apply_mk
Documentation

The abelianized class-inclusion map retains the original representative.

Source context 5 commands

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

namespace ProCGroups.ProC
open ProCGroups.Abelian
universe u
variable {C D : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem residualAbelianizationMapOfClassInclusion_apply_mk
    (hCD : ∀ {Q : Type u} [Group Q], C Q → D Q) (x : G) :
    residualAbelianizationMapOfClassInclusion hCD
        (TopologicalAbelianization.mk (G ⧸ proCResidualCore D G)
          (QuotientGroup.mk' (proCResidualCore D G) x)) =
      TopologicalAbelianization.mk (G ⧸ proCResidualCore C G)
        (QuotientGroup.mk' (proCResidualCore C G) x)
theorem

residualAbelianizationMapOfClassInclusion_surjective

L53 ↗
ProCGroups.ProC.residualAbelianizationMapOfClassInclusion_surjective
Documentation

The actual map between abelianized residual quotients is surjective.

Source context 5 commands

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

namespace ProCGroups.ProC
open ProCGroups.Abelian
universe u
variable {C D : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem residualAbelianizationMapOfClassInclusion_surjective
    (hCD : ∀ {Q : Type u} [Group Q], C Q → D Q) :
    Function.Surjective (residualAbelianizationMapOfClassInclusion (G := G) hCD)
theorem

residualAbelianizationMapOfClassInclusion_conjugation

L64 ↗
ProCGroups.ProC.residualAbelianizationMapOfClassInclusion_conjugation
Documentation

Class inclusion commutes with actual conjugation by the same ambient element on both abelianized residual quotients of a normal subgroup.

Source context 6 commands

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

namespace ProCGroups.ProC
open ProCGroups.Abelian
universe u
variable {C D : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem residualAbelianizationMapOfClassInclusion_conjugation
    (hC : FiniteGroupClass.FullFormation C) (hD : FiniteGroupClass.FullFormation D)
    (hCD : ∀ {Q : Type u} [Group Q], C Q → D Q)
    (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G)) (g : G)
    (a : TopologicalAbelianization (N ⧸ proCResidualCore D N)) :
    residualAbelianizationMapOfClassInclusion hCD
        (TopologicalAbelianization.congr
          (residualQuotientConjugationContinuousMulEquiv hD N hN g) a) =
      TopologicalAbelianization.congr
        (residualQuotientConjugationContinuousMulEquiv hC N hN g)
        (residualAbelianizationMapOfClassInclusion hCD a)
theorem

residualAbelianizationQuotientConjugation_injective_of_class_inclusion

L84 ↗
ProCGroups.ProC.residualAbelianizationQuotientConjugation_injective_of_class_inclusion
Documentation

Faithfulness detected by a finite-group class persists upon enlarging that class, using the constructed equivariant surjection.

Source context 6 commands

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

namespace ProCGroups.ProC
open ProCGroups.Abelian
universe u
variable {C D : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem residualAbelianizationQuotientConjugation_injective_of_class_inclusion
    (hC : FiniteGroupClass.FullFormation C) (hD : FiniteGroupClass.FullFormation D)
    (hCD : ∀ {Q : Type u} [Group Q], C Q → D Q)
    (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G))
    (hfaith : Function.Injective (residualAbelianizationQuotientConjugation hC N hN)) :
    Function.Injective (residualAbelianizationQuotientConjugation hD N hN)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.