The category of Profinite Types #
We construct the category of profinite topological spaces, often called profinite sets -- perhaps they could be called profinite types in Lean.
The type of profinite topological spaces is called Profinite
. It has a category
instance and is a fully faithful subcategory of TopCat
. The fully faithful functor
is called Profinite.toTop
.
Implementation notes #
A profinite type is defined to be a topological space which is compact, Hausdorff and totally disconnected.
TODO #
- Link to category of projective limits of finite discrete sets.
- finite coproducts
- Clausen/Scholze topology on the category
Profinite
.
Tags #
profinite
- toCompHaus : CompHaus
The underlying compact Hausdorff space of a profinite space.
- IsTotallyDisconnected : TotallyDisconnectedSpace ↑s.toCompHaus.toTop
A profinite space is totally disconnected.
The type of profinite topological spaces.
Instances For
Construct a term of Profinite
from a type endowed with the structure of a
compact, Hausdorff and totally disconnected topological space.
Instances For
(Implementation) The object part of the connected_components functor from compact Hausdorff spaces to Profinite spaces, given by quotienting a space by its connected components. See: https://stacks.math.columbia.edu/tag/0900
Instances For
(Implementation) The bijection of homsets to establish the reflective adjunction of Profinite spaces in compact Hausdorff spaces.
Instances For
The connected_components functor from compact Hausdorff spaces to profinite spaces, left adjoint to the inclusion functor.
Instances For
Finite types are given the discrete topology.
Instances For
An explicit limit cone for a functor F : J ⥤ Profinite
, defined in terms of
CompHaus.limitCone
, which is defined in terms of TopCat.limitCone
.
Instances For
The limit cone Profinite.limitCone F
is indeed a limit cone.
Instances For
The adjunction between CompHaus.to_Profinite and Profinite.to_CompHaus
Instances For
The category of profinite sets is reflective in the category of compact Hausdorff spaces
Any morphism of profinite spaces is a closed map.
Any continuous bijection of profinite spaces induces an isomorphism.
Any continuous bijection of profinite spaces induces an isomorphism.