ProCGroups.LocalWeight

6 sections | 6 files | 94 declarations

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

CardinalInvariantsAndLocalWeight

1 files | 46 declarations | 38 Theorem | 7 Definition | 1 Abbreviation

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

Bundled closed normal subgroup data for quotient constructions.

1 files | 2 declarations | 2 Theorem

A generating set converging to \(1\) is countable exactly when the profinite group admits a countable descending open-normal chain at the identity.

1 files | 3 declarations | 3 Theorem

6.2(a). Closed generating subsets compute the local weight.

1 files | 11 declarations | 10 Theorem | 1 Definition

6. Quotient local weight at the identity coset.

1 files | 8 declarations | 5 Theorem | 2 Definition | 1 Abbreviation

A family of subgroups intended to model a chain appearing in the transfinite local-weight arguments.