Theorem: Characterization of Isomorphism in Loc*/Isomorphism iff Lower Adjoint is Frame Isomorphism

Let $\mathbf{Loc_*}$ denote the category of locales with localic mappings.
Let $\mathbf{Frm}$ denote the category of frames.
Let $L_1 = \struct{S_1, \preceq_1}$ and $L_2 = \struct{S_2, \preceq_2}$ be locales.
Let $f:L_1 \to L_2$ be a localic mapping of $\mathbf{Loc_*}$.
Let $\loweradjoint f : L_2 \to L_1$ be the lower adjoint of $f$ in $\mathbf{Frm}$.
Then:
:$f$ is an isomorphism of $\mathbf{Loc_*}$ {{iff}} $\loweradjoint f$ is a frame isomorphism.

Proof:
==== Necessary Condition ====
Let $f$ be an isomorphism of $\mathbf{Loc_*}$.
By definition of isomorphism:
:there exists a localic mapping $g: L_2 \to L_1$ of $\mathbf{Loc_*}$:
::$g \circ f = \operatorname{id}_{L_1}$
:and
::$f \circ g = \operatorname{id}_{L_2}$
By definition of localic mapping:
:$g$ has a lower adjoint $\loweradjoint g : L_1 \to L_2$ in $\mathbf{Frm}$
By definition of localic mapping:
:$\tuple{f, \loweradjoint f}, \tuple{g, \loweradjoint g}$ are galois connections
From Composition of Galois Connections is Galois Connection:
:$\tuple{g \circ f, \loweradjoint f \circ \loweradjoint g}, \tuple{f \circ g, \loweradjoint g \circ \loweradjoint f}$ are galois connections
Hence:
:$\tuple{\operatorname{id}_{L_1}, \loweradjoint f \circ \loweradjoint g}, \tuple{\operatorname{id}_{L_2}, \loweradjoint g \circ \loweradjoint f}$ are galois connections
From Identity Mapping forms Galois Connection:
:$\tuple{\operatorname{id}_{L_1}, \operatorname{id}_{L_1}}, \tuple{\operatorname{id}_{L_2}, \operatorname{id}_{L_2}}$ are galois connections
From Galois Connection is Unique for Given Upper Adjoint:
:$\loweradjoint f \circ \loweradjoint g = \operatorname{id}_{L_1}$
and:
:$\loweradjoint g \circ \loweradjoint f = \operatorname{id}_{L_2}$
By definition of category of frames:
:$\loweradjoint f$ and $\loweradjoint g$ are isomorphisms in $\mathbf{Frm}$
From Frame Isomorphism is Isomorphism in Category Frm:
:$\loweradjoint f$ and $\loweradjoint g$ are frame isomorphisms
{{qed|lemma}}
==== Sufficient Condition ====
Let $\loweradjoint f$ be a frame isomorphism.
From Frame Isomorphism is Isomorphism in Category Frm:
:$\loweradjoint f$ is an isomorphism in $\mathbf{Frm}$
Let $\loweradjoint g : L_1 \to L_2$ be a frame homomorphism in $\mathbf{Frm}$:
:$\loweradjoint f \circ \loweradjoint g = \operatorname{id}_{L_1}$
and:
:$\loweradjoint g \circ \loweradjoint f = \operatorname{id}_{L_2}$
From Frame Homomorphism is Lower Adjoint of Galois Connection:
:there exists a localic mapping $\upperadjoint g : L_2 \to L_1$ such that $\tuple{\upperadjoint g, \loweradjoint g}$ is a galois connection
By definition of localic mapping:
:$\tuple{f, \loweradjoint f}$ is a galois connection
From Composition of Galois Connections is Galois Connection:
:$\tuple{\upperadjoint g \circ f, \loweradjoint f \circ \loweradjoint g}, \tuple{f \circ \upperadjoint g, \loweradjoint g \circ \loweradjoint f}$ are galois connections
Hence:
:$\tuple{\upperadjoint g \circ f, \operatorname{id}_{L_1}}, \tuple{f \circ \upperadjoint g, \operatorname{id}_{L_2}}$ are galois connections
From Identity Mapping forms Galois Connection:
:$\tuple{\operatorname{id}_{L_1}, \operatorname{id}_{L_1}}, \tuple{\operatorname{id}_{L_2}, \operatorname{id}_{L_2}}$ are galois connections
From Galois Connection is Unique for Given Lower Adjoint:
:$\upperadjoint g \circ f = \operatorname{id}_{L_1}$
and:
:$f \circ \upperadjoint g = \operatorname{id}_{L_2}$
By definition of isomorphism:
:$f$ be an isomorphism of $\mathbf{Loc_*}$