Module

SigmaMaximalQuotient.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaMaximalQuotient

2 declarations indexed from sourceView source ↗

Module documentation

Abelianization-faithfulness of the maximal pro-Sigma quotient

Open subgroups and their open normal subgroups are pulled back along the actual residual projection. The maximal-quotient subgroup comparison identifies the residual quotient of each preimage with the original subgroup and preserves conjugation. Thus Sigma-abelianization-faithfulness gives ordinary abelianization-faithfulness of the maximal pro-Sigma quotient.

Imports14

Imported by3

theorem

quotient_action_injective_of_residual_preimage

L38 ↗

ProCGroups.FiniteStepSolvableQuotients.quotient_action_injective_of_residual_preimage

Source context 3 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.ProC ProCGroups.Abelian
universe u

Lean source · statement

theorem quotient_action_injective_of_residual_preimage
    {C : FiniteGroupClass.{u}}
    {G Q : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]
    (hC : FiniteGroupClass.FullFormation C)
    (π : G →ₜ* Q) (hπ : IsMaximalProCQuotient C π.toMonoidHom)
    (N : OpenNormalSubgroup Q)
    (hfaith : Function.Injective
      (residualAbelianizationQuotientConjugation hC
        ((N : Subgroup Q).comap π.toMonoidHom)
        (N.isClosed.preimage π.continuous_toFun))) :
    Function.Injective
      (quotientConjugationTopologicalAbelianizationMap (N := (N : Subgroup Q)))

theorem

isAbFaithful_residualQuotient

L83 ↗

ProCGroups.FiniteStepSolvableQuotients.IsSigmaAbFaithful.isAbFaithful_residualQuotient

Documentation

The actual maximal pro-Sigma quotient of a Sigma-abelianization-faithful profinite group is abelianization-faithful.