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

Definition of the points functor pt -

@[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

@[simp]

theorem Locale.openOfElementHom_toFun (L : Type u_1) [CompleteLattice L] (u : L) : (Locale.openOfElementHom L) u = {x : Locale.PT L | x u}

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

• Locale.openOfElementHom L = { toFun := fun (u : L) => {x : Locale.PT L | x u}, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ }

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

• Locale.PT.instTopologicalSpace L = { IsOpen := fun (s : Set (Locale.PT L)) => ∃ (u : L), {x : Locale.PT L | x u} = s, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

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.

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.

@[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)

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

• Locale.localePointOfSpacePoint X x = { toFun := fun (x_1 : TopologicalSpace.Opens X) => x ∈ x_1, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ }

def Locale.counitAppCont (L : Locale) : FrameHom (↑L.unop) (TopologicalSpace.Opens (Locale.PT ↑L.unop))

The counit is a frame homomorphism.

Equations

• L.counitAppCont = { toFun := fun (u : ↑L.unop) => { carrier := (Locale.openOfElementHom ↑L.unop) u, is_open' := ⋯ }, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ }

def Locale.adjunctionTopToLocalePT : topToLocale ⊣ Locale.pt

The forgetful functor topToLocale is left adjoint to the functor pt.

Equations

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