Yamaguchi26AbfaithfulGalois.centralizer_criterion_6_3
Centralizers of open subgroups containing D lie in the image of D.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC ProCGroups.FiniteStepSolvableQuotients
universe uLean source · statement
theorem centralizer_criterion_6_3 {G : Type u}
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(sigma : Set ℕ) (hG : IsSigmaAbFaithful sigma G)
(D : ClosedSubgroup G) [(D : Subgroup G).Normal]
(H : OpenSubgroup G) (hDH : (D : Subgroup G) ≤ (H : Subgroup G)) :
Subgroup.centralizer ((H : Subgroup G).map (QuotientGroup.mk' (sigmaResidualKernel sigma D)) :
Set (G ⧸ sigmaResidualKernel sigma D)) ≤
(D : Subgroup G).map (QuotientGroup.mk' (sigmaResidualKernel sigma D))