Yamaguchi Lean 4 Library
ProCGroups.FreeProC.Characterization
ProCGroups/FreeProC/Characterization

ProCGroups.FreeProC.Characterization

4 sections | 4 files | 43 declarations

Wrapper for the ProCGroups.FreeProC.Characterization folder.

EmbeddingProblems

1 files | 18 declarations | 14 Definition | 1 Abbreviation | 3 Structure
A subgroup is minimal normal if it is nontrivial, normal, and has no proper nontrivial normal subgroup below it.

FreenessAndLifting

1 files | 2 declarations | 2 Theorem
Weak solvability reduces to the finite minimal normal kernel case when the reduction step is supplied explicitly.

InverseLimitTowers

1 files | 18 declarations | 6 Theorem | 4 Definition | 1 Abbreviation | 2 Structure | 5 Instance
A countable surjective inverse system of free pro-\(C\) groups. This record stores the transition maps for all m \(\le\) n, together with the identity and composition laws. Its ...

Quasifree

1 files | 5 declarations | 5 Definition
An abstract group has a generating set of cardinality \(\kappa\). This is not the right rank condition for quasifree profinite groups; use HasTopologicalGeneratingSetOfCardinali...