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

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

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

Proof

$\blacksquare$