theorem
L33 ↗openSubgroup
ProCGroups.FiniteStepSolvableQuotients.IsSigmaAbFaithful.openSubgroup
Every open subgroup of a Sigma-abelianization-faithful profinite group is Sigma-abelianization-faithful.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.ProC
universe uLean source · full declaration
theorem IsSigmaAbFaithful.openSubgroup {sigma : Set ℕ} {G : Type u}
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(hG : IsSigmaAbFaithful sigma G) (U : OpenSubgroup G) :
letI : CompactSpace (U : Subgroup G) :=
U.isClosed.isClosedEmbedding_subtypeVal.compactSpace
IsSigmaAbFaithful sigma (U : Subgroup G) := by
have : CompactSpace (U : Subgroup G) :=
U.isClosed.isClosedEmbedding_subtypeVal.compactSpace
intro H
have : CompactSpace (H : Subgroup (U : Subgroup G)) :=
H.isClosed.isClosedEmbedding_subtypeVal.compactSpace
intro N
let Hmap : OpenSubgroup G :=
{ toSubgroup := (H : Subgroup (U : Subgroup G)).map (U : Subgroup G).subtype
isOpen' := U.isOpen.isOpenMap_subtype_val _ H.isOpen }
have : CompactSpace (Hmap : Subgroup G) :=
Hmap.isClosed.isClosedEmbedding_subtypeVal.compactSpace
let e : (H : Subgroup (U : Subgroup G)) ≃* (Hmap : Subgroup G) :=
(H : Subgroup (U : Subgroup G)).equivMapOfInjective
(U : Subgroup G).subtype Subtype.val_injective
have he : Continuous e :=
Continuous.subtype_mk (continuous_subtype_val.comp continuous_subtype_val) _
let t : (H : Subgroup (U : Subgroup G)) ≃ₜ* (Hmap : Subgroup G) :=
{ toMulEquiv := e
continuous_toFun := he
continuous_invFun :=
(e.toEquiv.toHomeomorphOfContinuousClosed he he.isClosedMap).continuous_invFun }
let Nmap : OpenNormalSubgroup (Hmap : Subgroup G) :=
ProCGroups.ProC.OpenNormalSubgroup.map
(ContinuousMonoidHom.toContinuousMonoidHom t)
t.toHomeomorph.isOpenMap t.surjective N
exact (residualAbelianizationQuotientConjugation_injective_map_iff
(FiniteGroupClass.sigmaGroup_fullFormation sigma) t
(N : Subgroup (H : Subgroup (U : Subgroup G))) N.isClosed).mp (hG Hmap Nmap)