Category of Locales with Localic Mappings is Isomorphic to Category of Locales/Lemma 1

== Theorem ==
Let $\mathbf{Loc}$ denote the category of locales.
Let $\mathbf{Loc_*}$ denote the category of locales with localic mappings.
Let $F : \mathbf{Loc} \to \mathbf{Loc_*}$ be defined by:
:for each locale $L$ of $\mathbf{Loc_*} : \map F L = L$
:for each continuous map $f : L_1 \to L_2$ of $\mathbf{Loc} : \map F f = f_*$
where:
:$f_* : L_1 \to L_2$ denotes the upper adjoint of the frame homomorphism $f^* : L_2 \to L_1$
:$f = \paren{f^*}^{\operatorname{op}}$
Then:
:$F : \mathbf{Loc} \to \mathbf{Loc_*}$ is a well-defined covariant functor
== Proof ==
=== $F$ is Well-defined ===
By definition of $\mathbf{Loc}$ and $\mathbf {Loc_*}$ the objects of $\mathbf{Loc}$ are the objects of $\mathbf{Loc_*}$.
The object functor of $F$ is the identity object functor and so is well-defined.
Let $f : L_1 \to L_2$ be a continuous map of $\mathbf{Loc}$.
By definition of continuous map:
:there exists a frame homomorphism $\loweradjoint f : L_2 \to L_1$ such that $f = \paren{\loweradjoint f}^{\operatorname{op}}$.
From Frame Homomorphism is Lower Adjoint of Galois Connection:
:there exists an upper adjoint $\upperadjoint f$ such that $\tuple{\upperadjoint f, \loweradjoint f}$ is a Galois connection.
From Galois Connection is Unique for Given Lower Adjoint, it follows that $\loweradjoint f$ is unique.
Hence the morphism functor of $F$ is well-defined.
=== $F$ Preserves Composition of Morphisms ===
Let $L_1, L_2, L_3$ be locales.
Let $f : L_1 \to L_2, g : L_2 \to L_3$ be a continuous maps of $\mathbf{Loc}$.
Let $\tuple{\upperadjoint f, \loweradjoint f}$ be the Galois connection such that:
:$f = \paren{\loweradjoint f}^{\operatorname{op}}$
:$\map F f = \upperadjoint f$
Let $\tuple{\upperadjoint g, \loweradjoint g}$ be the Galois connection such that:
:$g = \paren{\loweradjoint g}^{\operatorname{op}}$
:$\map F g = \upperadjoint g$
Let $\tuple{\upperadjoint {\paren{g \circ f}}, \loweradjoint {\paren{g \circ f}}}$ be the Galois connection such that:
:$g \circ f = \paren{\loweradjoint {\paren{g \circ f}}}^{\operatorname{op}}$
:$\map F {g \circ f} = \upperadjoint {\paren{g \circ f}}$
We have:
Hence $F$ preserves composition.
=== $F$ Preserves Identity Morphisms ===
Let $L$ be a locale.
Let $\operatorname{id}_L : L \to L$ be the identity mapping on $L$.
Let $\tuple{\upperadjoint {\paren{\operatorname{id}_L}}, \loweradjoint {\paren{\operatorname{id}_L}}}$ be the Galois connection such that:
:$\operatorname{id}_L = \paren{\loweradjoint {\paren{\operatorname{id}_L}}}^{\operatorname{op}}$
:$\map F {\operatorname{id}_L} = \upperadjoint {\paren{\operatorname{id}_L}}$
By definition of dual category:
:$\operatorname{id}_L = \paren{\operatorname{id}_L}^{\operatorname{op}}$
So:
:$\paren{\operatorname{id}_L}^{\operatorname{op}} = \paren{\loweradjoint {\paren{\operatorname{id}_L}}}^{\operatorname{op}}$
By definition of dual category:
:$\operatorname{id}_L = \loweradjoint {\paren{\operatorname{id}_L}}$
From Identity Mapping forms Galois Connection:
:$\tuple{\operatorname{id}_L, \operatorname{id}_L}$ is a Galois connection
From Galois Connection is Unique for Given Lower Adjoint:
:$\tuple{\upperadjoint {\paren{\operatorname{id}_L}}, \loweradjoint {\paren{\operatorname{id}_L}}} = \tuple{\operatorname{id}_L, \operatorname{id}_L}$
We have:
Hence $F$ preserves identities.
The result follows.
Category:Category of Locales with Localic Mappings is Isomorphic to Category of Locales