The
objects of the category
CHey, the category
Frm of frames and the category
Loc of locales are complete Heyting algebras. These categories differ in what constitutes a
morphism: • The morphisms of
Frm are (necessarily
monotone) functions that preserve finite meets and arbitrary joins. • The definition of Heyting algebras crucially involves the existence of right adjoints to the binary meet operation, which together define an additional
implication operation. Thus, the morphisms of
CHey are morphisms of frames that in addition preserve implication. • The morphisms of
Loc are
opposite to those of
Frm, and they are usually called maps (of locales). The relation of locales and their maps to topological spaces and continuous functions may be seen as follows. Let f: X\to Y be any map. The
power sets
P(
X) and
P(
Y) are
complete Boolean algebras, and the map f^{-1}: P(Y)\to P(X) is a homomorphism of complete Boolean algebras. Suppose the spaces
X and
Y are
topological spaces, endowed with the topology
O(
X) and
O(
Y) of
open sets on
X and
Y. Note that
O(
X) and
O(
Y) are subframes of
P(
X) and
P(
Y). If f is a continuous function, then f^{-1}: O(Y)\to O(X) preserves finite meets and arbitrary joins of these subframes. This shows that
O is a
functor from the category
Top of topological spaces to
Loc, taking any continuous map : f: X\to Y to the map : O(f): O(X)\to O(Y) in
Loc that is defined in
Frm to be the inverse image frame homomorphism : f^{-1}: O(Y)\to O(X). Given a map of locales f: A\to B in
Loc, it is common to write f^*: B\to A for the frame homomorphism that defines it in
Frm. Using this notation, O(f) is defined by the equation O(f)^* = f^{-1}. Conversely, any locale
A has a topological space
S(
A), called its
spectrum, that best approximates the locale. In addition, any map of locales f: A\to B determines a continuous map S(A)\to S(B). Moreover, this assignment is functorial: letting
P(1) denote the locale that is obtained as the power set of the terminal set 1=\{*\}, the points of
S(
A) are the maps p: P(1)\to A in
Loc, i.e., the frame homomorphisms p^*: A\to P(1). For each a\in A we define U_a as the set of points p\in S(A) such that p^*(a) =\{*\}. It is easy to verify that this defines a frame homomorphism A\to P(S(A)), whose image is therefore a topology on
S(
A). Then, if f: A\to B is a map of locales, to each point p\in S(A) we assign the point S(f)(q) defined by letting S(f)(p)^* be the composition of p^* with f^*, hence obtaining a continuous map S(f): S(A)\to S(B). This defines a functor S from
Loc to
Top, which is right adjoint to
O. Any locale that is isomorphic to the topology of its spectrum is called
spatial, and any topological space that is homeomorphic to the spectrum of its locale of open sets is called
sober. The adjunction between topological spaces and locales restricts to an
equivalence of categories between sober spaces and spatial locales. Any function that preserves all joins (and hence any frame homomorphism) has a right adjoint, and, conversely, any function that preserves all meets has a left adjoint. Hence, the category
Loc is isomorphic to the category whose objects are the frames and whose morphisms are the meet preserving functions whose left adjoints preserve finite meets. This is often regarded as a representation of
Loc, but it should not be confused with
Loc itself, whose morphisms are formally the same as frame homomorphisms in the opposite direction. == Literature ==