ProCGroups.ProC.InverseLimits

3 sections | 3 files | 32 declarations

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

FiniteQuotients

1 files | 11 declarations | 11 Theorem

Any finite discrete group already lying in the class \(C\) is pro-\(C\).

1 files | 3 declarations | 2 Theorem | 1 Instance

The constructed object carries the topological space structure inherited from its construction.

1 files | 18 declarations | 12 Theorem | 6 Definition

Pronilpotent profinite groups, characterized by nilpotent finite quotients.