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

class ExtremallyDisconnected (X : Type u) [] :

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

• open_closure : ∀ (U : Set X), IsOpen ()

The closure of every open set is open.

Instances
theorem ExtremallyDisconnected.open_closure {X : Type u} [] [self : ] (U : Set X) :
IsOpen ()

The closure of every open set is open.

theorem extremallyDisconnected_of_homeo {X : Type u_1} {Y : Type u_2} [] [] (e : X ≃ₜ Y) :

Extremally disconnected spaces are totally separated.

Equations
• =

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem StoneCech.projective {X : Type u} [] [] :
theorem exists_compact_surjective_zorn_subset {A : Type u} {D : Type u} [] [] [] [] {π : DA} (π_cont : ) (π_surj : ) :
∃ (E : Set D), π '' E = Set.univ ∀ (E₀ : Set E), E₀ Set.univIsClosed E₀E.restrict π '' E₀ Set.univ

Lemma 2.4 in Gleason, Projective topological spaces: 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$.

theorem image_subset_closure_compl_image_compl_of_isOpen {A : Type u} {E : Type u} [] [] {ρ : EA} (ρ_cont : ) (ρ_surj : ) (zorn_subset : ∀ (E₀ : Set E), E₀ Set.univIsClosed E₀ρ '' E₀ Set.univ) {G : Set E} (hG : ) :
ρ '' G closure (ρ '' G)

Lemma 2.1 in Gleason, Projective topological spaces: 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$.

theorem ExtremallyDisconnected.disjoint_closure_of_disjoint_isOpen {A : Type u} [] {U₁ : Set A} {U₂ : Set A} (h : Disjoint U₁ U₂) (hU₁ : IsOpen U₁) (hU₂ : IsOpen U₂) :
Disjoint (closure U₁) (closure U₂)

Lemma 2.2 in Gleason, Projective topological spaces: 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.

noncomputable def ExtremallyDisconnected.homeoCompactToT2 {A : Type u} {E : Type u} [] [] [] [] [] {ρ : EA} (ρ_cont : ) (ρ_surj : ) (zorn_subset : ∀ (E₀ : Set E), E₀ Set.univIsClosed E₀ρ '' E₀ Set.univ) :
E ≃ₜ A

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

Equations
Instances For

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

@[deprecated CompactT2.projective_iff_extremallyDisconnected]

Alias of CompactT2.projective_iff_extremallyDisconnected.

instance instExtremallyDisconnected {ι : Type u_1} {π : ιType u_2} [(i : ι) → TopologicalSpace (π i)] [h₀ : ∀ (i : ι), ] :
ExtremallyDisconnected ((i : ι) × π i)

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

Equations
• =