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

source

@[reducible]

def Locale.PT (L : Type u_1) [CompleteLattice L] :

Type u_1

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.

Equations

Locale.PT L = FrameHom L Prop

Instances For

source

@[simp]

theorem Locale.openOfElementHom_toFun (L : Type u_1) [CompleteLattice L] (u : L) :

(Locale.openOfElementHom L) u = {x : Locale.PT L | x u}

source

def Locale.openOfElementHom (L : Type u_1) [CompleteLattice L] :

FrameHom L (Set (Locale.PT L))

The frame homomorphism from a complete lattice L to the complete lattice of sets of points of L.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance Locale.PT.instTopologicalSpace (L : Type u_1) [CompleteLattice L] :

TopologicalSpace (Locale.PT L)

The topology on the set of points of the complete lattice L.

Equations

One or more equations did not get rendered due to their size.

source

theorem Locale.PT.isOpen_iff (L : Type u_1) [CompleteLattice L] (U : Set (Locale.PT L)) :

IsOpen U ↔ ∃ (u : L), {x : Locale.PT L | x u} = U

Characterization of when a subset of the space of points is open.

source

def Locale.pt :

CategoryTheory.Functor Locale TopCat

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Locale.localePointOfSpacePoint_toFun (X : Type u_1) [TopologicalSpace X] (x : X) :

∀ (x_1 : TopologicalSpace.Opens X), (Locale.localePointOfSpacePoint X x) x_1 = (x ∈ x_1)

source

def Locale.localePointOfSpacePoint (X : Type u_1) [TopologicalSpace X] (x : X) :

Locale.PT (TopologicalSpace.Opens X)

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.

Equations