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

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

Then:

$F : \mathbf{Loc} \to \mathbf{Loc_*}$ is a well-defined functor

Proof

$\blacksquare$