Sober Space iff Completely Prime Filter is Unique System of Open Neighborhoods/Necessary Condition

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\struct{S, \tau}$ be a $\struct{S, \tau}$ is a sober space.

For each $x \in S$, let:

$\map \UU x$ denote the system of open neighborhoods of $x$


Then:

for each completely prime filter $\FF$ in the complete lattice $\struct{\tau, \subseteq}$:
$\exists ! x \in S : \FF = \map \UU x$


Proof

Recall by definition of system of open neighborhoods:

$\forall x \in S : \map \UU x = \set{U \in \tau : x \in U}$


Let $\FF$ be a completely prime filter of $\struct{\tau, \subseteq}$.


Let $W = \bigcup \set{U \in \tau : U \notin \FF}$.


By the contrapositive statement of the definition of completely prime filter:

$W \notin \FF$


From Completely Prime Filter Induces Meet-Irreducible Open Set:

$W$ is a meet-irreducible open set

By definition of sober space:

$\exists ! x \in S : W = S \setminus \set x^-$


We have:

\(\ds \forall U \in \tau: \, \) \(\ds U \notin \FF\) \(\leadsto\) \(\ds U \subseteq W\) Set is Subset of Union
\(\ds \) \(\leadsto\) \(\ds U \subseteq S \setminus \set x^-\) As $W = S \setminus x^-$
\(\ds \) \(\leadstoandfrom\) \(\ds U \notin \map \UU x\) Open Set Not in System of Open Neighborhoods Iff Subset of Complement of Singleton Closure


We also have

\(\ds \forall U \in \tau: \, \) \(\ds U \notin \map \UU x\) \(\leadsto\) \(\ds U \subseteq S \setminus \set x^-\) Open Set Not in System of Open Neighborhoods Iff Subset of Complement of Singleton Closure
\(\ds \) \(\leadsto\) \(\ds U \subseteq W\) As $W = S \setminus x^-$
\(\ds \) \(\leadsto\) \(\ds U \notin \FF\) Filter Axiom $\paren{3}$ and $W \notin \FF$


Hence:

$\forall U \in \tau : U \notin \FF \iff U \notin \map \UU x$


From Biconditional Equivalent to Biconditional of Negations:

$\forall U \in \tau : U \in \FF \iff U \in \map \UU x$

By definition of set equality:

$\FF = \map \UU x$


From System of Open Neighborhoods are Equal Iff Singleton Closures are Equal:

$x$ is unique


The result follows.

$\blacksquare$


Also see