ProCGroups.FreeProC

9 sections | 15 files | 249 declarations

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

Abelianization

1 files | 1 declarations | 1 Theorem

A finite cyclic coordinate on the topological abelianization of a finite-rank free pro-\(\Sigma\) group, sending one chosen basis element to the standard generator.

Basic

Free pro-\(C\) groups via a strengthened universal property. The lifting property quantifies over all continuous maps into pro-\(C\) groups, rather than only maps whose image ge...

CanonicalData

1 files | 8 declarations | 6 Theorem | 1 Definition | 1 Structure

The usual \(\delta\)-basis map into a direct product.

Characterization

Wrapper for the `ProCGroups.FreeProC.Characterization` folder.

Constructions

1 files | 3 declarations | 3 Theorem

A maximal pro-\(C'\) quotient of a pointed free pro-\(C\) group is again pointed free on the same pointed space. This version fixes a chosen maximal quotient map \(\pi : F \to Q...

Criteria

Wrapper for the `ProCGroups.FreeProC.Criteria` folder.

FinitelyGenerated

1 files | 19 declarations | 14 Theorem | 3 Definition | 2 Structure

For a finite basis and a concrete finite-group class, every target map has a unique continuous lift. This is the finite-rank replacement for repeatedly supplying the automatic c...

SolvableQuotients

1 files | 6 declarations | 3 Theorem | 3 Definition

The endomorphism induced by collapseToFinset on a maximal solvable quotient.

Spaces

1 files | 5 declarations | 2 Theorem | 1 Definition | 2 Structure

The underlying space of a free pro-\(C\) group is profinite when the group is profinite.