Yamaguchi Lean 4 Library
ProCGroups.Categorical
ProCGroups/Categorical

ProCGroups.Categorical

5 sections | 5 files | 243 declarations

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

AlgebraicPullbacks

1 files | 66 declarations | 49 Theorem | 16 Definition | 1 Abbreviation
Concrete pullback subgroup of \(\beta_1\) and \(\beta_2\).

ProfinitePullbacks

1 files | 42 declarations | 33 Theorem | 8 Definition | 1 Abbreviation
Continuous pullback carrier attached to two continuous homomorphisms.

PullbackComparison

1 files | 21 declarations | 18 Theorem | 3 Definition
The canonical comparison map from an abstract profinite pullback square to the concrete pullback.

PushoutSquares

1 files | 50 declarations | 32 Theorem | 14 Definition | 2 Abbreviation | 1 Structure | 1 Instance
The abstract free product used as the carrier before imposing pushout relations.

QuotientPullbackEquivalences

1 files | 64 declarations | 48 Theorem | 15 Definition | 1 Instance
An infimum of normal subgroups is normal.