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]

class ExtremallyDisconnected (X : Type u) [TopologicalSpace X] : Prop

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

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

  The closure of every open set is open.

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

The closure of every open set is open.

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

instance instTotallySeparatedSpaceOfExtremallyDisconnectedOfT2Space (X : Type u) [TopologicalSpace X] [ExtremallyDisconnected X] [T2Space X] : TotallySeparatedSpace X

Extremally disconnected spaces are totally separated.

Equations

• ⋯ = ⋯

def CompactT2.Projective (X : Type u) [TopologicalSpace X] : Prop

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.

theorem StoneCech.projective {X : Type u} [TopologicalSpace X] [DiscreteTopology X] : CompactT2.Projective (StoneCech X)

theorem CompactT2.Projective.extremallyDisconnected {X : Type u} [TopologicalSpace X] [CompactSpace X] [T2Space X] (h : CompactT2.Projective X) : ExtremallyDisconnected X

theorem exists_compact_surjective_zorn_subset {A : Type u} {D : Type u} [TopologicalSpace A] [TopologicalSpace D] [T1Space A] [CompactSpace D] {π : D → A} (π_cont : Continuous π) (π_surj : Function.Surjective π) : ∃ (E : Set D), CompactSpace ↑E ∧ π '' E = Set.univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ Set.univ → IsClosed 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] {ρ : E → A} (ρ_cont : Continuous ρ) (ρ_surj : Function.Surjective ρ) (zorn_subset : ∀ (E₀ : Set E), E₀ ≠ Set.univ → IsClosed 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] {ρ : E → A} (ρ_cont : Continuous ρ) (ρ_surj : Function.Surjective ρ) (zorn_subset : ∀ (E₀ : Set E), E₀ ≠ Set.univ → IsClosed 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

• ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj zorn_subset = ρ_cont.homeoOfEquivCompactToT2

theorem CompactT2.ExtremallyDisconnected.projective {A : Type u} [TopologicalSpace A] [ExtremallyDisconnected A] [CompactSpace A] [T2Space A] : CompactT2.Projective A

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.

theorem CompactT2.projective_iff_extremallyDisconnected {A : Type u} [TopologicalSpace A] [CompactSpace A] [T2Space A] : CompactT2.Projective A ↔ ExtremallyDisconnected A

@[deprecated CompactT2.projective_iff_extremallyDisconnected]

theorem CompactT2.projective_iff_extremallyDisconnnected {A : Type u} [TopologicalSpace A] [CompactSpace A] [T2Space A] : CompactT2.Projective A ↔ ExtremallyDisconnected A

Alias of CompactT2.projective_iff_extremallyDisconnected.

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

• ⋯ = ⋯