# 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.

## 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

@[reducible]
def Locale.PT (L : Type u_1) [] :
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
Instances For
@[simp]
theorem Locale.openOfElementHom_toFun (L : Type u_1) [] (u : L) :
= {x : | x u}
def Locale.openOfElementHom (L : Type u_1) [] :
FrameHom L (Set ())

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
instance Locale.PT.instTopologicalSpace (L : Type u_1) [] :

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.
theorem Locale.PT.isOpen_iff (L : Type u_1) [] (U : Set ()) :
∃ (u : L), {x : | x u} = U

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

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
@[simp]
theorem Locale.localePointOfSpacePoint_toFun (X : Type u_1) [] (x : X) :
∀ (x_1 : ), x_1 = (x x_1)
def Locale.localePointOfSpacePoint (X : Type u_1) [] (x : 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
• One or more equations did not get rendered due to their size.
Instances For

The counit is a frame homomorphism.

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

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

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