feat(Topology/ExtremallyDisconnected): prove Gleason's theorem (#5634)

This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.

Co-authored-by: Filippo A E Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Dagur Ásgeirsson <dagurtomas@gmail.com>
Co-authored-by: Nikolas Kuhn <nikolaskuhn@gmx.de>

Mathlib/Data/Set/Basic.lean

@@ -607,6 +607,14 @@ theorem nonempty_iff_ne_empty : s.Nonempty ↔ s ≠ ∅ :=
   not_nonempty_iff_eq_empty.not_right
 #align set.nonempty_iff_ne_empty Set.nonempty_iff_ne_empty
 
+/-- See also `nonempty_iff_ne_empty'`. -/
+theorem not_nonempty_iff_eq_empty' : ¬Nonempty s ↔ s = ∅ := by
+  rw [nonempty_subtype, not_exists, eq_empty_iff_forall_not_mem]
+
+/-- See also `not_nonempty_iff_eq_empty'`. -/
+theorem nonempty_iff_ne_empty' : Nonempty s ↔ s ≠ ∅ :=
+  not_nonempty_iff_eq_empty'.not_right
+
 alias nonempty_iff_ne_empty ↔ Nonempty.ne_empty _
 #align set.nonempty.ne_empty Set.Nonempty.ne_empty
 

Mathlib/Data/Set/Functor.lean

@@ -72,4 +72,24 @@ instance : Alternative Set :=
     orElse := fun s t => s ∪ (t ())
     failure := ∅ }
 
+/-! ## Monadic coercion lemmas -/
+
+variable {β : Set α} {γ : Set β}
+
+theorem mem_coe_of_mem (ha : a ∈ β) (ha' : ⟨a, ha⟩ ∈ γ) : a ∈ (γ : Set α) :=
+  ⟨_, ⟨⟨_, rfl⟩, _, ⟨ha', rfl⟩, rfl⟩⟩
+
+theorem coe_subset : (γ : Set α) ⊆ β := by
+  intro _ ⟨_, ⟨⟨⟨_, ha⟩, rfl⟩, _, ⟨_, rfl⟩, _⟩⟩; convert ha
+
+theorem mem_of_mem_coe (ha : a ∈ (γ : Set α)) : ⟨a, coe_subset ha⟩ ∈ γ := by
+  rcases ha with ⟨_, ⟨_, rfl⟩, _, ⟨ha, rfl⟩, _⟩; convert ha
+
+theorem eq_univ_of_coe_eq (hγ : (γ : Set α) = β) : γ = univ :=
+  eq_univ_of_forall fun ⟨_, ha⟩ => mem_of_mem_coe <| hγ.symm ▸ ha
+
+theorem image_coe_eq_restrict_image {f : α → δ} : f '' γ = β.restrict f '' γ :=
+  ext fun _ =>
+    ⟨fun ⟨_, h, ha⟩ => ⟨_, mem_of_mem_coe h, ha⟩, fun ⟨_, h, ha⟩ => ⟨_, mem_coe_of_mem _ h, ha⟩⟩
+
 end Set

Mathlib/Topology/Constructions.lean

@@ -1623,3 +1623,21 @@ instance [TopologicalSpace α] [DiscreteTopology α] : DiscreteTopology (ULift 
   embedding_uLift_down.discreteTopology
 
 end ULift
+
+section Monad
+
+variable [TopologicalSpace α] {β : Set α} {γ : Set β}
+
+theorem IsOpen.trans (hγ : IsOpen γ) (hβ : IsOpen β) : IsOpen (γ : Set α) := by
+  rcases isOpen_induced_iff.mp hγ with ⟨δ, hδ, rfl⟩
+  convert IsOpen.inter hβ hδ
+  ext
+  exact ⟨fun h => ⟨coe_subset h, mem_of_mem_coe h⟩, fun ⟨hβ, hδ⟩ => mem_coe_of_mem hβ hδ⟩
+
+theorem IsClosed.trans (hγ : IsClosed γ) (hβ : IsClosed β) : IsClosed (γ : Set α) := by
+  rcases isClosed_induced_iff.mp hγ with ⟨δ, hδ, rfl⟩
+  convert IsClosed.inter hβ hδ
+  ext
+  exact ⟨fun h => ⟨coe_subset h, mem_of_mem_coe h⟩, fun ⟨hβ, hδ⟩ => mem_coe_of_mem hβ hδ⟩
+
+end Monad

Mathlib/Topology/ExtremallyDisconnected.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
+import Mathlib.Topology.Homeomorph
 import Mathlib.Topology.StoneCech
 
 #align_import topology.extremally_disconnected from "leanprover-community/mathlib"@"7e281deff072232a3c5b3e90034bd65dde396312"
@@ -19,34 +20,30 @@ compact Hausdorff spaces.
 * `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.
-
-# TODO
-
-Prove the converse to `CompactT2.Projective.extremallyDisconnected`, namely that a compact,
-Hausdorff, extremally disconnected space is 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]
 -/
 
+noncomputable section
 
-open Set
+open Classical Function Set
 
-open Classical
+universe u
 
-universe u v w
+section
 
 variable (X : Type u) [TopologicalSpace X]
 
-open Function
-
 /-- An extremally disconnected topological space is a space
 in which the closure of every open set is open. -/
 class ExtremallyDisconnected : Prop where
+  /-- The closure of every open set is open. -/
   open_closure : ∀ U : Set X, IsOpen U → IsOpen (closure U)
 #align extremally_disconnected ExtremallyDisconnected
 
@@ -85,8 +82,6 @@ def CompactT2.Projective : Prop :=
         ∃ h : X → Y, Continuous h ∧ g ∘ h = f
 #align compact_t2.projective CompactT2.Projective
 
-end
-
 variable {X}
 
 theorem StoneCech.projective [DiscreteTopology X] : CompactT2.Projective (StoneCech X) := by
@@ -116,16 +111,16 @@ protected theorem CompactT2.Projective.extremallyDisconnected [CompactSpace X] [
   have f_sur : Surjective f := by
     intro x
     by_cases hx : x ∈ U
-    · exact ⟨⟨(x, false), Or.inr ⟨subset_closure hx, Set.mem_singleton _⟩⟩, rfl⟩
-    · exact ⟨⟨(x, true), Or.inl ⟨hx, Set.mem_singleton _⟩⟩, rfl⟩
+    · exact ⟨⟨(x, false), Or.inr ⟨subset_closure hx, mem_singleton _⟩⟩, rfl⟩
+    · exact ⟨⟨(x, true), Or.inl ⟨hx, mem_singleton _⟩⟩, rfl⟩
   haveI : CompactSpace Z := isCompact_iff_compactSpace.mp hZ.isCompact
   obtain ⟨g, hg, g_sec⟩ := h continuous_id f_cont f_sur
   let φ := Subtype.val ∘ g
   have hφ : Continuous φ := continuous_subtype_val.comp hg
   have hφ₁ : ∀ x, (φ x).1 = x := congr_fun g_sec
   suffices closure U = φ ⁻¹' Z₂ by
-    rw [this, Set.preimage_comp, ← isClosed_compl_iff, ← preimage_compl, ←
-      preimage_subtype_coe_eq_compl Subset.rfl]
+    rw [this, preimage_comp, ← isClosed_compl_iff, ← preimage_compl,
+      ← preimage_subtype_coe_eq_compl Subset.rfl]
     · exact hZ₁.preimage hφ
     · rw [hZ₁₂.inter_eq, inter_empty]
   refine' (closure_minimal _ <| hZ₂.preimage hφ).antisymm fun x hx => _
@@ -139,11 +134,162 @@ protected theorem CompactT2.Projective.extremallyDisconnected [CompactSpace X] [
     exact hx.1
 #align compact_t2.projective.extremally_disconnected CompactT2.Projective.extremallyDisconnected
 
+end
+
+section
+
+variable {A D E : Type u} [TopologicalSpace A] [TopologicalSpace D] [TopologicalSpace E]
+
+/-- 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$. -/
+lemma exists_compact_surjective_zorn_subset [T1Space A] [CompactSpace D] {π : D → A}
+    (π_cont : Continuous π) (π_surj : π.Surjective) : ∃ E : Set D, CompactSpace E ∧ π '' E = univ ∧
+    ∀ E₀ : Set E, E₀ ≠ univ → IsClosed E₀ → E.restrict π '' E₀ ≠ univ := by
+  -- suffices to apply Zorn's lemma on the subsets of $D$ that are closed and mapped onto $A$
+  let S : Set <| Set D := {E : Set D | IsClosed E ∧ π '' E = univ}
+  suffices ∀ (C : Set <| Set D) (_ : C ⊆ S) (_ : IsChain (· ⊆ ·) C), ∃ s ∈ S, ∀ c ∈ C, s ⊆ c by
+    rcases zorn_superset S this with ⟨E, ⟨E_closed, E_surj⟩, E_min⟩
+    refine ⟨E, isCompact_iff_compactSpace.mp E_closed.isCompact, E_surj, ?_⟩
+    intro E₀ E₀_min E₀_closed
+    contrapose! E₀_min
+    exact eq_univ_of_coe_eq <|
+      E_min E₀ ⟨E₀_closed.trans E_closed, image_coe_eq_restrict_image ▸ E₀_min⟩ coe_subset
+  -- suffices to prove intersection of chain is minimal
+  intro C C_sub C_chain
+  -- prove intersection of chain is closed
+  refine ⟨iInter (fun c : C => c), ⟨isClosed_iInter fun ⟨_, h⟩ => (C_sub h).left, ?_⟩,
+    fun c hc _ h => mem_iInter.mp h ⟨c, hc⟩⟩
+  -- prove intersection of chain is mapped onto $A$
+  by_cases hC : Nonempty C
+  · refine eq_univ_of_forall fun a => inter_nonempty_iff_exists_left.mp ?_
+    -- apply Cantor's intersection theorem
+    refine iInter_inter (ι := C) (π ⁻¹' {a}) _ ▸
+      IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed _
+      ?_ (fun c => ?_) (fun c => IsClosed.isCompact ?_) (fun c => ?_)
+    · replace C_chain : IsChain (· ⊇ ·) C := C_chain.symm
+      have : ∀ s t : Set D, s ⊇ t → _ ⊇ _ := fun _ _ => inter_subset_inter_left <| π ⁻¹' {a}
+      exact (directedOn_iff_directed.mp C_chain.directedOn).mono_comp (· ⊇ ·) this
+    · rw [← image_inter_nonempty_iff, (C_sub c.mem).right, univ_inter]
+      exact singleton_nonempty a
+    all_goals exact (C_sub c.mem).left.inter <| (T1Space.t1 a).preimage π_cont
+  · rw [@iInter_of_empty _ _ <| not_nonempty_iff.mp hC, image_univ_of_surjective π_surj]
+
+/-- 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$. -/
+lemma image_subset_closure_compl_image_compl_of_isOpen {ρ : E → A} (ρ_cont : Continuous ρ)
+    (ρ_surj : ρ.Surjective) (zorn_subset : ∀ E₀ : Set E, E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ)
+    {G : Set E} (hG : IsOpen G) : ρ '' G ⊆ closure ((ρ '' Gᶜ)ᶜ) := by
+  -- suffices to prove for nonempty $G$
+  by_cases G_empty : G = ∅
+  · simpa only [G_empty, image_empty] using empty_subset _
+  · -- let $a \in \rho(G)$
+    intro a ha
+    rw [mem_closure_iff]
+    -- let $N$ be a neighbourhood of $a$
+    intro N N_open hN
+    -- get $x \in A$ from nonempty open $G \cap \rho^{-1}(N)$
+    rcases (G.mem_image ρ a).mp ha with ⟨e, he, rfl⟩
+    have nonempty : (G ∩ ρ⁻¹' N).Nonempty := ⟨e, mem_inter he <| mem_preimage.mpr hN⟩
+    have is_open : IsOpen <| G ∩ ρ⁻¹' N := hG.inter <| N_open.preimage ρ_cont
+    have ne_univ : ρ '' (G ∩ ρ⁻¹' N)ᶜ ≠ univ :=
+      zorn_subset _ (compl_ne_univ.mpr nonempty) is_open.isClosed_compl
+    rcases nonempty_compl.mpr ne_univ with ⟨x, hx⟩
+    -- prove $x \in N \cap (A \setminus \rho(E \setminus G))$
+    have hx' : x ∈ (ρ '' Gᶜ)ᶜ := fun h => hx <| image_subset ρ (by simp) h
+    rcases ρ_surj x with ⟨y, rfl⟩
+    have hy : y ∈ G ∩ ρ⁻¹' N := by simpa using mt (mem_image_of_mem ρ) <| mem_compl hx
+    exact ⟨ρ y, mem_inter (mem_preimage.mp <| mem_of_mem_inter_right hy) hx'⟩
+
+/-- 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. -/
+lemma ExtremallyDisconnected.disjoint_closure_of_disjoint_IsOpen [ExtremallyDisconnected A]
+    {U₁ U₂ : Set A} (h : Disjoint U₁ U₂) (hU₁ : IsOpen U₁) (hU₂ : IsOpen U₂) :
+    Disjoint (closure U₁) (closure U₂) :=
+  (h.closure_right hU₁).closure_left <| open_closure U₂ hU₂
+
+private lemma ExtremallyDisconnected.homeoCompactToT2_injective [ExtremallyDisconnected A]
+    [T2Space A] [T2Space E] [CompactSpace E] {ρ : E → A} (ρ_cont : Continuous ρ)
+    (ρ_surj : ρ.Surjective) (zorn_subset : ∀ E₀ : Set E, E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ) :
+    ρ.Injective := by
+  -- let $x_1, x_2 \in E$ be distinct points such that $\rho(x_1) = \rho(x_2)$
+  intro x₁ x₂ hρx
+  by_contra hx
+  -- let $G_1$ and $G_2$ be disjoint open neighbourhoods of $x_1$ and $x_2$ respectively
+  rcases t2_separation hx with ⟨G₁, G₂, G₁_open, G₂_open, hx₁, hx₂, disj⟩
+  -- prove $A \setminus \rho(E - G_1)$ and $A \setminus \rho(E - G_2)$ are disjoint
+  have G₁_comp : IsCompact G₁ᶜ := IsClosed.isCompact G₁_open.isClosed_compl
+  have G₂_comp : IsCompact G₂ᶜ := IsClosed.isCompact G₂_open.isClosed_compl
+  have G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ := (G₁_comp.image ρ_cont).isClosed.isOpen_compl
+  have G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ := (G₂_comp.image ρ_cont).isClosed.isOpen_compl
+  have disj' : Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ := by
+    rw [disjoint_iff_inter_eq_empty, ← compl_union, ← image_union, ← compl_inter,
+      disjoint_iff_inter_eq_empty.mp disj, compl_empty, compl_empty_iff,
+      image_univ_of_surjective ρ_surj]
+  -- apply Lemma 2.2 to prove their closures are disjoint
+  have disj'' : Disjoint (closure (ρ '' G₁ᶜ)ᶜ) (closure (ρ '' G₂ᶜ)ᶜ) :=
+    disjoint_closure_of_disjoint_IsOpen disj' G₁_open' G₂_open'
+  -- apply Lemma 2.1 to prove $\rho(x_1) = \rho(x_2)$ lies in their intersection
+  have hx₁' := image_subset_closure_compl_image_compl_of_isOpen ρ_cont ρ_surj zorn_subset G₁_open <|
+    mem_image_of_mem ρ hx₁
+  have hx₂' := image_subset_closure_compl_image_compl_of_isOpen ρ_cont ρ_surj zorn_subset G₂_open <|
+    mem_image_of_mem ρ hx₂
+  exact disj''.ne_of_mem hx₁' hx₂' hρx
+
+/-- 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. -/
+noncomputable def ExtremallyDisconnected.homeoCompactToT2 [ExtremallyDisconnected A] [T2Space A]
+    [T2Space E] [CompactSpace E] {ρ : E → A} (ρ_cont : Continuous ρ) (ρ_surj : ρ.Surjective)
+    (zorn_subset : ∀ E₀ : Set E, E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ) : E ≃ₜ A :=
+  ρ_cont.homeoOfEquivCompactToT2
+    (f := Equiv.ofBijective ρ ⟨homeoCompactToT2_injective ρ_cont ρ_surj zorn_subset, ρ_surj⟩)
+
+/-- 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.-/
+protected theorem CompactT2.ExtremallyDisconnected.projective [ExtremallyDisconnected A]
+    [CompactSpace A] [T2Space A] : CompactT2.Projective A := by
+  -- let $B$ and $C$ be compact; let $f : B \twoheadrightarrow C$ and $\phi : A \to C$ be continuous
+  intro B C _ _ _ _ _ _ φ f φ_cont f_cont f_surj
+  -- let $D := \{(a, b) : \phi(a) = f(b)\}$ with projections $\pi_1 : D \to A$ and $\pi_2 : D \to B$
+  let D : Set <| A × B := {x | φ x.fst = f x.snd}
+  have D_comp : CompactSpace D := isCompact_iff_compactSpace.mp
+    (isClosed_eq (φ_cont.comp continuous_fst) (f_cont.comp continuous_snd)).isCompact
+  -- apply Lemma 2.4 to get closed $E$ satisfying "Zorn subset condition"
+  let π₁ : D → A := Prod.fst ∘ Subtype.val
+  have π₁_cont : Continuous π₁ := continuous_fst.comp continuous_subtype_val
+  have π₁_surj : π₁.Surjective := fun a => ⟨⟨⟨a, _⟩, (f_surj <| φ a).choose_spec.symm⟩, rfl⟩
+  rcases exists_compact_surjective_zorn_subset π₁_cont π₁_surj with ⟨E, _, E_onto, E_min⟩
+  -- apply Lemma 2.3 to get homeomorphism $\pi_1|_E : E \to A$
+  let ρ : E → A := E.restrict π₁
+  have ρ_cont : Continuous ρ := π₁_cont.continuousOn.restrict
+  have ρ_surj : ρ.Surjective := fun a => by
+    rcases (E_onto ▸ mem_univ a : a ∈ π₁ '' E) with ⟨d, ⟨hd, rfl⟩⟩; exact ⟨⟨d, hd⟩, rfl⟩
+  let ρ' := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
+  -- prove $\rho := \pi_2|_E \circ \pi_1|_E^{-1}$ satisfies $\phi = f \circ \rho$
+  let π₂ : D → B := Prod.snd ∘ Subtype.val
+  have π₂_cont : Continuous π₂ := continuous_snd.comp continuous_subtype_val
+  refine ⟨E.restrict π₂ ∘ ρ'.symm, ⟨π₂_cont.continuousOn.restrict.comp ρ'.symm.continuous, ?_⟩⟩
+  suffices f ∘ E.restrict π₂ = φ ∘ ρ' by
+    rw [← comp.assoc, this, comp.assoc, Homeomorph.self_comp_symm, comp.right_id]
+  ext x
+  exact x.val.mem.symm
+
+protected theorem CompactT2.projective_iff_extremallyDisconnnected [CompactSpace A] [T2Space A] :
+    Projective A ↔ ExtremallyDisconnected A :=
+  ⟨Projective.extremallyDisconnected, fun _ => ExtremallyDisconnected.projective⟩
+
+end
+
 -- 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
+/-- The sigma-type of extremally disconnected 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 ⊢