Documentation

Mathlib.Topology.ExtremallyDisconnected

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 #

References #

[Gleason, Projective topological spaces][gleason1958]

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

Instances

    The closure of every open set is open.

    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 exists_compact_surjective_zorn_subset {A : Type u} {D : Type u} [TopologicalSpace A] [TopologicalSpace D] [T1Space A] [CompactSpace D] {π : DA} (π_cont : Continuous π) (π_surj : Function.Surjective π) :
      ∃ (E : Set D), CompactSpace E π '' E = Set.univ ∀ (E₀ : Set E), E₀ Set.univIsClosed E₀E.restrict π '' E₀ Set.univ

      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$.

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

      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$.

      theorem ExtremallyDisconnected.disjoint_closure_of_disjoint_isOpen {A : Type u} [TopologicalSpace A] [ExtremallyDisconnected A] {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][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.

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

      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.

      Equations
      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.

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

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

        Equations
        • =