ProCGroups.Boundary.isConj_iff_forall_openNormal_quotient_isConj
Two elements of a profinite group are conjugate if and only if their images are conjugate in every open-normal finite quotient.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups.Boundary
universe uLean source · statement
theorem isConj_iff_forall_openNormal_quotient_isConj
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
{x y : G} :
IsConj x y ↔
∀ U : OpenNormalSubgroup G,
IsConj
(QuotientGroup.mk' (U : Subgroup G) x)
(QuotientGroup.mk' (U : Subgroup G) y)