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 functorstopToLocale
andpt
.
Motivation #
This adjunction provides a framework in which several Stonetype 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 typeL
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
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
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.
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
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.