nLab Sierpinski space

Contents

Context

Topology

topology (point-set topology, point-free topology)

see also differential topology, algebraic topology, functional analysis and topological homotopy theory

Introduction

Basic concepts

Universal constructions

Extra stuff, structure, properties

Examples

Basic statements

Theorems

Analysis Theorems

topological homotopy theory

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}\{0,1\},

  2. whose set of open subsets is {,{1},{0,1}}\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 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 PP of Σ\Sigma is open as long as it is upward closed: pqp \Rightarrow q and pPp \in P imply that qPq \in P. The ability to place a topology on Top(X,Σ)\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:Σ1:\Sigma
  • A meet operation ()():Σ×ΣΣ(-)\wedge(-): \Sigma \times \Sigma \to \Sigma
  • A left unit identity for meet
    m λ: a:Σ1a=am_\lambda:\prod_{a:\Sigma} 1 \wedge a = a
  • A right unit identity for meet
    m ρ: a:Σa1=am_\rho:\prod_{a:\Sigma} a \wedge 1 = a
  • A associative identity for meet
    m α: a:Σ b:Σ c:Σ(ab)c=a(bc)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 κ: a:Σ b:Σab=bam_\kappa:\prod_{a:\Sigma} \prod_{b:\Sigma} a \wedge b = b \wedge a
  • An idempotent identity for meet
    m ι: a:Σaa=am_\iota:\prod_{a:\Sigma} a \wedge a = a
  • A bottom term 0:Σ0:\Sigma
  • A join operation ()():Σ×ΣΣ(-)\vee(-): \Sigma \times \Sigma \to \Sigma
  • A left unit identity for join
    j λ: a:Σ0a=aj_\lambda:\prod_{a:\Sigma} 0 \vee a = a
  • A right unit identity for join
    j ρ: a:Σa0=aj_\rho:\prod_{a:\Sigma} a \vee 0 = a
  • A associative identity for join
    j α: a:Σ b:Σ c:Σ(ab)c=a(bc)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 κ: a:Σ b:Σab=baj_\kappa:\prod_{a:\Sigma} \prod_{b:\Sigma} a \vee b = b \vee a
  • An idempotent identity for join
    j ι: a:Σaa=aj_\iota:\prod_{a:\Sigma} a \vee a = a
  • A meet-join absorption identity
    m j: a:Σ b:Σa(ab)=am_j:\prod_{a:\Sigma} \prod_{b:\Sigma} a \wedge (a \vee b) = a
  • A join-meet absorption identity
    j m: a:Σ b:Σa(ab)=aj_m:\prod_{a:\Sigma} \prod_{b:\Sigma} a \vee (a \wedge b) = a
  • A sequential join function:
    n:()(n):(Σ)Σ\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to \Sigma) \to \Sigma
  • An ascending sequence condition:
    s: n: s:Σs(n)( i:s(i))=s(n)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: x:Σ s:Σ( n:s(n)x=s(n))(( n:s(n))x= n:s(n))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: x:Σ s:Σ𝓉(x,s)(n)=xs(n)p:\prod_{x:\Sigma} \prod_{s:\mathbb{N} \to \Sigma} \mathcal{t}(x,s)(n) = x \wedge s(n)
  • A sequentially distributive condition:
    d: x:Σ s:Σx( n:s(n))= n:𝓉(x,s)(n)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
    τ 0: a:Σ b:ΣisProp(a=b)\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 n:()(n):(Σ)Σ\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:Σ,b:Σπ(a,b):isProp(ab)a:\Sigma, b:\Sigma \vdash \pi(a,b):isProp(a \leq b)

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

  • a family of dependent terms

    a:Σρ(a):aaa:\Sigma \vdash \rho(a):a \leq a

    representing the reflexive property of \leq.

  • a family of dependent terms

    a:Σ,b:Σ,c:Στ(a,b,c):(ab)×(bc)(ac)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:Σ,b:Σσ(a,b):(ab)×(ba)(a=b)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:Σt(a):aa:\Sigma \vdash t(a):\bot \leq a

    representing that \bot is initial in the poset.

  • three families of dependent terms

    a:Σ,b:Σi a(a,b):aaba:\Sigma, b:\Sigma \vdash i_a(a, b):a \leq a \vee b
    a:Σ,b:Σi b(a,b):baba:\Sigma, b:\Sigma \vdash i_b(a, b):b \leq a \vee b
    a:Σ,b:Σ,()():Σ×ΣΣ,i a(a,b):aab,i b(a,b):babi(a,b):(ab)(ab)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:,s:Σi(n,s):s(n) n:s(n)n:\mathbb{N}, s:\mathbb{N} \to \Sigma \vdash i(n, s):s(n) \leq \Vee_{n:\mathbb{N}} s(n)
    x:Σ,s:Σi(s,x): n:(s(n)x)( n:s(n)x)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:Σt(a):aa:\Sigma \vdash t(a):a \leq \top

    representing that \top is terminal in the poset.

  • three families of dependent terms

    a:Σ,b:Σp a(a,b):abaa:\Sigma, b:\Sigma \vdash p_a(a, b):a \wedge b \leq a
    a:Σ,b:Σp b(a,b):abba:\Sigma, b:\Sigma \vdash p_b(a, b):a \wedge b \leq b
    a:Σ,b:Σ,()():Σ×ΣΣ,p a(a,b):aab,p b(a,b):babp(a,b):(ab)(ab)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:Σ,s:Σi(s,x):( n:(s(n)x))( n:s(n)x)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 SierpSierp.

As a classifer for open/closed subspaces

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

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

References

Last revised on June 9, 2022 at 19:02:22. See the history of this page for a list of all contributions to it.