User:Leigh.Samphier/Topology/Category of Locales with Localic Mappings is Isomorphic to Category of Locales/Lemma 4

This page needs proofreading. Please check it for mathematical errors. If you believe there are none, please remove {{Proofread}} from the code. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Proofread}} from the code.

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 G 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}}$

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{g^*}^{\operatorname{op}}$

where:

$g^* : L_2 \to L_1$ denotes the frame homomorphism that is the lower adjoint of the localic mapping $g$

$\paren{g^*}^{\operatorname{op}}$ denotes the opposite morphism of the frame homomorphism

Then:

$FG = \operatorname{id}_{\mathbf {Loc_*}}$

Proof

$\blacksquare$