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 #

extremally_disconnected: Predicate for a space to be extremally disconnected.
compact_t2.projective: ¨Predicate for a topological space to be a projective object in the category of compact Hausdorff spaces.
compact_t2.projective.extremally_disconnected: Compact Hausdorff spaces that are projective are extremally disconnected.

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

source

@[class]

structure extremally_disconnected (X : Type u) [topological_space X] :

Prop

open_closure : ∀ (U : set X), is_open U → is_open (closure U)

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

source

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

compact_t2.projective X = ∀ {Y Z : Type u} [_inst_2 : topological_space Y] [_inst_3 : topological_space Z] [_inst_4 : compact_space Y] [_inst_5 : t2_space Y] [_inst_6 : compact_space Z] [_inst_7 : t2_space Z] {f : X → Z} {g : Y → Z}, continuous f → continuous g → function.surjective g → (∃ (h : X → Y), continuous h ∧ g ∘ h = f)

source

theorem stone_cech.projective {X : Type u} [topological_space X] [discrete_topology X] :

compact_t2.projective (stone_cech X)

source

@[protected]

theorem compact_t2.projective.extremally_disconnected {X : Type u} [topological_space X] [compact_space X] [t2_space X] (h : compact_t2.projective X) :

extremally_disconnected X