Yamaguchi Lean 4 Library
ProCGroups.Abelian
ProCGroups/Abelian

ProCGroups.Abelian

3 sections | 3 files | 89 declarations

This module develops finite quotient, subgroup, free pro-\(C\), generation, and cardinal-invariant constructions for profinite and pro-\(C\) groups.

TopologicalAbelianization

1 files | 24 declarations | 16 Theorem | 6 Definition | 1 Abbreviation | 1 Instance
The natural continuous quotient map to the topological abelianization.

TopologicalAbelianizationFunctoriality

1 files | 46 declarations | 23 Theorem | 14 Definition | 3 Abbreviation | 2 Structure | 4 Instance
Bundled commutative \(T_1\) topological groups with continuous homomorphisms.

TopologicalAbelianizationLimits

1 files | 19 declarations | 11 Theorem | 6 Definition | 2 Instance
The stagewise inverse system obtained by applying topological abelianization.