ProCGroups.ProC

9 sections | 38 files | 450 declarations

This module formalizes the category and quotient theory of pro-\(C\) groups.

Category

4 files | 72 declarations | 35 Theorem | 17 Definition | 3 Abbreviation | 2 Structure | 15 Instance

The category of pro-\(C\) groups for a fixed topological pro-\(C\) predicate.

GroupPredicate

1 files | 2 declarations | 1 Structure | 1 Instance

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

GroupPredicates

4 files | 109 declarations | 45 Theorem | 40 Definition | 2 Abbreviation | 2 Structure | 9 Class | 11 Instance

Every pro-abelian group is abelian.

InverseLimits

4 files | 32 declarations | 25 Theorem | 6 Definition | 1 Instance

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

Kernels

1 files | 16 declarations | 9 Theorem | 2 Definition | 5 Abbreviation

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

MaximalQuotients

4 files | 17 declarations | 11 Theorem | 2 Definition | 4 Structure

Maximal pro-\(C\) quotient groups via their universal property.

OpenNormalSubgroups

10 files | 136 declarations | 102 Theorem | 26 Definition | 1 Abbreviation | 2 Structure | 5 Instance

Open normal subgroups have a top element: the whole group.

Quotients

7 files | 49 declarations | 36 Theorem | 10 Definition | 1 Structure | 2 Instance

If \(G\) is pro-\(C\) and \(C\) is closed under quotients, then every quotient of \(G\) by a closed normal subgroup is again pro-\(C\). The proof reconstructs \(G/K\) as the inv...

Subgroups

3 files | 17 declarations | 17 Theorem

A closed subgroup of a pro-\(C\) group is pro-\(C\).