Domains and Classifying Topoi

TL;DR

This work advances a unifying synthetic domain theory by grounding its axioms in classifying topoi through a countable quasi-coherence principle, linking the interval object $\mathbb{I}$ to a duality between algebras and spectra. It shows that dominance, Phoa's principle, and the chain-completeness axiom can be derived from quasi-coherence for bounded distributive lattices and $\sigma$-frames, and extends these ideas to countably presented algebras to obtain infinitary domain-theoretic results such as the inductivity of the initial algebra $\omega$ and the chain-complete interval $\mathbb{I}$. The paper develops the partial map classifier $L$, the co-partial map classifier $T$, and a suite of local properties for $\mathbb{I}$, then demonstrates how spectra and affine spaces arise naturally as fixed points of an adjunction, enabling new models for synthetic domain theory based on countably presented sites. These results illuminate deep connections among synthetic domain theory, synthetic topology, and synthetic category theory, and point toward new models and further unifications with existing frameworks like Abstract Stone Duality. The work thereby provides a modular, algebraic toolkit for constructing and reasoning about domain-like structures within classifying topoi, with potential practical impact on synthetic approaches to computation and topology.

Abstract

We explore a new connection between synthetic domain theory and Grothendieck topoi related to the distributive lattice classifier. In particular, all the axioms of synthetic domain theory (including the inductive fixed point object and the chain completeness of the dominance) emanate from a countable version of the synthetic quasi-coherence principle that has emerged as a central feature in the unification of synthetic algebraic geometry, synthetic Stone duality, and synthetic category theory. The duality between quasi-coherent algebras and affine spaces in a topos with a distributive lattice object provides a new set of techniques for reasoning synthetically about domain-like structures, and reveals a broad class of (higher) sheaf models for synthetic domain theory.

Figures (1)

• Figure 1: Summary of axioms considered in this paper. Unlike the usual axiom sets for synthetic domain theory hyland1990first, the goal of these axioms is not to modularly specify all the properties of the interval with minimal overlap but instead to identify a sequence of increasingly strong descriptions of intervals that may play a role in synthetic domain theory.

Theorems & Definitions (172)

• Definition 2.1: Spectrum
• Definition 2.2: Observation algebra
• Proposition 2.3
• proof
• Example 2.5: Cubes
• Proposition 2.6
• Definition 2.7
• Proposition 2.8
• proof
• proof : Proof of \ref{['prop:spectra-are-powers-of-the-interval']}