NYLL
Module

ResidualSelfCentralizingImage.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.ResidualSelfCentralizingImage
2 declarations indexed from sourceView source ↗

Module documentation

Self-centralizing finite images detect residual conjugation

A homomorphism with finite image in a full formation factors through the actual residual quotient. If its image is commutative, equality after topological abelianization of that quotient forces equality in the image. Consequently, a self-centralizing such image of an open normal subgroup detects the residual quotient conjugation action. Only the subgroup image, and not the entire ambient target, is required to belong to the formation.

Imports14
Imported by2

Declarations

theorem

map_eq_of_residualTopologicalAbelianization_eq

L44 ↗
ProCGroups.FiniteStepSolvableQuotients.map_eq_of_residualTopologicalAbelianization_eq
Documentation

Equality in the abelianized residual quotient is detected by every continuous homomorphism with commutative finite image in the formation.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian ProCGroups.ProC
universe u
variable {C : FiniteGroupClass.{u}}
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem map_eq_of_residualTopologicalAbelianization_eq [CompactSpace H]
    (hC : FiniteGroupClass.FullFormation C)
    {D : Type u} [Group D] [TopologicalSpace D] [DiscreteTopology D]
    (f : H →ₜ* D) (hImage : C f.toMonoidHom.range)
    (hcomm : ∀ x y : H, Commute (f x) (f y))
    {x y : H}
    (hxy : TopologicalAbelianization.mk (H ⧸ proCResidualCore C H)
        (QuotientGroup.mk' (proCResidualCore C H) x) =
      TopologicalAbelianization.mk (H ⧸ proCResidualCore C H)
        (QuotientGroup.mk' (proCResidualCore C H) y)) :
    f x = f y
theorem

injective_residualQuotientConjugation_of_selfCentralizing_image

L84 ↗
ProCGroups.FiniteStepSolvableQuotients.injective_residualQuotientConjugation_of_selfCentralizing_image
Documentation

A commutative finite image in the formation, whose ambient centralizer has preimage contained in N, makes actual residual conjugation faithful.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian ProCGroups.ProC
universe u
variable {C : FiniteGroupClass.{u}}
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem injective_residualQuotientConjugation_of_selfCentralizing_image
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hC : FiniteGroupClass.FullFormation C)
    {D : Type u} [Group D] [TopologicalSpace D] [DiscreteTopology D]
    (N : OpenNormalSubgroup H) (θ : H →ₜ* D)
    (hImage : C (θ.toMonoidHom.comp (N : Subgroup H).subtype).range)
    (hcomm : ∀ n m : (N : Subgroup H), Commute
      (θ (n : H)) (θ (m : H)))
    (hcentralizer : ∀ h : H, (∀ n : (N : Subgroup H), Commute
      (θ h) (θ (n : H))) → h ∈ N) :
    Function.Injective
      (residualAbelianizationQuotientConjugation hC (N : Subgroup H) N.isClosed)

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