ProCGroups.FiniteStepSolvableQuotients.Commutators

4 sections | 4 files | 73 declarations

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

Basic

1 files | 17 declarations | 15 Theorem | 1 Definition | 1 Abbreviation

The topological closure of the abstract commutator subgroup.

1 files | 5 declarations | 4 Theorem | 1 Definition

Every element of the commutator subgroup is a product of at most \(n\) commutators.

Closed-map properties descend to the restriction to a subgroup preimage.

1 files | 7 declarations | 5 Theorem | 2 Definition

A product of commutators whose left factors lie in \(A\) and whose right factors are prescribed by \(x\).