Module

SigmaProPNormal.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaProPNormal

1 declaration indexed from sourceView source ↗

Module documentation

Sigma-faithfulness excludes normal pro-p subgroups

For an excluded prime, a normal pro-p subgroup acts trivially on the actual maximal pro-Sigma quotient of every open normal subgroup. Sigma-faithfulness puts it inside every open normal subgroup, whose intersection is trivial.

Imports5

Imported by1

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.All

theorem

normal_proP_eq_bot

L29 ↗

ProCGroups.FiniteStepSolvableQuotients.IsSigmaAbFaithful.normal_proP_eq_bot

Documentation

A Sigma-abelianization-faithful profinite group has no nontrivial normal pro-p subgroup when p is outside Sigma. Closedness of the subgroup is unnecessary.

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 IsSigmaAbFaithful.normal_proP_eq_bot
    {sigma : Set ℕ} {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : IsSigmaAbFaithful sigma G)
    (p : ℕ) [Fact p.Prime] (hp : p ∉ sigma)
    (P : Subgroup G) [P.Normal]
    (hP : HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) P) :
    P = ⊥

Module documentation

Sigma-faithfulness excludes normal pro-p subgroups

Declarations

normal_proP_eq_bot