mathlib3 documentation

topology.extremally_disconnected

Extremally disconnected spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

TODO #

Prove the converse to compact_t2.projective.extremally_disconnected, namely that a compact, Hausdorff, extremally disconnected space is a projective object in the category of compact Hausdorff spaces.

References #

Gleason, Projective topological spaces

@[class]
structure extremally_disconnected (X : Type u) [topological_space X] :
Prop

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

def compact_t2.projective (X : Type u) [topological_space X] :
Prop

The assertion compact_t2.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.

Equations