ProCGroups.FiniteStepSolvableQuotients.isSigmaAbFaithful_iff_isAbFaithful_of_proSigma
On a pro-Sigma group, Sigma-abelianization-faithfulness is equivalent to ordinary abelianization-faithfulness. No nonemptiness of Sigma is needed.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.ProC
universe uLean source · statement
theorem isSigmaAbFaithful_iff_isAbFaithful_of_proSigma
{sigma : Set ℕ} {G : Type u}
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(hpro : HasOpenNormalBasisInClass (FiniteGroupClass.sigmaGroup sigma) G) :
IsSigmaAbFaithful sigma G ↔ IsAbFaithful G