# Extremally disconnected spaces #

An extremally disconnected topological space is a space in which the closure of every open set is open. Such spaces are also called Stonean spaces. They are the projective objects in the category of compact Hausdorff spaces.

## Main declarations #

`ExtremallyDisconnected`

: Predicate for a space to be extremally disconnected.`CompactT2.Projective`

: Predicate for a topological space to be a projective object in the category of compact Hausdorff spaces.`CompactT2.Projective.extremallyDisconnected`

: Compact Hausdorff spaces that are projective are extremally disconnected.`CompactT2.ExtremallyDisconnected.projective`

: Extremally disconnected spaces are projective objects in the category of compact Hausdorff spaces.

## References #

[Gleason, *Projective topological spaces*][gleason1958]

The closure of every open set is open.

An extremally disconnected topological space is a space in which the closure of every open set is open.

## Instances

Extremally disconnected spaces are totally separated.

The assertion `CompactT2.Projective`

states that given continuous maps
`f : X → Z`

and `g : Y → Z`

with `g`

surjective between `t_2`

, compact topological spaces,
there exists a continuous lift `h : X → Y`

, such that `f = g ∘ h`

.

## Instances For

Lemma 2.4 in [Gleason, *Projective topological spaces*][gleason1958]:
a continuous surjection $\pi$ from a compact space $D$ to a Fréchet space $A$ restricts to
a compact subset $E$ of $D$, such that $\pi$ maps $E$ onto $A$ and satisfies the
"Zorn subset condition", where $\pi(E_0) \ne A$ for any proper closed subset $E_0 \subsetneq E$.

Lemma 2.1 in [Gleason, *Projective topological spaces*][gleason1958]:
if $\rho$ is a continuous surjection from a topological space $E$ to a topological space $A$
satisfying the "Zorn subset condition", then $\rho(G)$ is contained in
the closure of $A \setminus \rho(E \setminus G)}$ for any open set $G$ of $E$.

Lemma 2.2 in [Gleason, *Projective topological spaces*][gleason1958]:
in an extremally disconnected space, if $U_1$ and $U_2$ are disjoint open sets,
then $\overline{U_1}$ and $\overline{U_2}$ are also disjoint.

Lemma 2.3 in [Gleason, *Projective topological spaces*][gleason1958]:
a continuous surjection from a compact Hausdorff space to an extremally disconnected Hausdorff space
satisfying the "Zorn subset condition" is a homeomorphism.

## Instances For

Theorem 2.5 in [Gleason, *Projective topological spaces*][gleason1958]:
in the category of compact spaces and continuous maps,
the projective spaces are precisely the extremally disconnected spaces.

The sigma-type of extremally disconnected spaces is extremally disconnected.