Contents

Contents

Definition

In impredicative mathematics

Definition

The Sierpiński space $\Sigma$ is the topological space

1. whose underlying set has two elements, say $\{0,1\}$,

2. whose set of open subsets is $\left\{ \emptyset, \{1\}, \{0,1\} \right\}$.

(We could exchange “0” and “1” here, the result would of course be homeomorphic).

Equivalently we may think of the underlying set as the set of classical truth values $\{\bot, \top\}$, equipped with the specialization topology, in which $\{\bot\}$ is closed and $\{\top\}$ is an open but not conversely.

Remark

In constructive mathematics, it is important that $\{\top\}$ be open (and $\{\bot\}$ closed), rather than the other way around. Indeed, the general definition (since we can't assume that every element is either $\top$ or $\bot$) is that a subset $P$ of $\Sigma$ is open as long as it is upward closed: $p \Rightarrow q$ and $p \in P$ imply that $q \in P$. The ability to place a topology on $\Top(X,\Sigma)$ is fundamental to abstract Stone duality, a constructive approach to general topology.

In predicative constructive mathematics

Definition

The Sierpiński space $\Sigma$ is the initial $\sigma$-frame.

As a higher inductive type

In type theory, as a higher inductive type Sierpinski space $\Sigma$ is generated by the following constructors:

• A type $\Sigma$,
• A top term $1:\Sigma$
• A meet operation $(-)\wedge(-): \Sigma \times \Sigma \to \Sigma$
• A left unit identity for meet
$m_\lambda:\prod_{a:\Sigma} 1 \wedge a = a$
• A right unit identity for meet
$m_\rho:\prod_{a:\Sigma} a \wedge 1 = a$
• A associative identity for meet
$m_\alpha:\prod_{a:\Sigma} \prod_{b:\Sigma} \prod_{c:\Sigma} (a \wedge b) \wedge c = a \wedge (b \wedge c)$
• A commutative identity for meet
$m_\kappa:\prod_{a:\Sigma} \prod_{b:\Sigma} a \wedge b = b \wedge a$
• An idempotent identity for meet
$m_\iota:\prod_{a:\Sigma} a \wedge a = a$
• A bottom term $0:\Sigma$
• A join operation $(-)\vee(-): \Sigma \times \Sigma \to \Sigma$
• A left unit identity for join
$j_\lambda:\prod_{a:\Sigma} 0 \vee a = a$
• A right unit identity for join
$j_\rho:\prod_{a:\Sigma} a \vee 0 = a$
• A associative identity for join
$j_\alpha:\prod_{a:\Sigma} \prod_{b:\Sigma} \prod_{c:\Sigma} (a \vee b) \vee c = a \vee (b \vee c)$
• A commutative identity for join
$j_\kappa:\prod_{a:\Sigma} \prod_{b:\Sigma} a \vee b = b \vee a$
• An idempotent identity for join
$j_\iota:\prod_{a:\Sigma} a \vee a = a$
• A meet-join absorption identity
$m_j:\prod_{a:\Sigma} \prod_{b:\Sigma} a \wedge (a \vee b) = a$
• A join-meet absorption identity
$j_m:\prod_{a:\Sigma} \prod_{b:\Sigma} a \vee (a \wedge b) = a$
• A sequential join function:
$\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to \Sigma) \to \Sigma$
• An ascending sequence condition:
$s: \prod_{n:\mathbb{N}} \prod_{s:\mathbb{N} \to \Sigma} s(n) \wedge \left(\Vee_{i:\mathbb{N}} s(i)\right) = s(n)$
• A sequential least upper bound condition:
$l: \prod_{x:\Sigma} \prod_{s:\mathbb{N} \to \Sigma} \left(\prod_{n:\mathbb{N}} s(n) \wedge x = s(n)\right) \to \left(\left(\Vee_{n:\mathbb{N}} s(n)\right) \wedge x = \Vee_{n:\mathbb{N}} s(n)\right)$
• A function
$\mathcal{t}:(\Sigma \times (\mathbb{N} \to \Sigma)) \to \mathbb{N} \to \Sigma$
• A dependent function
$p:\prod_{x:\Sigma} \prod_{s:\mathbb{N} \to \Sigma} \mathcal{t}(x,s)(n) = x \wedge s(n)$
• A sequentially distributive condition:
$d: \prod_{x:\Sigma} \prod_{s:\mathbb{N} \to \Sigma} x \wedge \left(\Vee_{n:\mathbb{N}} s(n)\right) = \Vee_{n:\mathbb{N}} \mathcal{t}(x,s)(n)$
• A 0-truncator
$\tau_0: \prod_{a:\Sigma} \prod_{b:\Sigma} isProp(a=b)$

As a higher inductive-inductive type

The Sierpinski space $\Sigma$ is inductively generated by

• a term $\bot:\Sigma$
• a binary operation $(-)\vee(-):\Sigma \times \Sigma \to \Sigma$
• a function $\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to \Sigma) \to \Sigma$
• a term $\top:\Sigma$
• a binary operation $(-)\wedge(-):\Sigma \times \Sigma \to \Sigma$

and the partial order type family $\leq$ is simultaneously inductively generated by

• a family of dependent terms

$a:\Sigma, b:\Sigma \vdash \pi(a,b):isProp(a \leq b)$

representing that each type $a \leq b$ is a proposition.

• a family of dependent terms

$a:\Sigma \vdash \rho(a):a \leq a$

representing the reflexive property of $\leq$.

• a family of dependent terms

$a:\Sigma, b:\Sigma, c:\Sigma \vdash \tau(a, b, c):(a \leq b) \times (b \leq c) \to (a \leq c)$

representing the transitive property of $\leq$.

• a family of dependent terms

$a:\Sigma, b:\Sigma \vdash \sigma(a, b):(a \leq b) \times (b \leq a) \to (a = b)$

representing the anti-symmetric property of $\leq$.

• a family of dependent terms

$a:\Sigma \vdash t(a):\bot \leq a$

representing that $\bot$ is initial in the poset.

• three families of dependent terms

$a:\Sigma, b:\Sigma \vdash i_a(a, b):a \leq a \vee b$
$a:\Sigma, b:\Sigma \vdash i_b(a, b):b \leq a \vee b$
$a:\Sigma, b:\Sigma, (-)\oplus(-):\Sigma \times \Sigma \to \Sigma, i_a(a, b):a \leq a \oplus b, i_b(a, b):b \leq a \oplus b \vdash i(a,b):(a \vee b) \leq (a \oplus b)$

representing that $\vee$ is a coproduct in the poset.

• two families of dependent terms

$n:\mathbb{N}, s:\mathbb{N} \to \Sigma \vdash i(n, s):s(n) \leq \Vee_{n:\mathbb{N}} s(n)$
$x:\Sigma, s:\mathbb{N} \to \Sigma \vdash i(s, x):\prod_{n:\mathbb{N}}(s(n) \leq x) \to \left(\Vee_{n:\mathbb{N}} s(n) \leq x\right)$

representing that $\Vee$ is a denumerable/countable coproduct in the poset.

• a family of dependent terms

$a:\Sigma \vdash t(a):a \leq \top$

representing that $\top$ is terminal in the poset.

• three families of dependent terms

$a:\Sigma, b:\Sigma \vdash p_a(a, b):a \wedge b \leq a$
$a:\Sigma, b:\Sigma \vdash p_b(a, b):a \wedge b \leq b$
$a:\Sigma, b:\Sigma, (-)\otimes(-):\Sigma \times \Sigma \to \Sigma, p_a(a, b):a \leq a \otimes b, p_b(a, b):b \leq a \otimes b \vdash p(a,b):(a \otimes b) \leq (a \wedge b)$

representing that $\wedge$ is a product in the poset.

• a family of dependent terms

$x:\Sigma, s:\mathbb{N} \to \Sigma \vdash i(s, x):\left(\prod_{n:\mathbb{N}}(s(n) \leq x)\right) \to \left(\Vee_{n:\mathbb{N}} s(n) \leq x\right)$

representing the countably infinitary distributive property.

Properties

As a topological space

This Sierpinski space

According properties are inherited by the Sierpinski topos and the Sierpinski (∞,1)-topos over $Sierp$.

As a classifer for open/closed subspaces

The Sierpinski space $S$ is a classifier for open subspaces of a topological space $X$ in that for any open subspace $A$ of $X$ there is a unique continuous function $\chi_A: X \to S$ such that $A = \chi_A^{-1}(\top)$.

Dually, it classifies closed subsets in that any closed subspace $A$ is $\chi_A^{-1}(\bot)$. Note that the closed subsets and open subsets of $X$ are related by a bijection through complementation; one gets a topology on the set of either by identifying the set with $\Top(X,\Sigma)$ for a suitable function space topology. (This part does not work as well in constructive mathematics.)

References

Last revised on March 8, 2023 at 13:56:11. See the history of this page for a list of all contributions to it.