Yamaguchi Lean 4 Library
ProCGroups.Generation
ProCGroups/Generation

ProCGroups.Generation

7 sections | 7 files | 103 declarations

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

Basic

1 files | 32 declarations | 25 Theorem | 7 Definition
X topologically generates G if the abstract subgroup generated by X is dense in G.

Convergence

1 files | 9 declarations | 8 Theorem | 1 Definition
A continuous map between topological groups that sends \(1\) to \(1\) carries convergent sets to convergent sets, provided the source is profinite.

GeneratingFamilies

1 files | 4 declarations | 1 Theorem | 1 Definition | 1 Structure | 1 Instance
An indexed topological generating family converging to \(1\). This is deliberately weaker than a free pro-\(C\) basis: it records only generation and convergence of the image.

GeneratorConvergingPairs

1 files | 9 declarations | 4 Theorem | 2 Definition | 1 Structure | 2 Instance
A partial generating set together with a closed normal subgroup modulo which it converges.

QuotientCriteria

1 files | 3 declarations | 3 Theorem
Topological generation in a surjective inverse system can be checked after every projection.

QuotientGeneratorConvergingPairs

1 files | 36 declarations | 22 Theorem | 9 Definition | 1 Abbreviation | 1 Structure | 3 Instance
A quotient generator converging pair records compatible source and quotient generator data.

WordProductsAndClosure

1 files | 10 declarations | 10 Theorem
The identity element belongs to the word-product set.