Yamaguchi Lean 4 Library
ProCGroups.Completion
ProCGroups/Completion

ProCGroups.Completion

7 sections | 7 files | 206 declarations

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

FiniteQuotientLifts

1 files | 5 declarations | 3 Theorem | 2 Definition
Unique lifting property against finite discrete \(C\)-quotients of the source.

FiniteQuotientSystems

1 files | 21 declarations | 8 Theorem | 4 Definition | 1 Abbreviation | 2 Structure | 6 Instance
Normal subgroups whose corresponding quotient belongs to the chosen class \(C\).

ProCGroupAlgebra

1 files | 62 declarations | 22 Theorem | 11 Definition | 5 Abbreviation | 1 Structure | 23 Instance
The completed group-algebra indexing set records the open-normal quotient coordinate.

ProCInteger

1 files | 85 declarations | 42 Theorem | 15 Definition | 3 Abbreviation | 1 Structure | 24 Instance
A coefficient level: a positive modulus whose additive cyclic group is in \(C\).

ProCIntegerPrimePower

1 files | 10 declarations | 9 Theorem | 1 Definition
Pro C Groups / Completion / Prime-Power pro-C Integer.

SameFiniteQuotients

1 files | 11 declarations | 7 Theorem | 2 Definition | 1 Structure | 1 Class
Two abstract groups have the same finite quotients when they have exactly the same finite surjective homomorphic images.

UniversalProperty

1 files | 12 declarations | 8 Theorem | 3 Definition | 1 Structure
An abstract pro-\(C\) completion of a topological group.