ProCGroups.InverseSystems

13 sections | 13 files | 228 declarations

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

Basic

An inverse system of topological spaces indexed by a preorder.

1 files | 4 declarations | 2 Theorem | 2 Definition

The categorical TopCat diagram associated to a concrete inverse system.

1 files | 10 declarations | 6 Theorem | 4 Definition

Every open neighborhood in the inverse limit contains the inverse image of an open set along one projection.

1 files | 24 declarations | 19 Theorem | 4 Definition | 1 Structure

Compatibility restricted to indices below a fixed stage. This is only used to prove nonemptiness of the inverse limit.

1 files | 2 declarations | 2 Theorem

A second-countable profinite space is a sequential inverse limit of finite discrete spaces.

The constructed object carries the topological space structure inherited from its construction.

1 files | 9 declarations | 3 Theorem | 3 Definition | 3 Instance

The additive-multiplicative homeomorphism is compatible with the profinite topology and is determined by finite-quotient data.

1 files | 5 declarations | 3 Theorem | 2 Definition

The projection from a group-valued inverse limit to one component is viewed as a homomorphism.

1 files | 19 declarations | 15 Theorem | 3 Definition | 1 Abbreviation

A compact Hausdorff totally disconnected space has a basis of clopen sets.

1 files | 21 declarations | 15 Theorem | 6 Definition

The inverse system formed by the projection images of a subset of an inverse limit.

The transition map of a group-valued inverse system is bundled as a homomorphism.

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

A compatible family of stagewise continuous group isomorphisms between two concrete inverse systems.

1 files | 2 declarations | 1 Theorem | 1 Definition

A continuous bijection from a compact space to a Hausdorff space is a homeomorphism.