Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaAbelianNormalObstruction

Module documentation

Abelian normal subgroups obstruct Sigma-faithfulness

An abelian normal subgroup meeting a prime-order relative quotient nontrivially acts trivially on the residual abelianization when that prime is excluded. The commutator power identity and the required power injectivity are proved for the actual subgroup, quotient and conjugation maps.

theorem

not_isSigmaAbFaithful_of_abelian_normal_prime_quotient

L29 ↗

ProCGroups.FiniteStepSolvableQuotients.not_isSigmaAbFaithful_of_abelian_normal_prime_quotient

Documentation

A prime-order finite quotient detected by an abelian normal subgroup prevents Sigma-abelianization-faithfulness when its prime is excluded.

Source context 4 commands

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

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

Lean source · statement

theorem not_isSigmaAbFaithful_of_abelian_normal_prime_quotient
    {sigma : Set ℕ} {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (r : ℕ) [Fact r.Prime] (hr : r ∉ sigma)
    (I : Subgroup G) [I.Normal] [IsMulCommutative I]
    (N : OpenNormalSubgroup G)
    (hcard : Nat.card (G ⧸ (N : Subgroup G)) = r)
    (hI : ¬ I ≤ (N : Subgroup G)) :
    ¬ IsSigmaAbFaithful sigma G

Module documentation

Abelian normal subgroups obstruct Sigma-faithfulness

Declarations

not_isSigmaAbFaithful_of_abelian_normal_prime_quotient