nLab
Sierpinski space
Redirected from "Sierpinski topology".
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
open subset , closed subset , neighbourhood
topological space , locale
base for the topology , neighbourhood base
finer/coarser topology
closure , interior , boundary
separation , sobriety
continuous function , homeomorphism
uniformly continuous function
embedding
open map , closed map
sequence , net , sub-net , filter
convergence
category Top
Universal constructions
Extra stuff, structure, properties
nice topological space
metric space , metric topology , metrisable space
Kolmogorov space , Hausdorff space , regular space , normal space
sober space
compact space , proper map
sequentially compact , countably compact , locally compact , sigma-compact , paracompact , countably paracompact , strongly compact
compactly generated space
second-countable space , first-countable space
contractible space , locally contractible space
connected space , locally connected space
simply-connected space , locally simply-connected space
cell complex , CW-complex
pointed space
topological vector space , Banach space , Hilbert space
topological group
topological vector bundle , topological K-theory
topological manifold
Examples
empty space , point space
discrete space , codiscrete space
Sierpinski space
order topology , specialization topology , Scott topology
Euclidean space
cylinder , cone
sphere , ball
circle , torus , annulus , Moebius strip
polytope , polyhedron
projective space (real , complex )
classifying space
configuration space
path , loop
mapping spaces : compact-open topology , topology of uniform convergence
Zariski topology
Cantor space , Mandelbrot space
Peano curve
line with two origins , long line , Sorgenfrey line
K-topology , Dowker space
Warsaw circle , Hawaiian earring space
Basic statements
Theorems
Analysis Theorems
topological homotopy theory
Contents
Definition
In impredicative mathematics
Definition
The Sierpiński space Σ \Sigma is the topological space
whose underlying set has two elements, say { 0 , 1 } \{0,1\} ,
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 classical truth values { ⊥ , ⊤ } \{\bot, \top\} , equipped with the specialization topology , in which { ⊥ } \{\bot\} is closed and { ⊤ } \{\top\} is an open but not conversely.
In predicative constructive mathematics
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 meetm λ : ∏ a : Σ 1 ∧ a = a m_\lambda:\prod_{a:\Sigma} 1 \wedge a = a
A right unit identity for meetm ρ : ∏ a : Σ a ∧ 1 = a m_\rho:\prod_{a:\Sigma} a \wedge 1 = a
A associative identity for meetm α : ∏ a : Σ ∏ b : Σ ∏ c : Σ ( a ∧ b ) ∧ c = a ∧ ( b ∧ c ) 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 meetm κ : ∏ a : Σ ∏ b : Σ a ∧ b = b ∧ a m_\kappa:\prod_{a:\Sigma} \prod_{b:\Sigma} a \wedge b = b \wedge a
An idempotent identity for meetm ι : ∏ a : Σ a ∧ a = a m_\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 joinj λ : ∏ a : Σ 0 ∨ a = a j_\lambda:\prod_{a:\Sigma} 0 \vee a = a
A right unit identity for joinj ρ : ∏ a : Σ a ∨ 0 = a j_\rho:\prod_{a:\Sigma} a \vee 0 = a
A associative identity for joinj α : ∏ a : Σ ∏ b : Σ ∏ c : Σ ( a ∨ b ) ∨ c = a ∨ ( b ∨ c ) 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 joinj κ : ∏ a : Σ ∏ b : Σ a ∨ b = b ∨ a j_\kappa:\prod_{a:\Sigma} \prod_{b:\Sigma} a \vee b = b \vee a
An idempotent identity for joinj ι : ∏ a : Σ a ∨ a = a j_\iota:\prod_{a:\Sigma} a \vee a = a
A meet-join absorption identitym j : ∏ a : Σ ∏ b : Σ a ∧ ( a ∨ b ) = a m_j:\prod_{a:\Sigma} \prod_{b:\Sigma} a \wedge (a \vee b) = a
A join-meet absorption identityj m : ∏ a : Σ ∏ b : Σ a ∨ ( a ∧ b ) = a j_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 functionp : ∏ x : Σ ∏ s : ℕ → Σ 𝓉 ( x , s ) ( n ) = x ∧ s ( 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 ( a ≤ b ) a:\Sigma, b:\Sigma \vdash \pi(a,b):isProp(a \leq b)
representing that each type a ≤ b a \leq b is a proposition .
a family of dependent terms
a : Σ ⊢ ρ ( a ) : a ≤ a a:\Sigma \vdash \rho(a):a \leq a
representing the reflexive property of ≤ \leq .
a family of dependent terms
a : Σ , b : Σ , c : Σ ⊢ τ ( a , b , c ) : ( a ≤ b ) × ( b ≤ c ) → ( a ≤ c ) 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 ) : ( a ≤ b ) × ( b ≤ a ) → ( 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 ) : ⊥ ≤ a a:\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 ) : a ≤ a ∨ b a:\Sigma, b:\Sigma \vdash i_a(a, b):a \leq a \vee b a : Σ , b : Σ ⊢ i b ( a , b ) : b ≤ a ∨ b a:\Sigma, b:\Sigma \vdash i_b(a, b):b \leq a \vee b a : Σ , b : Σ , ( − ) ⊕ ( − ) : Σ × Σ → Σ , i a ( a , b ) : a ≤ a ⊕ b , i b ( a , b ) : b ≤ a ⊕ b ⊢ i ( a , b ) : ( a ∨ b ) ≤ ( a ⊕ 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 : ℕ , 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 ) : a ≤ ⊤ a:\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 ) : a ∧ b ≤ a a:\Sigma, b:\Sigma \vdash p_a(a, b):a \wedge b \leq a a : Σ , b : Σ ⊢ p b ( a , b ) : a ∧ b ≤ b a:\Sigma, b:\Sigma \vdash p_b(a, b):a \wedge b \leq b a : Σ , b : Σ , ( − ) ⊗ ( − ) : Σ × Σ → Σ , p a ( a , b ) : a ≤ a ⊗ b , p b ( a , b ) : b ≤ a ⊗ b ⊢ p ( a , b ) : ( a ⊗ b ) ≤ ( a ∧ 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 : Σ , 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 Sierp Sierp .
As a classifer for open/closed subspaces
The Sierpinski space S S is a classifier for open subspaces of a topological space X X in that for any open subspace A A of X X there is a unique continuous function χ A : X → S \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 A A is χ A − 1 ( ⊥ ) \chi_A^{-1}(\bot) . Note that the closed subsets and open subsets of X X 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 March 8, 2023 at 13:56:11.
See the history of this page for a list of all contributions to it.