The category of Compact Hausdorff Spaces #
We construct the category of compact Hausdorff spaces.
The type of compact Hausdorff spaces is denoted CompHaus
, and it is endowed with a category
instance making it a full subcategory of TopCat
.
The fully faithful functor CompHaus ⥤ TopCat
is denoted compHausToTop
.
Note: The file Topology/Category/Compactum.lean
provides the equivalence between Compactum
,
which is defined as the category of algebras for the ultrafilter monad, and CompHaus
.
CompactumToCompHaus
is the functor from Compactum
to CompHaus
which is proven to be an
equivalence of categories in CompactumToCompHaus.isEquivalence
.
See topology/category/Compactum.lean
for a more detailed discussion where these definitions are
introduced.
- toTop : TopCat
The underlying topological space of an object of
CompHaus
. - is_compact : CompactSpace ↑s.toTop
The underlying topological space is compact.
- is_hausdorff : T2Space ↑s.toTop
The underlying topological space is T2.
The type of Compact Hausdorff topological spaces.
Instances For
A constructor for objects of the category CompHaus
,
taking a type, and bundling the compact Hausdorff topology
found by typeclass inference.
Instances For
Any continuous function on compact Hausdorff spaces is a closed map.
Any continuous bijection of compact Hausdorff spaces is an isomorphism.
Any continuous bijection of compact Hausdorff spaces induces an isomorphism.
Instances For
(Implementation) The object part of the compactification functor from topological spaces to compact Hausdorff spaces.
Instances For
(Implementation) The bijection of homsets to establish the reflective adjunction of compact Hausdorff spaces in topological spaces.
Instances For
The Stone-Cech compactification functor from topological spaces to compact Hausdorff spaces, left adjoint to the inclusion functor.
Instances For
The category of compact Hausdorff spaces is reflective in the category of topological spaces.
An explicit limit cone for a functor F : J ⥤ CompHaus
, defined in terms of
TopCat.limitCone
.
Instances For
The limit cone CompHaus.limitCone F
is indeed a limit cone.