jonmsterling.com
+581
Martinfest/main.typ
+581
Martinfest/main.typ
···+So you put on your pith helmet and come in with your big and loud machines and terraform the mathematical world. It is a good day’s work.+Everything is very “civilised”: the sticky saps dry up, the buzzing insects zip away, and the last scurrying critters scatter to their holes.+Finally, all resistance muzzled, we can…show that the spectrum of a ring is a topological space.+But the thing about those little critters and buzzing bees and the sap that gets between your toes is—these entities were already an ecosystem with its own topology, geometry, arithmetic, computation—all intertwined together.+I wish to be as quiet as I possibly can, so I may hear the chirping, #pause chittering, #pause barking, #pause and buzzing #pause of the little creatures of little mathematics who,\ #pause+I would like to share with you some things I have learned recently about partial map classifiers and their generalisations.+Some of this I learned from my collaborations with my students Leoni Pugh and Lingyuan Ye respectively.+A $Sigma$-algebra is a bounded distributive lattice equipped with a homomorphism from $Sigma$, _i.e._ an object of $ALG :equiv Sigma arrow.b #DL$.+Each lattice $Sigma$ determines an “intrinsic” or “synthetic” topology, \ notions of open and closed subspace, partial map, _etc_.+Similar to _synthetic (domain theory, topology, algebraic geometry, _etc._)_ \ and _Abstract Stone Duality_ (Taylor), but we do not assume axioms\ globally: our language is HoTT/UF.+Delta^n &= Spec Sigma[sans(x)_1,...,sans(x)_n] #math.class("relation", sym.slash) sans(x)_i >= sans(x)_(i+1)+Some important shapes are _not_ spectrums, _e.g._ the generic inner horn $Horn$ obtained by glueing the interval onto itself end-to-end.+The interval $II$ is both a space (the spectrum of $Sigma[sans(x)]$) and the underlying \ set of the algebra $Sigma$.++ For any element $alpha in A^II$ we have $alpha(i) = alpha(0) or floor.l i floor.r and alpha(1)$.+Phoa's principle from _synthetic domain theory_ states $Sigma$ itself satisfies the property above. Implications for synthetic higher categories too.++ $Sigma$ is _dominant_ when it is conservative and the subuniverse $[-]colon Sigma arrow.r.hook PROP$ is closed under internal sums.+*NB*: if every quotient of $Sigma$ by finitely many equations is quasi-coherent, then both $Sigma$ and $Sigma^(op)$ are dominant (S. & Ye; _cf._ Cherubini _et al._).+Let $X$ be a space. An _observation_ of $X$ is an element of the observational algebra $Obs(X)$, _i.e._ a function $phi colon X -> II$.+We shall refer to an arrow of the form $U arrow.r.hook X$ arising from some observation as an _open embedding_. A _cloven open embedding_ is defined \ to be an open embedding equipped with an observation whence it arises.+By duality, a _closed embedding_ is an embedding $K arrow.r.hook X$ arising from an observation $phi in CoObs(X)$ in the *dual lattice context*. In terms of $Sigma$, this\ is a pullback of the inclusion ${0} arrow.r.hook II$.+A _cloven_ open partial map from $X$ to $Y$ is a partial map equipped with a _cleaving_ for its constituent open embedding:+The _partial product_ of the generic open embedding ${1} arrow.r.hook II$ with a\ space $Y$ classifies cloven open partial maps into $Y$. Defining+Every cloven open partial map from $X$ to $Y$ arises from a _unique_ function $X -> Lift(Y)$ in the following way:+Y edge("d", "hook->") & U edge("d", "hook->") edge("l", ->) edge("r", ->) & {1} edge("d", "hook->")\+Lift(Y) & X edge("l", "-->", label: exists!, label-side: #left) edge("r", ->, label-side: #right) & II+X edge("d", "hook->") & bold(0) edge("d", "hook->") edge("l", "hook->", label: !_X) edge("r", ->) & {1} edge("d", "hook->")\+Lift(X) & bold(1) edge("l", "hook-->", label: "und"_X, label-side: #left) edge("r", ->, label-side: #right, label: "0") & II+In ordinary domain/category/topos theory, the open partial map classifier $Lift(X)$ is _also_ the *Sierpiński cone* $X_bot$, which freely adds a bottom point.+X edge("d", ->) edge("r", ->, label: 1_X) & X edge("d", "hook->", label: iota_X, label-side: #left)\+X edge("d", ->) edge("r", "hook->", label: (0,X)) & II times X edge("d", "hook->", label: gamma_X, label-side: #center) & edge("l", "hook->", (1,X)) X edge("dl", "hook->", label: iota_X, label-angle: #auto, label-side: #left)\+*NB*: $bot$ is _closed_ in $X_bot$, and $iota_X$ is an _open embedding_ as soon as $Sigma$ is strict.+X edge("d", "hook->") edge("r", ->, label: (0, X)) & II times X edge("d", "hook->", label-side: #left, label: "glue"_X)\+If induced comparison map $X_bot -> Lift(X)$ is an equivalence for _generic_ $X$, then naturally each $[i]_bot -> Lift [i]$ is an equivalence. But+and so for any $j <= i$ we may conclude either $j=0$ or $i=1$. Considering $j :equiv i$ we therefore have $i=0 or i=1$, which makes all spaces codiscrete. When $II$ is strict, this makes the boundary inclusion $bold(2) arrow.r.hook II$ an equivalence.+In domains/categories/toposes, $X_bot -> Lift(X)$ is an equivalence for _global_ $X$, not for _generic_ $X$. We could use a $flat$-modality or switch to the Mitchell--Bénabou language to safely assert it only for global things.+But I am more interested in powering down the engines so that we can _hear_ what the spaces are telling us in their own terms.++ It is not fair to compare $X_bot$ with $Lift(X)$ without fixing a universe of discourse, which (in synthetic mathematics) means an _accessible reflective subuniverse_ in which to compute the pushout $X_bot$.++ “All” the comparison maps $X_bot -> Lift(X)$ is far too large a left class to generate a reflective subuniverse, but *this localisation is nonetheless accessible and reflective*, and the presentation is _extremely_ small.++ For free we get a _limit-style_ computation of _mapping cylinders_ (Artin glueings) without higher inductive types.+_*Definition.*_ A type $X$ is called _$[0]$-connected_ when either of the following equivalent conditions hold:+_*Remark.*_ When $Sigma$ is conservative, the above is a slight _strengthening_ of the Segal condition for synthetic $(infinity,1)$-categories.+Last year I proved a restricted version for $0$-truncated $C$. Last month, I proved it unconditionally in Martin-Löf’s intensional type theory with function extensionality, for an arbitrary bounded partial order $Sigma$.+Many geometrical constructions expressed globally are actually _sums_ of simpler structures that can only be written down in type theory.+Here, open/closed refers not to the topology induced by $Sigma$ but rather to the partitioning of the ambient higher topos $cal(E)$ into open/closed subtoposes. Nonetheless, there is a startling connection.+The partial map classifier with respect to $Sigma$ is the _sum_ of all the open modalities $opmod([i])$, as we have $Lift(X) equiv mysum(i,II) opmod([i]) X$. Conversely, letting $ isf(-) colon II -> PROP $ be the indicator function for $0 in II$,+we will see that the Sierpiński cone is the sum of all the _closed modalities_ $clmod(isf(i))$, _i.e._+A beautiful symmetry emerging from the failure of De Morgan’s laws in constructive mathematics, which I learned from Reid Barton.+#only("2-")[Then we apply the left adjoint $mysum(i,II) colon TYPE_(slash (i:II)) -> TYPE$, which preserves colimits.] #only("3-")[Then we simplify.]+E edge("d", ->, label: f) edge("r", ->, label: 1_E) & E edge("d", "hook->", label: iota_f, label-side: #left)\+E edge("d", ->) edge("r", "hook->", label: (0,E)) & II times E edge("d", "hook->", label: gamma_f, label-side: #center) & edge("l", "hook->", (1,E)) E edge("dl", "hook->", label: iota_f, label-angle: #auto, label-side: #left)\+*NB*: $B arrow.r.hook MCyl(f)$ is a closed embedding; when $f colon E -> B$ is a $[0]$-connected map, then $iota_f colon E arrow.r.hook MCyl(f)$ is an open embedding.+The open mapping cylinder $MCyl(f)$ turns out to be the sum of all the Sierpiński cones of the _fibres_ of $f$. #only("2-")[We compute generically in $x:B$.] #only("3-")[Then we apply the left adjoint $mysum(x,B) colon TYPE_(slash (x:B)) -> TYPE$.] #only("4-")[Simplify with Frobenius,] #only("5-")[ and straightening/unstraightening.]+mysum(x,B) fib(f,x) edge("d", ->) edge("r", "hook->") & mysum(x,B) II times fib(f,x) edge("d", ->) \+mysum(x,B) fib(f,x) edge("d", ->) edge("r", "hook->") & II times mysum(x,B) fib(f,x) edge("d", ->) \+From a type theoretic point of view, the function $f colon E -> B$ could be viewed instead as a family $x:B tack.r E[-] : TYPE$, whose open mapping cylinder we can define more directly.+All this suggests a “logical” or limit-style counterpart to the open mapping cylinder, using the partial map classifier:\+Let $x:B tack.r E[x]$ be a family of $[0]$-connected types. Then we have an evident universal comparison map $MCylFam_((x:B)) E[x] -> LiftFam_((x:B)) E[x]$.+_*Corollary.*_ Let $C$ be Sierpínski complete. Then for any family $x:B tack.r E[x]$ of $[0]$-connected types, $C$ is orthogonal to this comparison map, _i.e._+Several years ago, I asked whether the Artin glueing of a geometric morphism classifies models of an interesting theory.+Our results imply an answer to the analogous question for *synthetic topology*: in suitable reflective subuniverses, mapping cylinders may be computed as sums of partial map classifiers. The subtlety is to ensure the reflective subuniverse is closed under mapping cylinders of _suitable_#footnote[Take care: the appropriate condition on the family is _not_ fiberwise: we need the _fibration_ $mysum(b,B)E[x] -> B$ and the base $B$ to be local.] families.+All these notions and results can be dualised to _closed embeddings_ by considering the dual lattice $Sigma^"op"$. We have Hyland's co-partial map classifier $CoLift(X)$ and the inverted Sierpiński cone $X^top$, and the closed mapping cylinders $ClMCyl(f)$.