Yamaguchi Lean 4 Library
ProCGroups.ProC.Category
ProCGroups/ProC/Category

ProCGroups.ProC.Category

3 sections | 3 files | 72 declarations

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

Basic

1 files | 40 declarations | 11 Theorem | 9 Definition | 3 Abbreviation | 2 Structure | 15 Instance
The category of pro-\(C\) groups for a fixed topological pro-\(C\) predicate.

Pullbacks

1 files | 17 declarations | 13 Theorem | 4 Definition
A pullback square in the bundled category pro-\(C\) groups.

Pushouts

1 files | 15 declarations | 11 Theorem | 4 Definition
A pushout square in the bundled category pro-\(C\) groups.