Page 22 - Textos de Matemática Vol. 41

8 Chapter 2. Locales, frames and spaces 2.2. Locales and the category Loc. The formulas with Ω constitute a con-
travariant functor
Ω : Top → Frm.
We will see that restricted to sober spaces it is a full embedding. This gives importance to the dual, Frmop, which can then be thought of as a natural extension of the category of (sober) topological spaces.
Morphism in Frmop are, of course, frame homomorphisms taken backwards, which may obscure the intuition. But, since frame homomorphisms h : L → M preserve all joins, they have (uniquely defined) right adjoints h∗ : M → L that can be used as a representation of the h as mappings running in the proper direction. This leads to replacing Frmop by the category of locales
Loc
in which the objects are frames (from now on, also called locales: a third name for the same object, but chosen to emphasize the choice of morphisms one works with), and the morphisms are the localic maps, that is, mappings f : L → M that have left adjoints f∗ preserving finite meets (i.e. f∗(1) = 1 and f∗(a∧b) = f∗(a) ∧ f∗(b) for every a,b ∈ M).
The locale {0 = 1} (one-element frame) will be denoted by O and called the empty or void locale. The two-point Boolean algebra {0 < 1} will be often denoted by P and called the one-point locale. Also, locales isomorphic with O resp. P will be sometimes referred to as empty, resp. one-point ones.
Note that O behaves like a void space, that is, for every locale L there is exactly one localic map O → L and unless L is void itself, there is no L → O. Similarly, P behaves like a one-point space in the sense that for every L there is exactly one localic map L → P. But there is much more to it: see 2.5.1 below.
2.2.1. The following characteristics of localic maps will be useful in the sequel. Proposition. Let f : L → M have a left adjoint f∗. Then
(a) f∗(1) = 1 iff
f [L {1}] ⊆ M {1}, (b) f∗ preserves binary meets iff
f(f∗(a)→b) = a→f(b).
Proof. (a) If f∗(1) = 1 and 1 ≤ f(x) then 1 = f∗(1) ≤ f∗f(x) ≤ x; on the other hand, if the inclusion holds, use the inequality f(f∗(1)) ≥ 1.
and