NYLL
Module

ResidualProGroupFaithfulness.lean

Nyll.ProCGroups.ProC.MaximalQuotients.ResidualProGroupFaithfulness
2 declarations indexed from sourceView source ↗

Module documentation

Ordinary faithfulness for pro-C subgroups

The identity map of a pro-C group kills its residual core, so that core is trivial. The resulting actual quotient retraction carries residual conjugation back to ordinary conjugation on topological abelianizations.

Imports11
Imported by2

Declarations

theorem

proCResidualCore_eq_bot_of_hasOpenNormalBasisInClass

L38 ↗
ProCGroups.ProC.proCResidualCore_eq_bot_of_hasOpenNormalBasisInClass
Documentation

A compact Hausdorff pro-C group has trivial residual core.

Source context 4 commands

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

namespace ProCGroups.ProC
open ProCGroups.Abelian
universe u
variable {C : FiniteGroupClass.{u}} {G : Type u}
  [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G]
Lean source · statement
theorem proCResidualCore_eq_bot_of_hasOpenNormalBasisInClass
    (hC : FiniteGroupClass.Hereditary C)
    (hG : HasOpenNormalBasisInClass C G) : proCResidualCore C G = ⊥
theorem

residualAbelianizationQuotientConjugation_injective_of_ordinary_of_proC

L51 ↗
ProCGroups.ProC.residualAbelianizationQuotientConjugation_injective_of_ordinary_of_proC
Documentation

For a pro-C normal subgroup, ordinary quotient-conjugation faithfulness implies faithfulness on its actual abelianized residual quotient.

Source context 5 commands

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

namespace ProCGroups.ProC
open ProCGroups.Abelian
universe u
variable {C : FiniteGroupClass.{u}} {G : Type u}
  [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G]
variable [TotallyDisconnectedSpace G]
Lean source · statement
theorem residualAbelianizationQuotientConjugation_injective_of_ordinary_of_proC
    (hC : FiniteGroupClass.FullFormation C)
    (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G))
    (hpro : HasOpenNormalBasisInClass C N)
    (hfaith : Function.Injective (quotientConjugationTopologicalAbelianizationMap N)) :
    Function.Injective (residualAbelianizationQuotientConjugation hC N hN)

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