feat: Adjunction between topological spaces and locales (#4593)

We define the contravariant functors between the categories of Frames and Topological Spaces and prove that they form an adjunction. 
Work started at the BIRS workshop "Formalization of Cohomology Theories", Banff, May 2023.

Co-authored-by: Anne Baanen <vierkantor@vierkantor.com>
Co-authored-by: leopoldmayer <leomayer@uw.edu>
Co-authored-by: Brendan Seamas Murphy <shamrockfrost@gmail.com>



Co-authored-by: leopoldmayer <leomayer@uw.edu>
Co-authored-by: Brendan Murphy <shamrockfrost@gmail.com>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Mathlib.lean

@@ -3488,6 +3488,7 @@ import Mathlib.Topology.OmegaCompletePartialOrder
 import Mathlib.Topology.Order
 import Mathlib.Topology.Order.Basic
 import Mathlib.Topology.Order.Category.AlexDisc
+import Mathlib.Topology.Order.Category.FrameAdjunction
 import Mathlib.Topology.Order.Hom.Basic
 import Mathlib.Topology.Order.Hom.Esakia
 import Mathlib.Topology.Order.Lattice

Mathlib/Data/Set/Basic.lean

@@ -568,6 +568,8 @@ theorem setOf_false : { _a : α | False } = ∅ :=
   rfl
 #align set.set_of_false Set.setOf_false
 
+@[simp] theorem setOf_bot : { _x : α | ⊥ } = ∅ := rfl
+
 @[simp]
 theorem empty_subset (s : Set α) : ∅ ⊆ s :=
   fun.
@@ -668,6 +670,8 @@ theorem setOf_true : { _x : α | True } = univ :=
   rfl
 #align set.set_of_true Set.setOf_true
 
+@[simp] theorem setOf_top : { _x : α | ⊤ } = univ := rfl
+
 @[simp, mfld_simps]
 theorem mem_univ (x : α) : x ∈ @univ α :=
   trivial

Mathlib/Topology/Order/Category/FrameAdjunction.lean

@@ -0,0 +1,119 @@
+/-
+Copyright (c) 2023 Anne Baanen, Sam v. Gool, Leo Mayer, Brendan S. Murphy. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen, Sam v. Gool, Leo Mayer, Brendan S. Murphy
+-/
+import Mathlib.Topology.Category.Locale
+
+/-!
+# Adjunction between Locales and Topological Spaces
+
+This file defines the point functor from the category of locales to topological spaces
+and proves that it is right adjoint to the forgetful functor from topological spaces to locales.
+
+## Main declarations
+
+* `Locale.pt`: the *points* functor from the category of locales to the category of topological
+spaces.
+
+* `Locale.adjunctionTopToLocalePT`: the adjunction between the functors `topToLocale` and `pt`.
+
+## Motivation
+
+This adjunction provides a framework in which several Stone-type dualities fit.
+
+## Implementation notes
+
+* In naming the various functions below, we follow common terminology and reserve the word *point*
+  for an inhabitant of a type `X` which is a topological space, while we use the word *element* for
+  an inhabitant of a type `L` which is a locale.
+
+## References
+
+* [J. Picado and A. Pultr, Frames and Locales: topology without points][picado2011frames]
+
+## Tags
+
+topological space, frame, locale, Stone duality, adjunction, points
+-/
+
+open CategoryTheory Order Set Topology TopologicalSpace
+
+namespace Locale
+
+/- ### Definition of the points functor `pt` --/
+
+section pt_definition
+
+variable (L : Type*) [CompleteLattice L]
+
+/-- The type of points of a complete lattice `L`, where a *point* of a complete lattice is,
+by definition, a frame homomorphism from `L` to `Prop`. -/
+@[reducible]
+def PT := FrameHom L Prop
+
+/-- The frame homomorphism from a complete lattice `L` to the complete lattice of sets of
+points of `L`. -/
+@[simps]
+def openOfElementHom : FrameHom L (Set (PT L)) where
+  toFun u := {x | x u}
+  map_inf' a b := by simp [Set.setOf_and]
+  map_top' := by simp
+  map_sSup' S := by ext; simp [Prop.exists_iff]
+
+namespace PT
+
+/-- The topology on the set of points of the complete lattice `L`. -/
+instance instTopologicalSpace : TopologicalSpace (PT L) where
+  IsOpen s := ∃ u, {x | x u} = s
+  isOpen_univ := ⟨⊤, by simp⟩
+  isOpen_inter := by rintro s t ⟨u, rfl⟩ ⟨v, rfl⟩; use u ⊓ v; simp_rw [map_inf]; rfl
+  isOpen_sUnion S hS := by
+    choose f hf using hS
+    use ⨆ t, ⨆ ht, f t ht
+    simp_rw [map_iSup, iSup_Prop_eq, setOf_exists, hf, sUnion_eq_biUnion]
+
+/-- Characterization of when a subset of the space of points is open. -/
+lemma isOpen_iff (U : Set (PT L)) : IsOpen U ↔ ∃ u : L, {x | x u} = U := Iff.rfl
+
+end PT
+
+/-- The covariant functor `pt` from the category of locales to the category of
+topological spaces, which sends a locale `L` to the topological space `PT L` of homomorphisms
+from `L` to `Prop` and a locale homomorphism `f` to a continuous function between the spaces
+of points. -/
+def pt : Locale ⥤ TopCat where
+  obj L := ⟨PT L.unop, inferInstance⟩
+  map f := ⟨fun p ↦ p.comp f.unop, continuous_def.2 <| by rintro s ⟨u, rfl⟩; use f.unop u; rfl⟩
+end pt_definition
+
+section locale_top_adjunction
+
+variable (X : Type*) [TopologicalSpace X] (L : Locale)
+
+/-- The unit of the adjunction between locales and topological spaces, which associates with
+a point `x` of the space `X` a point of the locale of opens of `X`. -/
+@[simps]
+def localePointOfSpacePoint (x : X) : PT (Opens X) where
+  toFun := (x ∈ ·)
+  map_inf' a b := rfl
+  map_top' := rfl
+  map_sSup' S := by simp [Prop.exists_iff]
+
+/-- The counit is a frame homomorphism. -/
+def counitAppCont : FrameHom L (Opens <| PT L) where
+  toFun u := ⟨openOfElementHom L u, u, rfl⟩
+  map_inf' a b := by simp
+  map_top' := by simp
+  map_sSup' S := by ext; simp
+
+/-- The forgetful functor `topToLocale` is left adjoint to the functor `pt`. -/
+def adjunctionTopToLocalePT : topToLocale ⊣ pt :=
+  Adjunction.mkOfUnitCounit
+    { unit := { app := fun X ↦ ⟨localePointOfSpacePoint X, continuous_def.2 <|
+        by rintro _ ⟨u, rfl⟩; simpa using u.2⟩ }
+      counit := { app := fun L ↦ ⟨counitAppCont L⟩ } }
+
+end locale_top_adjunction
+
+end Locale

Mathlib/Topology/Sets/Opens.lean

@@ -184,6 +184,8 @@ theorem coe_bot : ((⊥ : Opens α) : Set α) = ∅ :=
   rfl
 #align topological_space.opens.coe_bot TopologicalSpace.Opens.coe_bot
 
+@[simp] theorem mk_empty : (⟨∅, isOpen_empty⟩ : Opens α) = ⊥ := rfl
+
 -- porting note: new lemma
 @[simp, norm_cast]
 theorem coe_eq_empty {U : Opens α} : (U : Set α) = ∅ ↔ U = ⊥ :=
@@ -194,6 +196,8 @@ theorem coe_top : ((⊤ : Opens α) : Set α) = Set.univ :=
   rfl
 #align topological_space.opens.coe_top TopologicalSpace.Opens.coe_top
 
+@[simp] theorem mk_univ : (⟨univ, isOpen_univ⟩ : Opens α) = ⊤ := rfl
+
 -- porting note: new lemma
 @[simp, norm_cast]
 theorem coe_eq_univ {U : Opens α} : (U : Set α) = univ ↔ U = ⊤ :=

docs/references.bib

@@ -2136,6 +2136,15 @@ @Article{         phillips1940
   url           = {https://doi.org/10.2307/1990004}
 }
 
+@Book{            picado2011frames,
+  title         = {Frames and Locales: topology without points},
+  author        = {Picado, Jorge and Pultr, Ale{\v{s}}},
+  year          = {2011},
+  publisher     = {Birkhäuser Basel},
+  doi           = {10.1007/978-3-0348-0154-6},
+  isbn          = {9783034801539}
+}
+
 @Misc{            ponton2020chebyshev,
   title         = {Roots of {C}hebyshev polynomials: a purely algebraic
                   approach},