ProCGroups

27 sections | 573 files | 6514 declarations

Reusable formalization of profinite and pro-\(C\) groups. The library covers finite-group classes, inverse systems and completions, free pro-\(C\) groups and products, generation, presentations, duality, topologies, and wreath products.

ProCGrp C is the full subcategory of ProfiniteGrp cut out by the open-normal finite-quotient basis condition for C; its categorical and concrete structures are inherited from Mathlib. FiniteGroupClass includes finiteness and invariance under multiplicative equivalence, so the corresponding finite-group object property is isomorphism-invariant without extra hypotheses.

This public aggregate imports every maintained Pro-C Groups component, including the Reidemeister--Schreier, completed group algebra, Fox differential, and Crowell exact-sequence layers.

imports

Imported by

None

Abelian

4 files | 71 declarations | 44 Theorems | 23 Definitions | 1 Abbreviation | 3 Instances

This aggregate module exposes topological abelianization, its functoriality, and its compatibility with inverse limits.

Categorical

6 files | 174 declarations | 125 Theorems | 42 Definitions | 4 Abbreviations | 3 Instances

This umbrella module exports the concrete algebraic and continuous pullback, comparison, quotient-pullback, and pushout APIs.

CompletedGroupAlgebra

72 files | 697 declarations | 481 Theorems | 163 Definitions | 11 Abbreviations | 7 Structures | 35 Instances

This aggregate exports terminal-index and finite-stage augmentations, the canonical all-finite augmentation, its comparison with the \(C\)-indexed augmentation, and the complete...

Completion

6 files | 109 declarations | 62 Theorems | 20 Definitions | 2 Abbreviations | 2 Structures | 23 Instances

This is the aggregate import for pro-\(C\) completion universal properties, finite-quotient lifting, pro-\(C\) integers, and finite-quotient comparison.

CrowellExactSequence

21 files | 105 declarations | 75 Theorems | 27 Definitions | 2 Abbreviations | 1 Structure

Applications of the profinite Crowell exact sequence, including the finite-rank criterion for free pro-\(C\) presentations.

Duality

1 file | 19 declarations | 14 Theorems | 4 Definitions | 1 Instance

This module formalizes elementary duality constructions for profinite groups.

FiniteGeneration

3 files | 70 declarations | 48 Theorems | 18 Definitions | 4 Instances

This aggregate module exposes the basic theory of topologically finitely generated groups, characteristic subgroup chains, and the associated finite-index bounds.

FiniteGroups

4 files | 128 declarations | 96 Theorems | 19 Definitions | 1 Abbreviation | 6 Structures | 1 Class | 5 Instances

This module defines `FiniteGroupClass.allFinite` and proves its standard closure properties: formation, subgroup, normal-subgroup, quotient, finite-subdirect-product, extension,...

FiniteStepSolvableQuotients

10 files | 151 declarations | 105 Theorems | 13 Lemmas | 23 Definitions | 7 Abbreviations | 3 Instances

This module formalizes finite-step solvable quotients and their abelian actions.

FoxDifferential

272 files | 2956 declarations | 2053 Theorems | 618 Definitions | 100 Abbreviations | 6 Structures | 179 Instances

This module defines crossed homomorphisms for an additive group action and their scalar-character specialization. It supplies the Fox product, inverse, conjugation, commutator, ...

Frattini

1 file | 13 declarations | 11 Theorems | 2 Definitions

This module formalizes Frattini-type constructions for profinite groups.

FreeConstructions

3 files | 3 declarations | 2 Theorems | 1 Definition

The aggregate exports the concrete generating-data predicates and theorems that concatenate finite generating families to bound the rank of the ambient group.

FreeProC

14 files | 125 declarations | 82 Theorems | 33 Definitions | 1 Abbreviation | 7 Structures | 2 Instances

This module identifies the topological abelianization of a free pro-\(C\) group through its universal property and finite abelian targets.

FreeProducts

2 files | 18 declarations | 14 Theorems | 3 Definitions | 1 Structure

This aggregate exports the universal property and basic API for free pro-\(C\) products.

Generation

7 files | 107 declarations | 78 Theorems | 21 Definitions | 1 Abbreviation | 2 Structures | 5 Instances

This module defines topological generation, convergence to one, the corresponding cardinal ranks, and the finite word-product filtration of a set. It develops extensionality, cl...

GroupTheory

4 files | 22 declarations | 17 Theorems | 3 Definitions | 2 Abbreviations

Centralizer lemmas and closed-cyclic-subgroup results used by the profinite applications.

InverseSystems

14 files | 226 declarations | 116 Theorems | 64 Definitions | 1 Abbreviation | 6 Structures | 4 Classes | 35 Instances

This module defines preorder-indexed inverse systems of topological spaces and realizes their inverse limit as the subtype of compatible families. It proves the topological univ...

LocalWeight

7 files | 80 declarations | 63 Theorems | 10 Definitions | 3 Abbreviations | 2 Structures | 2 Instances

This aggregate module exposes generating families converging to the identity and the resulting cardinal invariants, subgroup chains, metrizability criteria, and quotient estimates.

NormalSubgroups

7 files | 11 declarations | 8 Theorems | 3 Definitions

This aggregate module exposes the closed-normal-subgroup framework, maximal-normal-subgroup criteria, and finite-intersection and compactness results for simple quotients.

Order

2 files | 37 declarations | 24 Theorems | 9 Definitions | 4 Instances

This aggregate module exposes the lattice operations and finite-index estimates for closed subgroups used throughout the profinite-group development.

Presentations

2 files | 12 declarations | 7 Theorems | 3 Definitions | 1 Abbreviation | 1 Instance

This aggregate exposes the canonical profinite presentation API: closed normal closures and free pro-\(C\) relator presentations.

ProC

36 files | 223 declarations | 159 Theorems | 46 Definitions | 6 Abbreviations | 3 Structures | 9 Instances

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

Profinite

3 files | 12 declarations | 11 Theorems | 1 Definition

This aggregate module exposes separation and permanence results for profinite groups and their open subgroups.

ReidemeisterSchreier

60 files | 948 declarations | 556 Theorems | 7 Lemmas | 316 Definitions | 27 Abbreviations | 17 Structures | 4 Inductive types | 19 Instances | 2 Macros

This module formalizes the classical discrete Reidemeister--Schreier theorem.

TopologicalGroups

1 file | 27 declarations | 8 Theorems | 1 Definition | 6 Abbreviations | 4 Structures | 8 Instances

This module formalizes basic topological-group constructions used by the pro-\(C\) library.

Topologies

10 files | 102 declarations | 64 Theorems | 4 Lemmas | 23 Definitions | 1 Abbreviation | 3 Structures | 7 Instances

This file bundles conjugation by a normalizing element as a continuous multiplicative equivalence. It also descends conjugation to quotients by topologically characteristic subg...

WreathProducts

1 file | 68 declarations | 39 Theorems | 17 Definitions | 2 Abbreviations | 10 Instances

This module formalizes permutational wreath products.