ProCGroups

The natural continuous quotient map to the topological abelianization.

Concrete pullback subgroup of \(\beta_1\) and \(\beta_2\).

Unique lifting property against finite discrete \(C\)-quotients of the source.

This module formalizes elementary duality constructions for profinite groups.

Finitely generated as a topological group.

The class of all finite groups.

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

This module formalizes Frattini-type constructions for profinite groups.

A finite nontrivial \(p\)-group has a nontrivial central element. This is the group-theoretic core used for finite normal subgroups in pro-\(p\) amalgam arguments.

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.

The abstract group underlying the binary free product of the two factors.

X topologically generates G if the abstract subgroup generated by X is dense in G.

The centralizer of a set of elements.

An inverse system of topological spaces indexed by a preorder.

The cardinality of a family of subsets is viewed as a subtype.

A group is noncommutative when its abstract commutator subgroup is nontrivial.

Closed subgroups have a top element: the whole group.

The closed normal subgroup generated by a set of profinite relators.

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

An unbundled profinite group is a compact Hausdorff totally disconnected topological group.

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

Conjugation by an ambient element as a continuous automorphism of a normal subgroup.

This module formalizes permutational wreath products.