Theorem: Homeomorphism Preserves Sobriety

Let $T_1 = \struct{S_1, \tau_1}$ be a sober space.
Let $T_2 = \struct{S_2, \tau_2}$ be a topological space.
Let $f : T_1 \to T_2$ be a homeomorphism.
Then:
:$T_2$ is a sober space.

Proof:
From Sober Space iff Completely Prime Filter is Unique System of Open Neighborhoods it is sufficent to show:
:for each completely prime filter $\FF$ in the complete lattice $\struct{\tau_2, \subseteq}$:
::$\exists ! y \in S_2 : \FF = \map \UU y$
Let $f^{-1}$ denote the inverse of $f$.
From Inverse of Homeomorphism is Homeomorphism:
:$f^{-1} : T_2 \to T_1$ is a homeomorphism
Let $\FF$ be a completely prime filter in $\struct{\tau_2, \subseteq}$.
From Frame Homomorphism of Continuous Mapping is Frame Homomorphism:
:the mapping $\map \Omega {f^{-1} } : \tau_1 \to \tau_2$ defined by: $\map {\map \Omega {f^{-1} } } U = \map { \paren{f^{-1} }^\gets} U$
is a frame homomorphism, where:
:$\paren{f^{-1} }^\gets : \powerset {S_1} \to \powerset {S_2}$ denotes the inverse image mapping of $f^{-1}$
From Inverse Image Mapping of Frame Homomorphism Preserves Completely Prime Filter:
:$\map {\map \Omega {f^{-1} }^\gets} \FF$ is a completely prime filter of $\struct{\tau_1, \subseteq}$
We have {{hypothesis}}:
:$T_1$ is a sober space
From Sober Space iff Completely Prime Filter is Unique System of Open Neighborhoods:
:$(1):\quad \exists ! x \in S_1 : \map {\map \Omega {f^{-1} }^\gets} \FF = \map \UU x$
Consider:
:$(2):\quad y = \map f x \in S_2$.
We have:
{{begin-eqn}}
{{eqn | l = \map \UU y
      | r = \map \UU {\map f x}
      | c = by $(2)$
}}
{{eqn | r = f^\to \sqbrk {\map \UU x}
      | c = Homeomorphism Preserves System of Open Neighborhoods
}}
{{eqn | r = f^\to \sqbrk {\map {\map \Omega {f^{-1} }^\gets} \FF}
      | c = by $(1)$
}}
{{eqn | r = f^\to \sqbrk {\map \Omega {f^{-1} }^{-1} \sqbrk \FF}
      | c = {{Defof|Inverse Image Mapping}}
}}
{{eqn | r = f^\to \sqbrk {\paren{\paren {f^{-1} }^\gets}^{-1} \sqbrk \FF}
      | c = {{Defof|Frame Homomorphism of Continuous Mapping}}
}}
{{eqn | r = f^\to \sqbrk {\paren {f^{-1} }^\to \sqbrk \FF}
      | c = Inverse Image Mapping of Bijection is Inverse of Direct Image Mapping
}}
{{eqn | r = \paren{f^\to \circ {\paren {f^{-1} }^\to} } \sqbrk \FF
      | c = Preimage of Subset under Composite Mapping
}}
{{eqn | r = \paren{f^\to \circ {\paren {f^{\to} }^{-1} } } \sqbrk \FF
      | c = Inverse of Direct Image Mapping is Direct Image Mapping of Inverse
}}
{{eqn | n = 3
      | r = \FF
      | c = {{Defof|Inverse Mapping}}
}}
{{end-eqn}}
We now show the uniqueness of $y$.
Let:
:$(4) \quad \map \UU {y'} = \FF$.
We have {{hypothesis}}:
:$f$ is a surjection
By definition of surjection:
:$(5) \quad \exists x'\in S_1 : \map f {x'} = y'$
We have:
{{begin-eqn}}
{{eqn | l = \map \UU {y'}
      | r = \map \UU y
      | c = from $(3)$ and $(4)$
}}
{{eqn | ll = \leadsto
      | l = \map \UU {\map f {x'} }
      | r = \map \UU {\map f x}
      | c = from $(2)$ and $(5)$
}}
{{eqn | ll = \leadsto
      | l = f^\to \sqbrk {\map \UU {x'} }
      | r = f^\to \sqbrk {\map \UU x}
      | c = Homeomorphism Preserves System of Open Neighborhoods
}}
{{eqn | ll = \leadsto
      | l = \map \UU {x'}
      | r = \map \UU x
      | c = Mapping is Bijection iff Direct Image Mapping is Bijection
}}
{{eqn | ll = \leadsto
      | l = x'
      | r = x
      | c = Sober Space iff Completely Prime Filter is Unique System of Open Neighborhoods
}}
{{eqn | ll = \leadsto
      | l = \map f x'
      | r = \map f x
      | c = {{Defof|Mapping}}
}}
{{eqn | ll = \leadsto
      | l = y'
      | r = y
      | c = from $(2)$ and $(5)$
}}
{{end-eqn}}
The result follows.
{{qed}}
Category:Sober Spaces
Category:Homeomorphisms (Topological Spaces)
rqqhd0erjk8xb9o0tn7h066nufsoh6n