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 #
- Define procategories and prove that
Profinite
is equivalent toPro (FintypeCat)
.
Tags #
profinite
The type of profinite topological spaces.
- toCompHaus : CompHaus
The underlying compact Hausdorff space of a profinite space.
- isTotallyDisconnected : TotallyDisconnectedSpace ↑self.toCompHaus.toTop
A profinite space is totally disconnected.
Instances For
A profinite space is totally disconnected.
Construct a term of Profinite
from a type endowed with the structure of a
compact, Hausdorff and totally disconnected topological space.
Equations
- Profinite.of X = Profinite.mk (CompHaus.mk { α := X, str := inferInstance })
Instances For
Equations
- Profinite.instInhabited = { default := Profinite.of PEmpty.{u_1 + 1} }
Equations
- Profinite.hasForget₂ = CategoryTheory.InducedCategory.hasForget₂ fun (X : CategoryTheory.InducedCategory CompHaus Profinite.toCompHaus) => X.toCompHaus.toTop
Equations
- Profinite.instCoeSortType = { coe := fun (X : Profinite) => ↑X.toCompHaus.toTop }
Equations
- ⋯ = ⋯
Equations
- Profinite.instTopologicalSpaceObjForget = let_fun this := inferInstance; this
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
Equations
(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
Equations
- X.toProfiniteObj = Profinite.mk (CompHaus.mk (TopCat.of (ConnectedComponents ↑X.toTop)))
Instances For
(Implementation) The bijection of homsets to establish the reflective adjunction of Profinite spaces in compact Hausdorff spaces.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The connected_components functor from compact Hausdorff spaces to profinite spaces, left adjoint to the inclusion functor.
Equations
Instances For
Finite types are given the discrete topology.
Instances For
Equations
Equations
An explicit limit cone for a functor F : J ⥤ Profinite
, defined in terms of
CompHaus.limitCone
, which is defined in terms of TopCat.limitCone
.
Equations
- Profinite.limitCone F = { pt := Profinite.mk (CompHaus.limitCone (F.comp profiniteToCompHaus)).pt, π := { app := (CompHaus.limitCone (F.comp profiniteToCompHaus)).π.app, naturality := ⋯ } }
Instances For
The limit cone Profinite.limitCone F
is indeed a limit cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The adjunction between CompHaus.to_Profinite and Profinite.to_CompHaus
Equations
Instances For
The category of profinite sets is reflective in the category of compact Hausdorff spaces
Equations
Equations
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.
Equations
Instances For
Equations
Construct an isomorphism from a homeomorphism.
Equations
- Profinite.isoOfHomeo f = CategoryTheory.asIso { toFun := ⇑f, continuous_toFun := ⋯ }
Instances For
Construct a homeomorphism from an isomorphism.
Equations
- Profinite.homeoOfIso f = CompHaus.homeoOfIso (profiniteToCompHaus.mapIso f)
Instances For
The equivalence between isomorphisms in Profinite
and homeomorphisms
of topological spaces.
Equations
- Profinite.isoEquivHomeo = { toFun := Profinite.homeoOfIso, invFun := Profinite.isoOfHomeo, left_inv := ⋯, right_inv := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯