ProCGroups.ProC.quotientConjugationTopologicalAbelianizationMap_injective_of_residual
Faithfulness on an abelianized residual quotient implies ordinary abelianization-faithfulness of the same relative quotient.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups.ProC
open ProCGroups.Abelian
universe uLean source · statement
theorem quotientConjugationTopologicalAbelianizationMap_injective_of_residual
{C : FiniteGroupClass.{u}} {G : Type u}
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(hC : FiniteGroupClass.FullFormation C)
(N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G))
(hfaith : Function.Injective (residualAbelianizationQuotientConjugation hC N hN)) :
Function.Injective (quotientConjugationTopologicalAbelianizationMap N)