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

== Theorem ==
Let $\mathbf{Loc}$ denote the category of locales.
Let $\mathbf{Loc_*}$ denote the category of locales with localic mappings.
Let $G : \mathbf{Loc_*} \to \mathbf{Loc}$ be defined by:
:for each locale $L$ of $\mathbf{Loc_*} : \map G L = L$
:for each localic mapping $g : L_1 \to L_2$ of $\mathbf{Loc_*} : \map G g = \paren{\loweradjoint g}^{\operatorname{op}}$
where:
:$\loweradjoint g : L_2 \to L_1$ denotes the frame homomorphism that is the lower adjoint of the localic mapping $g$
:$\paren{\loweradjoint g}^{\operatorname{op}}$ denotes the opposite morphism of the frame homomorphism
Then:
:$G : \mathbf{Loc_*} \to \mathbf{Loc}$ is a well-defined covariant functor
== Proof ==
=== $G$ 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 $G$ is the identity object functor and so is well-defined.
Let $g : L_1 \to L_2$ be a localic mapping of $\mathbf{Loc_*}$.
By definition of localic mapping:
:there exists a Galois connection $\tuple{\upperadjoint g, \loweradjoint g}$ such that $g = \upperadjoint g$ and $\loweradjoint g$ is a frame homomorphism.
From Galois Connection is Unique for Given Upper Adjoint, it follows that the Galois connection $\tuple{\upperadjoint g, \loweradjoint g}$ is unique.
By definition of dual category:
:$\paren{\loweradjoint g}^{\operatorname{op}}$ is a morphism of $\mathbf {Loc}$.
Hence the morphism functor of $G$ is well-defined.
=== $G$ Preserves Composition of Morphisms ===
Let $L_1, L_2, L_3$ be locales.
Let $g : L_1 \to L_2, h : L_2 \to L_3$ be localic mappings of $\mathbf{Loc_*}$.
Let $\tuple{\upperadjoint g, \loweradjoint g}$ be the Galois connection such that:
:$g = \upperadjoint g$
:$\map G g = \paren{\loweradjoint g}^{\operatorname{op} }$
Let $\tuple{\upperadjoint h, \loweradjoint h}$ be the Galois connection such that:
:$h = \upperadjoint h$
:$\map G h = \paren{\loweradjoint h}^{\operatorname{op} }$
Let $\tuple{\upperadjoint {\paren{h \circ g}}, \loweradjoint {\paren{h \circ g}}}$ be the Galois connection such that:
:$h \circ g = \upperadjoint {\paren{h \circ g}}$
:$\map G {h \circ g} = \paren{\loweradjoint {\paren{h \circ g}}}^{\operatorname{op} }$
We have:
Hence $G$ preserves composition.
=== $G$ Preserves Identity Morphisms ===
Let $L$ be a locale.
Let $\operatorname{id}_L : L \to L$ be the identity mapping on $L$.
Let $\tuple{\upperadjoint {\operatorname{id}_L}, \loweradjoint {\operatorname{id}_L}}$ be the Galois connection such that:
:$\operatorname{id}_L = \upperadjoint {\paren{\operatorname{id}_L}}$
:$\map G {\operatorname{id}_L} = \paren{\loweradjoint {\paren{\operatorname{id}_L}}}^{\operatorname{op} }$
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 $G$ preserves identities.
The result follows.
Category:Category of Locales with Localic Mappings is Isomorphic to Category of Locales