Writing the introduction

Jon Sterling 1a87080b

Changed files
+378
+289
.gitignore
···
+
*.ist
+
*.pdf
+
.DS_STORE
+
*.mtc
+
*.ptc
+
*~
+
*#*
+
*.ptb
+
+
*.agdai
+
+
+
+
## Core latex/pdflatex auxiliary files:
+
*.aux
+
*.lof
+
*.log
+
*.lot
+
*.fls
+
*.out
+
*.toc
+
*.fmt
+
*.fot
+
*.cb
+
*.cb2
+
.*.lb
+
+
## Intermediate documents:
+
*.dvi
+
*.xdv
+
*-converted-to.*
+
# these rules might exclude image files for figures etc.
+
# *.ps
+
# *.eps
+
# *.pdf
+
+
## Generated if empty string is given at "Please type another file name for output:"
+
.pdf
+
+
## Bibliography auxiliary files (bibtex/biblatex/biber):
+
*.bbl
+
*.bcf
+
*.blg
+
*-blx.aux
+
*-blx.bib
+
*.run.xml
+
+
## Build tool auxiliary files:
+
*.fdb_latexmk
+
*.synctex
+
*.synctex(busy)
+
*.synctex.gz
+
*.synctex.gz(busy)
+
*.pdfsync
+
+
## Build tool directories for auxiliary files
+
# latexrun
+
latex.out/
+
+
## Auxiliary and intermediate files from other packages:
+
# algorithms
+
*.alg
+
*.loa
+
+
# achemso
+
acs-*.bib
+
+
# amsthm
+
*.thm
+
+
# beamer
+
*.nav
+
*.pre
+
*.snm
+
*.vrb
+
+
# changes
+
*.soc
+
+
# comment
+
*.cut
+
+
# cprotect
+
*.cpt
+
+
# elsarticle (documentclass of Elsevier journals)
+
*.spl
+
+
# endnotes
+
*.ent
+
+
# fixme
+
*.lox
+
+
# feynmf/feynmp
+
*.mf
+
*.mp
+
*.t[1-9]
+
*.t[1-9][0-9]
+
*.tfm
+
+
#(r)(e)ledmac/(r)(e)ledpar
+
*.end
+
*.?end
+
*.[1-9]
+
*.[1-9][0-9]
+
*.[1-9][0-9][0-9]
+
*.[1-9]R
+
*.[1-9][0-9]R
+
*.[1-9][0-9][0-9]R
+
*.eledsec[1-9]
+
*.eledsec[1-9]R
+
*.eledsec[1-9][0-9]
+
*.eledsec[1-9][0-9]R
+
*.eledsec[1-9][0-9][0-9]
+
*.eledsec[1-9][0-9][0-9]R
+
+
# glossaries
+
*.acn
+
*.acr
+
*.glg
+
*.glo
+
*.gls
+
*.glsdefs
+
*.lzo
+
*.lzs
+
+
# uncomment this for glossaries-extra (will ignore makeindex's style files!)
+
# *.ist
+
+
# gnuplottex
+
*-gnuplottex-*
+
+
# gregoriotex
+
*.gaux
+
*.gtex
+
+
# htlatex
+
*.4ct
+
*.4tc
+
*.idv
+
*.lg
+
*.trc
+
*.xref
+
+
# hyperref
+
*.brf
+
+
# knitr
+
*-concordance.tex
+
# TODO Comment the next line if you want to keep your tikz graphics files
+
# *.tikz
+
*-tikzDictionary
+
+
# listings
+
*.lol
+
+
# luatexja-ruby
+
*.ltjruby
+
+
# makeidx
+
*.idx
+
*.ilg
+
*.ind
+
+
# minitoc
+
*.maf
+
*.mlf
+
*.mlt
+
*.mtc[0-9]*
+
*.slf[0-9]*
+
*.slt[0-9]*
+
*.stc[0-9]*
+
+
# minted
+
_minted*
+
*.pyg
+
+
# morewrites
+
*.mw
+
+
# nomencl
+
*.nlg
+
*.nlo
+
*.nls
+
+
# pax
+
*.pax
+
+
# pdfpcnotes
+
*.pdfpc
+
+
# sagetex
+
*.sagetex.sage
+
*.sagetex.py
+
*.sagetex.scmd
+
+
# scrwfile
+
*.wrt
+
+
# sympy
+
*.sout
+
*.sympy
+
sympy-plots-for-*.tex/
+
+
# pdfcomment
+
*.upa
+
*.upb
+
+
# pythontex
+
*.pytxcode
+
pythontex-files-*/
+
+
# tcolorbox
+
*.listing
+
+
# thmtools
+
*.loe
+
+
# TikZ & PGF
+
*.dpth
+
*.md5
+
*.auxlock
+
+
# todonotes
+
*.tdo
+
+
# vhistory
+
*.hst
+
*.ver
+
+
# easy-todo
+
*.lod
+
+
# xcolor
+
*.xcp
+
+
# xmpincl
+
*.xmpi
+
+
# xindy
+
*.xdy
+
+
# xypic precompiled matrices and outlines
+
*.xyc
+
*.xyd
+
+
# endfloat
+
*.ttt
+
*.fff
+
+
# Latexian
+
TSWLatexianTemp*
+
+
## Editors:
+
# WinEdt
+
*.bak
+
*.sav
+
+
# Texpad
+
.texpadtmp
+
+
# LyX
+
*.lyx~
+
+
# Kile
+
*.backup
+
+
# gummi
+
.*.swp
+
+
# KBibTeX
+
*~[0-9]*
+
+
# TeXnicCenter
+
*.tps
+
+
# auto folder when using emacs and auctex
+
./auto/*
+
*.el
+
+
# expex forward references with \gathertags
+
*-tags.tex
+
+
# standalone packages
+
*.sta
+
+
# Makeindex log files
+
*.lpz
+89
main.tex
···
+
\documentclass[12pt,a4paper]{amsart}
+
\usepackage[tt=false]{libertine}
+
\usepackage{microtype}
+
\usepackage{amsmath,amssymb,amsfonts,mathtools}
+
\usepackage{tikz-cd}
+
\usetikzlibrary{arrows.meta}
+
+
\title{The synthetic Sierpi\'nski cone}
+
\author{Jonathan Sterling}
+
\thanks{This is an extended version of the conference paper, \emph{When is the partial map classifier a Sierpi\'nski cone?} by Pugh and Sterling, which was presented at LICS 2025. Relative to \emph{op.\ cit.}, I present some new results including a strengthening of the Sierpi\'nski completeness theorem to apply to completely untruncated spaces.}
+
+
\NewDocumentCommand\Spx{m}{\Delta^{#1}}
+
\NewDocumentCommand\Ord{m}{\mathbf{#1}}
+
\NewDocumentCommand\One{}{\Ord{1}}
+
\NewDocumentCommand\Zero{}{\Ord{0}}
+
+
\NewDocumentCommand\II{}{\mathbb{I}}
+
\NewDocumentCommand\XX{}{\mathbb{X}}
+
+
\begin{document}
+
\maketitle
+
\tableofcontents
+
+
\tikzcdset{
+
open immersion/.style={
+
-{Triangle[open]}, hook
+
},
+
closed immersion/.style={
+
-{Triangle[fill=black]}, hook
+
}
+
}
+
+
\section{Introduction}
+
+
In both category theory and domain theory, there is a remarkable coincidence involving the Sierpi\'nski object $\II\equiv \{ 0\hookrightarrow 1 \}$. A figure $\II\xrightarrow{\alpha}\mathbb{C}$ represents an arrow $\alpha \colon \alpha(0)\to \alpha(1)$ in $\mathbb{C}$; on the other hand, an arrow $\mathbb{C}\xrightarrow{\chi}\II$ represents an ``open'' subspace of $\mathbb{C}$ given by the preimage of $1\in \II$.
+
+
The two-handedness of $\II$ extends to an identification between the \emph{Sierpi\'nski cone} and the \emph{partial map classifier} of any space $\XX$, which we illuminate below. The Sierpi\'nski cone $\XX_\bot$ of a space $\XX$ is the following co-comma square, which we may compute by means of a pushout:
+
\[
+
\begin{tikzcd}
+
\XX\ar[r,equals]\ar[d] & \XX \ar[d,open immersion,"\iota_\XX"]\\
+
\One\arrow[r,swap,closed immersion,"\bot_\XX"]\ar[ur,phantom,"{\Uparrow}\gamma_\XX"] & \XX\mathrlap{_\bot}
+
\end{tikzcd}
+
\qquad
+
\begin{tikzcd}
+
\XX\ar[r,closed immersion,"{(0,\XX)}"]\ar[d] & \II\times\XX \ar[d,"\gamma_\XX"description] & \XX\ar[l,open immersion,swap,"{(1,\XX)}"]\ar[dl,sloped,swap,open immersion,"\iota_\XX"] \\
+
\One\ar[r,swap,closed immersion,"\bot_\XX"] & \XX\mathrlap{_\bot}\ar[ul,phantom,very near start,"\ulcorner"]
+
\end{tikzcd}
+
\]
+
+
The (open) partial map classifier $\eta\colon \XX\hookrightarrow L(\XX)$ is, on the other hand, the partial product of the open embedding $\{1\}\hookrightarrow \XX$ and classifies spans
+
\[
+
\begin{tikzcd}
+
\XX & U\ar[l]\ar[r,open immersion]& \mathbb{Y}
+
\end{tikzcd}
+
\]
+
where $U$ is an \emph{open} subspace of $\mathbb{Y}$, \emph{i.e.}\ a pullback of $\{1\}\hookrightarrow \II$ in the such that every such span arises in the context of a unique pullback square:
+
\[
+
\begin{tikzcd}
+
U\ar[r]\ar[d,open immersion]\ar[dr,phantom,very near start,"\lrcorner"] & \XX\ar[d,open immersion,"\eta_\XX"]\\
+
\mathbb{Y}\ar[r,densely dashed,swap,"\exists!"] & L(\XX)
+
\end{tikzcd}
+
\]
+
+
Now, it so happens that we may define a comparison map $\sigma_\XX\colon \XX_\bot\to L(\XX)$ using \emph{either} the universal property of the Sierpi\'nski cone or the universal property of the partial map classifier. In the former case, we construct a lax square (left) and in the latter case we observe that $\iota_\XX\colon \XX\hookrightarrow \XX_\bot$ is an open embedding and construct a partial map (right):
+
+
\[
+
\begin{tikzcd}
+
\XX\ar[r,equals]\ar[d] & \XX \ar[d,open immersion,"\eta_\XX"]\\
+
\One\arrow[r,swap,closed immersion,"\bot_\XX"]\ar[ur,phantom,"{\Uparrow}"] & L(X)
+
\\
+
|[gray]|\varnothing \ar[u,gray,open immersion]\ar[ur,gray,phantom,very near start,"\urcorner"] \ar[r,gray,-{Triangle[fill=gray]}, hook] & |[gray]|\XX \ar[u,swap,gray,open immersion,"\eta_\XX"]
+
\end{tikzcd}
+
\qquad
+
\begin{tikzcd}
+
\XX\ar[r,equals]\ar[d,open immersion,swap,"\iota_\XX"]\ar[dr,phantom,very near start,"\lrcorner"] & \XX\ar[d,open immersion,"\eta_\XX"]\\
+
\XX_\bot\ar[r,densely dashed,swap,"\exists!"] & L(\XX)
+
\end{tikzcd}
+
\]
+
+
The promised coincidence is that the induced comparison map $\XX_\bot\to L(\XX)$ is invertible. This property also extends to models of higher categories: when $L(X)$ is the open partial map classifier of a simplicial set,\footnote{We mean, $L(X)$ classifies partial maps whose support is classified by the nerve of the open embedding $\{1\}\hookrightarrow \{0\to 1\}$.} we actually do have $L(X) \cong \Spx{\Zero}\star X \equiv X_\bot$. It is therefore reasonable to say that the correspondence between classifying partial maps and representing mapping cones is part of the core logic--geometry duality shared by (higher) category theory, domain theory, topology, \emph{etc.}
+
+
Surprisingly, the situation changes considerably when passing to synthetic notions of space---as in synthetic domain theory, synthetic topology, and synthetic (higher) category theory.
+
+
+
\subsection{Foundations and preliminaries}
+
+
In what follows, we work in the vernacular of univalent foundations---though, it is worth noting, none of our results depends on univalent universes. Unlike many works of synthetic mathematics, we do not globally assume any axioms aside from function extensionality; instead we locally assume structures satisfying various axioms where needed.
+
+
\end{document}