feat: define the category of extremally disconnected compact Hausdorff spaces (#5761)

Co-authored-by: Adam Topaz [topaz@ualberta.ca](mailto:topaz@ualberta.ca) @adamtopaz 
Basics of the category `Stonean` of extremally disconnected compact Hausdorff spaces. This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.

Author: dagurtomas

Mathlib.lean

@@ -3159,6 +3159,8 @@ import Mathlib.Topology.Category.Profinite.AsLimit
 import Mathlib.Topology.Category.Profinite.Basic
 import Mathlib.Topology.Category.Profinite.CofilteredLimit
 import Mathlib.Topology.Category.Profinite.Projective
+import Mathlib.Topology.Category.Stonean.Basic
+import Mathlib.Topology.Category.Stonean.Limits
 import Mathlib.Topology.Category.TopCat.Adjunctions
 import Mathlib.Topology.Category.TopCat.Basic
 import Mathlib.Topology.Category.TopCat.EpiMono

Mathlib/Data/Set/Image.lean

@@ -1637,3 +1637,17 @@ theorem preimage_eq_empty_iff {s : Set β} : f ⁻¹' s = ∅ ↔ Disjoint s (ra
 end Set
 
 end Disjoint
+
+section Sigma
+
+variable {α : Type _} {β : α → Type _} {i j : α} {s : Set (β i)}
+
+lemma sigma_mk_preimage_image' (h : i ≠ j) : Sigma.mk j ⁻¹' (Sigma.mk i '' s) = ∅ := by
+  change Sigma.mk j ⁻¹' {⟨i, u⟩ | u ∈ s} = ∅
+  simp [h]
+
+lemma sigma_mk_preimage_image_eq_self : Sigma.mk i ⁻¹' (Sigma.mk i '' s) = s := by
+  change Sigma.mk i ⁻¹' {⟨i, u⟩ | u ∈ s} = s
+  simp
+
+end Sigma

Mathlib/Topology/Category/Stonean/Basic.lean

@@ -0,0 +1,146 @@
+/-
+Copyright (c) 2023 Adam Topaz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam Topaz
+-/
+import Mathlib.Topology.ExtremallyDisconnected
+import Mathlib.CategoryTheory.Sites.Coherent
+import Mathlib.Topology.Category.CompHaus.Projective
+import Mathlib.Topology.Category.Profinite.Basic
+/-!
+# Extremally disconnected sets
+
+This file develops some of the basic theory of extremally disconnected sets.
+
+## Overview
+
+This file defines the type `Stonean` of all extremally (note: not "extremely"!)
+disconnected compact Hausdorff spaces, gives it the structure of a large category,
+and proves some basic observations about this category and various functors from it.
+
+The Lean implementation: a term of type `Stonean` is a pair, considering of
+a term of type `CompHaus` (i.e. a compact Hausdorff topological space) plus
+a proof that the space is extremally disconnected.
+This is equivalent to the assertion that the term is projective in `CompHaus`,
+in the sense of category theory (i.e., such that morphisms out of the object
+can be lifted along epimorphisms).
+
+## Main definitions
+
+* `Stonean` : the category of extremally disconnected compact Hausdorff spaces.
+* `Stonean.toCompHaus` : the forgetful functor `Stonean ⥤ CompHaus` from Stonean
+  spaces to compact Hausdorff spaces
+* `Stonean.toProfinite` : the functor from Stonean spaces to profinite spaces.
+
+-/
+universe u
+
+open CategoryTheory
+
+/-- `Stonean` is the category of extremally disconnected compact Hausdorff spaces. -/
+structure Stonean where
+  /-- The underlying compact Hausdorff space of a Stonean space. -/
+  compHaus : CompHaus.{u}
+  /-- A Stonean space is extremally disconnected -/
+  [extrDisc : ExtremallyDisconnected compHaus]
+
+namespace CompHaus
+
+/-- `Projective` implies `ExtremallyDisconnected`. -/
+instance (X : CompHaus.{u}) [Projective X] : ExtremallyDisconnected X := by
+  apply CompactT2.Projective.extremallyDisconnected
+  intro A B _ _ _ _ _ _ f g hf hg hsurj
+  have : CompactSpace (TopCat.of A) := by assumption
+  have : T2Space (TopCat.of A) := by assumption
+  have : CompactSpace (TopCat.of B) := by assumption
+  have : T2Space (TopCat.of B) := by assumption
+  let A' : CompHaus := ⟨TopCat.of A⟩
+  let B' : CompHaus := ⟨TopCat.of B⟩
+  let f' : X ⟶ B' := ⟨f, hf⟩
+  let g' : A' ⟶ B' := ⟨g,hg⟩
+  have : Epi g' := by
+    rw [CompHaus.epi_iff_surjective]
+    assumption
+  obtain ⟨h,hh⟩ := Projective.factors f' g'
+  refine ⟨h,h.2,?_⟩
+  ext t
+  apply_fun (fun e => e t) at hh
+  exact hh
+
+/-- `Projective` implies `Stonean`. -/
+@[simps!]
+def toStonean (X : CompHaus.{u}) [Projective X] :
+    Stonean where
+  compHaus := X
+
+end CompHaus
+
+namespace Stonean
+
+/-- Stonean spaces form a large category. -/
+instance : LargeCategory Stonean.{u} :=
+  show Category (InducedCategory CompHaus (·.compHaus)) from inferInstance
+
+/-- The (forgetful) functor from Stonean spaces to compact Hausdorff spaces. -/
+@[simps!]
+def toCompHaus : Stonean.{u} ⥤ CompHaus.{u} :=
+  inducedFunctor _
+
+/-- Construct a term of `Stonean` from a type endowed with the structure of a
+compact, Hausdorff and extremally disconnected topological space.
+-/
+def of (X : Type _) [TopologicalSpace X] [CompactSpace X] [T2Space X]
+    [ExtremallyDisconnected X] : Stonean :=
+  ⟨⟨⟨X, inferInstance⟩⟩⟩
+
+/-- The forgetful functor `Stonean ⥤ CompHaus` is full. -/
+instance : Full toCompHaus where
+  preimage := fun f => f
+
+
+/-- The forgetful functor `Stonean ⥤ CompHaus` is faithful. -/
+instance : Faithful toCompHaus := {}
+
+/-- Stonean spaces are a concrete category. -/
+instance : ConcreteCategory Stonean where
+  forget := toCompHaus ⋙ forget _
+
+instance : CoeSort Stonean.{u} (Type u) := ConcreteCategory.hasCoeToSort _
+instance {X Y : Stonean.{u}} : FunLike (X ⟶ Y) X (fun _ => Y) := ConcreteCategory.funLike
+
+/-- Stonean spaces are topological spaces. -/
+instance instTopologicalSpace (X : Stonean.{u}) : TopologicalSpace X :=
+  show TopologicalSpace X.compHaus from inferInstance
+
+/-- Stonean spaces are compact. -/
+instance (X : Stonean.{u}) : CompactSpace X :=
+  show CompactSpace X.compHaus from inferInstance
+
+/-- Stonean spaces are Hausdorff. -/
+instance (X : Stonean.{u}) : T2Space X :=
+  show T2Space X.compHaus from inferInstance
+
+instance (X : Stonean.{u}) : ExtremallyDisconnected X :=
+  X.2
+
+/-- The functor from Stonean spaces to profinite spaces. -/
+@[simps]
+def toProfinite : Stonean.{u} ⥤ Profinite.{u} where
+  obj X :=
+  { toCompHaus := X.compHaus,
+    IsTotallyDisconnected := show TotallyDisconnectedSpace X from inferInstance }
+  map f := f
+
+/-- The functor from Stonean spaces to profinite spaces is full. -/
+instance : Full toProfinite where
+  preimage f := f
+
+/-- The functor from Stonean spaces to profinite spaces is faithful. -/
+instance : Faithful toProfinite := {}
+
+/-- The functor from Stonean spaces to compact Hausdorff spaces
+    factors through profinite spaces. -/
+example : toProfinite ⋙ profiniteToCompHaus = toCompHaus :=
+  rfl
+
+end Stonean

Mathlib/Topology/Category/Stonean/Limits.lean

@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2023 Adam Topaz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam Topaz
+-/
+import Mathlib.Topology.Category.Stonean.Basic
+/-!
+# Explicit (co)limits in Extremally disconnected sets
+
+This file describes some explicit (co)limits in `Stonean`
+
+## Overview
+
+We define explicit finite coproducts in `Stonean` as sigma types (disjoint unions).
+
+TODO: Define pullbacks of open embeddings.
+
+-/
+
+open CategoryTheory
+
+namespace Stonean
+
+/-!
+This section defines the finite Coproduct of a finite family
+of profinite spaces `X : α → Stonean.{u}`
+
+Notes: The content is mainly copied from
+`Mathlib/Topology/Category/CompHaus/ExplicitLimits.lean`
+-/
+section FiniteCoproducts
+
+open Limits
+
+variable {α : Type} [Fintype α] {B : Stonean.{u}}
+  (X : α → Stonean.{u})
+
+/--
+The coproduct of a finite family of objects in `Stonean`, constructed as the disjoint
+union with its usual topology.
+-/
+def finiteCoproduct : Stonean := Stonean.of <| Σ (a : α), X a
+
+/-- The inclusion of one of the factors into the explicit finite coproduct. -/
+def finiteCoproduct.ι (a : α) : X a ⟶ finiteCoproduct X where
+  toFun := fun x => ⟨a,x⟩
+  continuous_toFun := continuous_sigmaMk (σ := fun a => X a)
+
+/--
+To construct a morphism from the explicit finite coproduct, it suffices to
+specify a morphism from each of its factors.
+This is essentially the universal property of the coproduct.
+-/
+def finiteCoproduct.desc {B : Stonean.{u}} (e : (a : α) → (X a ⟶ B)) :
+    finiteCoproduct X ⟶ B where
+  toFun := fun ⟨a,x⟩ => e a x
+  continuous_toFun := by
+    apply continuous_sigma
+    intro a; exact (e a).continuous
+
+@[reassoc (attr := simp)]
+lemma finiteCoproduct.ι_desc {B : Stonean.{u}} (e : (a : α) → (X a ⟶ B)) (a : α) :
+  finiteCoproduct.ι X a ≫ finiteCoproduct.desc X e = e a := rfl
+
+lemma finiteCoproduct.hom_ext {B : Stonean.{u}} (f g : finiteCoproduct X ⟶ B)
+    (h : ∀ a : α, finiteCoproduct.ι X a ≫ f = finiteCoproduct.ι X a ≫ g) : f = g := by
+  ext ⟨a,x⟩
+  specialize h a
+  apply_fun (fun q => q x) at h
+  exact h
+
+/-- The coproduct cocone associated to the explicit finite coproduct. -/
+@[simps]
+def finiteCoproduct.cocone (F : Discrete α ⥤ Stonean) :
+    Cocone F where
+  pt := finiteCoproduct F.obj
+  ι := Discrete.natTrans fun a => finiteCoproduct.ι F.obj a
+
+/-- The explicit finite coproduct cocone is a colimit cocone. -/
+@[simps]
+def finiteCoproduct.isColimit (F : Discrete α ⥤ Stonean) :
+    IsColimit (finiteCoproduct.cocone F) where
+  desc := fun s => finiteCoproduct.desc _ fun a => s.ι.app a
+  fac := fun s ⟨a⟩ => finiteCoproduct.ι_desc _ _ _
+  uniq := fun s m hm => finiteCoproduct.hom_ext _ _ _ fun a => by
+    specialize hm a
+    ext t
+    apply_fun (fun q => q t) at hm
+    exact hm
+
+/-- The category of extremally disconnected spaces has finite coproducts.
+-/
+instance hasFiniteCoproducts : HasFiniteCoproducts Stonean.{u} where
+  out _ := {
+    has_colimit := fun F => {
+      exists_colimit := ⟨{
+        cocone := finiteCoproduct.cocone F
+        isColimit := finiteCoproduct.isColimit F }⟩ } }
+
+end FiniteCoproducts
+
+end Stonean

Mathlib/Topology/ExtremallyDisconnected.lean

@@ -34,8 +34,6 @@ spaces.
 -/
 
 
-noncomputable section
-
 open Set
 
 open Classical
@@ -52,6 +50,29 @@ class ExtremallyDisconnected : Prop where
   open_closure : ∀ U : Set X, IsOpen U → IsOpen (closure U)
 #align extremally_disconnected ExtremallyDisconnected
 
+section TotallySeparated
+
+/-- Extremally disconnected spaces are totally separated. -/
+instance [ExtremallyDisconnected X] [T2Space X] : TotallySeparatedSpace X :=
+{ isTotallySeparated_univ := by
+    intro x _ y _ hxy
+    obtain ⟨U, V, hUV⟩ := T2Space.t2 x y hxy
+    use closure U
+    use (closure U)ᶜ
+    refine ⟨ExtremallyDisconnected.open_closure U hUV.1,
+      by simp only [isOpen_compl_iff, isClosed_closure], subset_closure hUV.2.2.1, ?_,
+      by simp only [Set.union_compl_self, Set.subset_univ], disjoint_compl_right⟩
+    simp only [Set.mem_compl_iff]
+    rw [mem_closure_iff]
+    push_neg
+    refine' ⟨V, ⟨hUV.2.1, hUV.2.2.2.1, _⟩⟩
+    rw [Set.nonempty_iff_ne_empty]
+    simp only [not_not]
+    rw [← Set.disjoint_iff_inter_eq_empty, disjoint_comm]
+    exact hUV.2.2.2.2 }
+
+end TotallySeparated
+
 section
 
 /-- The assertion `CompactT2.Projective` states that given continuous maps
@@ -117,3 +138,30 @@ protected theorem CompactT2.Projective.extremallyDisconnected [CompactSpace X] [
   · rw [← hφ₁ x]
     exact hx.1
 #align compact_t2.projective.extremally_disconnected CompactT2.Projective.extremallyDisconnected
+
+-- Note: It might be possible to use Gleason for this instead
+/-- The sigma-type of extremally disconneted spaces is extremally disconnected -/
+instance instExtremallyDisconnected
+    {π : ι → Type _} [∀ i, TopologicalSpace (π i)] [h₀ : ∀ i, ExtremallyDisconnected (π i)] :
+    ExtremallyDisconnected (Σi, π i) := by
+  constructor
+  intro s hs
+  rw [isOpen_sigma_iff] at hs ⊢
+  intro i
+  rcases h₀ i with ⟨h₀⟩
+  have h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
+  · apply h₀
+    exact hs i
+  suffices h₂ : Sigma.mk i ⁻¹' closure s = closure (Sigma.mk i ⁻¹' s)
+  · rwa [h₂]
+  apply IsOpenMap.preimage_closure_eq_closure_preimage
+  intro U _
+  · rw [isOpen_sigma_iff]
+    intro j
+    by_cases ij : i = j
+    · rw [← ij]
+      rw [sigma_mk_preimage_image_eq_self]
+      assumption
+    · rw [sigma_mk_preimage_image' ij]
+      apply isOpen_empty
+  · continuity