ProCGroups.Topologies

7 sections | 9 files | 105 declarations

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

Conjugation

1 files | 4 declarations | 2 Theorem | 2 Definition

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

1 files | 11 declarations | 8 Theorem | 3 Definition

A homomorphism from a topological group to a discrete group is continuous if its kernel is open.

1 files | 9 declarations | 5 Theorem | 4 Definition

The forward continuous homomorphism on inverse limits induced by a stagewise isomorphism.

3 files | 20 declarations | 14 Theorem | 4 Definition | 2 Structure

Wrapper for the `ProCGroups.Topologies.FullSubgroupTopology` folder.

1 files | 3 declarations | 2 Theorem | 1 Definition

The \(\top\) open subgroup is canonically equivalent to the ambient topological group.

1 files | 20 declarations | 12 Theorem | 8 Definition

The comap of a quotient subgroup is determined by the representative-level map when the kernel condition holds.

Identify the image of a subgroup with its Subgroup.map.