Extremally disconnected sets #
This file develops some of the basic theory of extremally disconnected compact Hausdorff spaces.
Overview #
This file defines the type Stonean
of all extremally (note: not "extremely"!)
disconnected compact Hausdorff spaces, gives it the structure of a large category,
and proves some basic observations about this category and various functors from it.
The Lean implementation: a term of type Stonean
is a pair, considering of
a term of type CompHaus
(i.e. a compact Hausdorff topological space) plus
a proof that the space is extremally disconnected.
This is equivalent to the assertion that the term is projective in CompHaus
,
in the sense of category theory (i.e., such that morphisms out of the object
can be lifted along epimorphisms).
Main definitions #
Stonean
: the category of extremally disconnected compact Hausdorff spaces.Stonean.toCompHaus
: the forgetful functorStonean ⥤ CompHaus
from Stonean spaces to compact Hausdorff spacesStonean.toProfinite
: the functor from Stonean spaces to profinite spaces.
Projective
implies ExtremallyDisconnected
.
Projective
implies Stonean
.
Instances For
Stonean spaces form a large category.
The (forgetful) functor from Stonean spaces to compact Hausdorff spaces.
Instances For
Construct a term of Stonean
from a type endowed with the structure of a
compact, Hausdorff and extremally disconnected topological space.
Instances For
Stonean spaces are a concrete category.
Stonean spaces are topological spaces.
Stonean spaces are compact.
Stonean spaces are Hausdorff.
The functor from Stonean spaces to profinite spaces.
Instances For
The functor from Stonean spaces to profinite spaces is full.
The functor from Stonean spaces to profinite spaces is faithful.
Construct an isomorphism from a homeomorphism.
Instances For
Construct a homeomorphism from an isomorphism.
Instances For
The equivalence between isomorphisms in Stonean
and homeomorphisms
of topological spaces.
Instances For
A finite discrete space as a Stonean space.
Instances For
Every Stonean space is projective in CompHaus
Every Stonean space is projective in Profinite
If X
is compact Hausdorff, presentation X
is a Stonean space equipped with an epimorphism
down to X
(see CompHaus.presentation.π
and CompHaus.presentation.epi_π
). It is a
"constructive" witness to the fact that CompHaus
has enough projectives.
Instances For
The morphism from presentation X
to X
.
Instances For
The morphism from presentation X
to X
is an epimorphism.
X
|
(f)
|
\/
Z ---(e)---> Y
If Z
is a Stonean space, f : X ⟶ Y
an epi in CompHaus
and e : Z ⟶ Y
is arbitrary, then
lift e f
is a fixed (but arbitrary) lift of e
to a morphism Z ⟶ X
. It exists because
Z
is a projective object in CompHaus
.
Instances For
If X
is profinite, presentation X
is a Stonean space equipped with an epimorphism down to
X
(see Profinite.presentation.π
and Profinite.presentation.epi_π
).
Instances For
The morphism from presentation X
to X
.
Instances For
The morphism from presentation X
to X
is an epimorphism.
X
|
(f)
|
\/
Z ---(e)---> Y
If Z
is a Stonean space, f : X ⟶ Y
an epi in Profinite
and e : Z ⟶ Y
is arbitrary,
then lift e f
is a fixed (but arbitrary) lift of e
to a morphism Z ⟶ X
. It is
CompHaus.lift e f
as a morphism in Profinite
.