Stonean.extrDisc
theorem Stonean.extrDisc : ∀ (self : Stonean), ExtremallyDisconnected ↑self.compHaus.toTop
This theorem states that a Stonean space is extremally disconnected. In other words, for any Stonean space, the underlying topological space (obtained from the compact Hausdorff space associated with the Stonean space) is extremally disconnected. Note that a topological space is said to be extremally disconnected if the closure of every open set in the space is open.
More concisely: Every Stonean space is an extremally disconnected topological space.
|
Stonean.epi_iff_surjective
theorem Stonean.epi_iff_surjective : ∀ {X Y : Stonean} (f : X ⟶ Y), CategoryTheory.Epi f ↔ Function.Surjective ⇑f := by
sorry
This theorem states that for any two objects `X` and `Y` in the `Stonean` category, a morphism `f` from `X` to `Y` is an epimorphism if and only if it is a surjective function. An epimorphism `f` is one that satisfies the property that for any two morphisms `g` and `h` from `Y` to any other object `Z`, if `g ∘ f = h ∘ f`, then `g = h`. On the other hand, a surjective function `f` is one where for every element `b` in the codomain `Y`, there exists an element `a` in the domain `X` such that `f(a) = b`. A future direction of this work is to prove that the functor `forget Stonean` preserves pushouts and then use this result to derive this theorem using general results about concrete categories.
More concisely: In the Stonean category, a morphism is an epimorphism if and only if it is a surjective function.
|