Theorem: Characterization of Localic Mapping Induced by Continuous Mapping

Let $T_1 = \struct{S_1, \tau_1}, T_2 = \struct{S_2, \tau_2}$ be topological spaces.
Let $f: T_1 \to \T_2$ be a continuous mapping.
Let $\map \Omega {T_1}, \map \Omega {T_2}$ be the locales of $T_1$ and $T_2$ respectively.
Let $F : \map \Omega {T_1} \to \map \Omega {T_2}$ be the localic mapping induced by $f$.
Then:
:$\forall U \in \tau_1 : \map F U = S_2 \setminus f \sqbrk{S_1 \setminus U}^-$
where:
:$S_2 \setminus f \sqbrk{S_1 \setminus U}^-$ denotes the relative complement of $f \sqbrk{S_1 \setminus U}^-$ in $S_2$ 
:$f \sqbrk{S_1 \setminus U}^-$ denotes the closure of $f \sqbrk{S_1 \setminus U}$ in $T_2$
:$f \sqbrk{S_1 \setminus U}$ denotes the image of $S_1 \setminus U$ under $f$
:$S_1 \setminus U$ denotes the relative complement of $U$ in $S_1$

Proof:
Let $G : \map \Omega {T_2} \to \map \Omega {T_1}$ be the frame homomorphism of $f$.
By definition of localic mapping induced by $f$, $F$ is the upper adjoint to $G$.
Hence:
:$\tuple{F, G}$ is a Galois connection
We have:
{{begin-eqn}}
{{eqn | q = \forall U \in \tau_1, V \in \tau_2
      | l = V
      | o = \subseteq
      | r = \map F U
}}
{{eqn | ll = \leadstoandfrom
      | l = \map G V
      | o = \subseteq
      | r = U
      | c = {{Defof|Galois Connection}}
}}
{{eqn | ll = \leadstoandfrom
      | l = f^{-1} \sqbrk V
      | o = \subseteq
      | r = U
      | c = {{Defof|Frame Homomorphism of Continuous Mapping}}
}}
{{eqn | n = 1
      | ll = \leadstoandfrom
      | l = V
      | o = \subseteq
      | r = S_2 \setminus f \sqbrk {S_1 \setminus U}
      | c = Preimage is Subset Iff Subset of Complement of Image of Complement
}}
{{end-eqn}}
Next, we have:
{{begin-eqn}}
{{eqn | q = \forall U \in \tau_1
      | l = \map F U
      | o = \subseteq
      | r = \map F U
      | c = Set is Subset of Itself
}}
{{eqn | o = \subseteq
      | r = S_2 \setminus f \sqbrk {S_1 \setminus U}
      | c = from $\paren 1$ and $\map F U \in \tau_2$
}}
{{eqn | ll = \leadsto
      | q = \forall U \in \tau_1
      | l = f \sqbrk {S_1 \setminus U}
      | o = \subseteq
      | r = S_2 \setminus \map F U
      | c = Relative Complement inverts Subsets of Relative Complement
}}
{{eqn | ll = \leadsto
      | q = \forall U \in \tau_1
      | l = f \sqbrk {S_1 \setminus U}^-
      | o = \subseteq
      | r = S_2 \setminus \map F U
      | c = Closure of Subset of Closed Set of Topological Space is Subset and $S_2 \setminus \map F U$ is closed in $T_2$
}}
{{eqn | ll = \leadsto
      | n = 2
      | q = \forall U \in \tau_1
      | l = \map F U
      | o = \subseteq
      | r = S_2 \setminus f \sqbrk {S_1 \setminus U}^-
      | c = Relative Complement inverts Subsets of Relative Complement
}}
{{end-eqn}}
And we have:
{{begin-eqn}}
{{eqn | q = \forall U \in \tau_1
      | l = f \sqbrk {S_1 \setminus U}
      | o = \subseteq
      | r = f \sqbrk {S_1 \setminus U}^-
      | c = Set is Subset of its Topological Closure
}}
{{eqn | ll = \leadsto
      | q = \forall U \in \tau_1
      | l = S_2 \setminus f \sqbrk {S_1 \setminus U}^-
      | o = \subseteq
      | r = S_2 \setminus f \sqbrk {S_1 \setminus U}
      | c = Relative Complement inverts Subsets
}}
{{eqn | ll = \leadsto
      | q = \forall U \in \tau_1
      | n = 3
      | l = S_2 \setminus f \sqbrk {S_1 \setminus U}^-
      | o = \subseteq
      | r = \map F U
      | c = from $\paren 1$
}}
{{end-eqn}}
From $\paren 2$, $\paren 3$ and set equality:
:$\forall U \in \tau_1 : \map F U = S_2 \setminus f \sqbrk {S_1 \setminus U}^-$
{{qed}}
Category:Localic Mappings
0dhy8uqraimh5ipvyhux9a76yejp55s