From 21c7184c628e8df2ffcc91b0591a273018f5cf92 Mon Sep 17 00:00:00 2001 From: samvang <59202064+samvang@users.noreply.github.com> Date: Sat, 21 Oct 2023 09:35:32 +0000 Subject: [PATCH] feat: Adjunction between topological spaces and locales (#4593) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Co-authored-by: leopoldmayer Co-authored-by: Brendan Seamas Murphy Co-authored-by: leopoldmayer Co-authored-by: Brendan Murphy Co-authored-by: Vierkantor Co-authored-by: Yaël Dillies --- Mathlib.lean | 1 + Mathlib/Data/Set/Basic.lean | 4 + .../Order/Category/FrameAdjunction.lean | 119 ++++++++++++++++++ Mathlib/Topology/Sets/Opens.lean | 4 + docs/references.bib | 9 ++ 5 files changed, 137 insertions(+) create mode 100644 Mathlib/Topology/Order/Category/FrameAdjunction.lean diff --git a/Mathlib.lean b/Mathlib.lean index 53a03aaeb6e74..c8b13aa68d1b6 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index af5c7c628126b..f71299285dccf 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/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 diff --git a/Mathlib/Topology/Order/Category/FrameAdjunction.lean b/Mathlib/Topology/Order/Category/FrameAdjunction.lean new file mode 100644 index 0000000000000..f11516d02c6da --- /dev/null +++ b/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 diff --git a/Mathlib/Topology/Sets/Opens.lean b/Mathlib/Topology/Sets/Opens.lean index 45c6cd630b991..627225d9f7c42 100644 --- a/Mathlib/Topology/Sets/Opens.lean +++ b/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 = ⊤ := diff --git a/docs/references.bib b/docs/references.bib index 9f15f1311d5b8..47d9b00fdfc4f 100644 --- a/docs/references.bib +++ b/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},