Liberating synthetic quasi-coherence from forcing

A little topos theory at the Topos Institute

Abstract

In this blog post, I’ll reformulate Ingo Blechschmidt’s “synthetic quasi-coherence” axiom — or more precisely his “general nullstellensatz” — as a lifting property inspired by Ivan Di Liberti’s work on coherent toposes and ultrastructures. This lifting property shows that synthetic quasi-coherence can be derived from a sort of “directed path induction” for toposes, suggesting the possibility of an internal logic for all toposes in which the axioms for any sort of synthetic mathematics would compute. (Based on joint work with Mitchell Riley)

1 The joy of synthetic mathematics

Since Bourbaki’s first lectures at the Café Grill-Room A. Capoulade in 1934, one could be forgiven for holding the belief that all mathematical activity consists of ever more elaborate arrangements of sets within sets within sets. We begin with the natural numbers, the ability to form pairs, and the ability to comprehend subsets carved out by properties, and before you know it we are describing rigid analytic spaces and ultracategories and twisted lax double functors — all just increasingly complex arrangements of sets. No matter what we can imagine, Bourbaki assures us, we can express in Cantor’s paradise.¹

A complex arrangement of sets satisfying certain properties and assumptions is known in logic as a theory. There is a theory of groups, a theory of rings, a theory of ultracategories and twisted lax double functors. A model of a theory is an actual arrangement of sets actually satisfying those properties and assumptions. The integers \mathbb{Z} with their addition + : \mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}² are a model of the theory of groups; with their multiplication as well they become a model of the theory of rings. The traditional view is that any mathematical concept, no matter how invovled, can modelled by some arrangement of sets expressed by a theory (in some or other logic).

But in 1963, Lawvere ate from the apple of knowledge in Cantor’s paradise and produced his thesis on the functorial semantics of algebraic theories. Lawvere identified an algebraic theory \mathbb{T} with a category \mathcal{L}(\mathbb{T}) built from the terms of the theory, and identified models M \models \mathbb{T} of \mathbb{T} with a product-preserving functors M : \mathcal{L}(\mathbb{T}) \to \mathsf{Set} into the category of sets. So far, not so different. But Lawvere’s reformulation opens up a whole new world for logic: now we can define a model of \mathbb{T} in any category \mathcal{C} with finite products as a product-preserving functor \mathcal{L}(\mathbb{T}) \to \mathcal{C}. For example, if \mathbb{T} is the theory of groups, then its models in in the category of sets are the groups as usual, but its models in the category of smooth manifolds are the Lie groups and in the category of algebraic varieties are the algebraic groups, and so on. With this extra freedom, we can work in any category we like, so long as it has finite products.³ Even more, there is always a universal choice of model: the identity functor \mathsf{id} : \mathcal{L}(\mathbb{T}) \to \mathcal{L}(\mathbb{T}) is a model of \mathbb{T} with absolutely no accidental assumptions creeping in. This is the universal model of the theory \mathbb{T}.

Soon, Lawvere observed that just as universal algebra could be interpreted in any category with finite products, all of set theory could be interpreted in any of Grothendieck’s categories of set-valued sheaves: toposes. Toposes of sheaves support not only a notion of natural number and finite products, but also power-sets and a comprehension axiom. In fact, toposes interpret all of Martin-Löf’s (roughly contemporaneously developed) dependent type theory with a univalent universe of propositions.

This means that any sort of theory we could interpret in the category of sets, we could just as well interpret in a category of sheaves — in toposes. We gain a powerful freedom in this ability to work “internally” to any topos, because toposes can have wonderful properties which are not true of the category of sets. For example, there are toposes where every real valued function is continuous⁴, or computable, or even smooth⁵. Because of this, you can use ordinary set theoretic arguments to construct whatever complicated functions you want, and they will be continuous/computable/measurable/regular/…, without you even having to check. That is, so as long as you judiciously avoid the law of excluded middle and the axiom of choice, which do not hold in all toposes. The logic of toposes is constructive.

The fact that you can just interpret set theoretical arguments into any topos has all sorts of nice and powerful consequences; for example, the category of abelian groups in any topos is an abelian category (because the proof of this for sets doesn’t use the law of excluded middle or the axiom of choice), a fact which has been highlighted by Clausen and Scholze in their re-foundations of analysis as a reason to work in a topos rather than with topological spaces. Even better, structures and properties on sheaves which may be difficult to describe from an ordinary external point of view can become familiar notions when seen from the internal point of view:

• A sheaf of rings is just a ring, internally.
• A sheaf of modules over a sheaf of rings is just a module over that ring, internally.
• A sheaf of modules is of finite type just when it is a finitely generated module, internally, and so on…⁶

We can then prove things about sheaves of finite type over some scheme by translating statements about finitely generated modules internal to the topos of sheaves on that scheme. We can also define sheaves internally in very conceptual ways. For example, projective n-space may be defined internally as the set of lines through the origin in affine space of dimension n+1; this is the usual definition which works over, say, the complex numbers, but taken internally it works over any base scheme.

By axiomatizing the special features of a topos we would like to work in, we can then work in what feels like ordinary set theory and carry out arguments which are more conceptually transparent than the corresponding external arguments would be. This is called synthetic mathematics, and there is now a flourishing garden of synthetic approaches to various mathematical topics:⁷

• First, there was Lawvere’s synthetic differential geometry, which takes a smooth real line \mathbb{R}_s as axiomatic and supposes the Kock-Lawvere axioms, including that: “every function f : \{\varepsilon : \mathbb{R}_s \mid \varepsilon^2 = 0 \} \to \mathbb{R}_s of a first order infinitesimal real number is linear: f(\varepsilon) = a + b\varepsilon for unique a and b”. Synthetic differential geometry is a wonderful little field; I did my PhD in it.⁸
• In his thesis, Ingo Blechschmidt laid out the beginnings of synthetic algebraic geometry, and it has since been taken up by a group at Gothenburg/Chalmers.
• Martin Hyland began a study into synthetic domain theory, which has continued to flourish at Cambridge (as in, for example, this recent paper by Sterling and Ye).
• In his work on homotopy type theory, Voevodsky (as well Warren and Awodey) identified the correct internal logic of higher toposes (of sheaves of homotopy types) which opened up the possibility for synthetic homotopy theory.
• In his Axiomatic Cohesion, Lawvere identified some modalities on a topos which characterize it as a topos of spaces; Schreiber interpreted these in higher toposes; and Shulman described a type theory for them, opening the way for synthetic algebraic topology.⁹
• Synthetic topology emerged out of synthetic domain theory through Taylor’s work on abstract stone duality and Escardó’s work on the topology of types; it has also been taken up by the Chalmers group.
• Riehl and Shulman put forward a simplicial type theory for working in (higher) toposes of simplicial sheaves. Weinberger et. al. have used this type theory to study synthetic higher category theory.
• Alex Simpson has begun working on a synthetic probability theory, which has strong relations to convenient categories for higher order probability theory.

It is a bit difficult to describe how pleasant it is to work synthetically without running through a single example in full; but this introduction has really gone on long enough. If you’re interested, I recommend checking out John Bell’s A primer of infinitesimal analysis for an elementary introduction to synthetic differential geometry and Ingo Blechschmidt’s wonderful PhD thesis for a comprehensive introduction on the uses of synthetic reasoning in algebraic geometry.

2 Which axioms should we take?

A work in synthetic mathematics begins by laying out some axioms which hold in the topos we intend to work in. However, it hasn’t always been clear exactly which axioms we need in order to prove the things we want to prove. For example, while the first axiom of synthetic differential geometry presented above is sufficient for some basic facts about derivatives, in order to argue well about higher order derivatives it needs to be extended to higher order infinitesimals. Even with a pretty comprehensive list of axioms (such as those at the beginning of Bunge et. al.’s Synthetic differential topology), we often run into cases that require more axioms.¹⁰ It’s not tenable to constantly fiddle with foundations in the course of a proof.¹¹

The main axioms generally fall in the following three sorts:

• (Duality): There is a duality between “affine schemes” and “finitely presented algebras”. In the algebraic setting, this is what Ingo Blechschmidt called synthetic quasi-coherence in his thesis. But it also includes the Kock-Lawvere axiom, which asks for a duality between Weil algebras and “infinitesimal varieties”¹², and Phoa’s principle as emphasized in Sterling and Ye’s recent paper (see Section 7). It also appears as Axiom 10 in this paper on synthetic higher category theory.
• (Local choice): Any surjection into an “affine scheme” admits sections on an “open cover”. This was isolated by Cherubini-Coquand-Hutzler in the algebraic setting as Zariski local choice, but it also includes the Bunge-Dubuc Covering Property from synthetic differential geometry, as well as the projectivity of the simplices which Mitchell Riley and I assume of our simplicial cohesion in order to give a synthetic proof of the nerve theorem.
• (Tinyness): Some objects are tiny: the functor (T \to (-)) has¹³ a right adjoint. This appears in synthetic differential geometry with the assumption that the infinitesimal varieties are tiny, which allows for the definition of differential form classifiers. Mark Williams has used presentability of (tiny) representables to show that dualities present for presheaves descend to sheaves.

But this scheme is more of a suggestion than a formula. What we need is a systematic approach to choosing axioms for synthetic mathematics.

3 Blechschmidt’s generalized nullstellensatz

In an unpublished but widely circulating note, “qcoh”, Ingo Blechschmidt has put forward a general axiom scheme which should work for any topos. I’ll work towards describing his idea here (using my own notation, for those following along in qcoh). From this point on, this blog post will assume that you know a fair bit of topos theory.

Lawvere’s functorial semantics for algebraic theories in cartesian categories and finite-product-preserving functors may be extended to a functorial semantics for positive, infinitary first-order theories (“geometric” theories) in toposes and “geometric morphisms” between them. A “geometric” theory is a theory in first-order logic which allows for equality, finite conjunctions, and infinite disjunctions (i.e. disjunctions indexed by an arbitrary set). For any such theory \mathbb{T}, there is a classifying topos \mathsf{Set}[\mathbb{T}] so that models of \mathbb{T} in any topos \mathcal{E} correspond to geometric morphisms \mathcal{E} \to \mathsf{Set}[\mathbb{T}]. The identity morphism therefore corresponds to a model U_{\mathbb{T}} of \mathbb{T} in \mathsf{Set}[\mathbb{T}], and this is the universal model of \mathbb{T}.

Furthermore, every topos of sheaves is the classifying topos for some theory; namely, if \mathcal{E} = \mathsf{Sh}(C, j) is the topos of sheaves on some site, then \mathcal{E} classifies “flat, j-continuous functors” out of C by Diaconescue’s theorem. Therefore, no matter what topos we intend to work internal to, we should at least start by assuming that we have a model U_{\mathbb{T}} of a theory \mathbb{T} it classifies. For example:

• If we want to do synthetic algebraic geometry in the big Zariski topos, we may first appeal to the fact that the big Zariski topos classifies the theory of local rings¹⁴ with the affine line \mathbb{A} being the universal local ring itself. We may then begin our axiomatization by asking for a local ring \mathbb{A}.
• If we want to work with simplicial sets, we may appeal to the fact that the topos of simplicial sets classifies total orders with distinct top and bottom elements, with the 1-simplex \Delta[1] being the universal model (and with \Delta[2] \hookrightarrow \Delta[1]\times \Delta[1] the order relation). We may then begin our axiomatization by asking for a total order with distinct top and bottom elements.

However, satisfying this assumption only guarantees that we are working in some topos equipped with a geometric morphism to the topos we intended to work in; we need something else to guarantee that this geometric morphism is the identity. Now, inverse images of geometric morphisms preserve the interpretations of all positive formulas (because they preserve finite limits and infinite colimits, and these suffice to interpret any positive formula), so that any positive formula which is true of the universal model is true of all models in all toposes; conversely, every positive formula which is true of the universal model is positively provable (see, e.g. Theorem 2.4 of this paper. Therefore, whatever extra axioms we need to take, they can’t be positive. The special features of the universal model are negative.¹⁵

Some of these negative properties have been known for a long time. For example, Kock remarked in 197? that the affine line in the big Zariski topos (the universal local ring) is in fact a field: every non-zero element has an inverse. This is a negative property because it is an implication with an implication in the antecedent:

(0 = x) \Rightarrow \bot \,\vdash\, \exists y. xy = 1.

In his thesis, Bechschmidt extended the Kock-Lawvere axiom to his synthetic quasi-coherence axiom and observes that it suffices to prove all known negative properties about the affine line, including that it is a field. But Blechschmidt doesn’t stop there. In qcoh, he isolates a general axiom scheme which suffices to prove every special property of the universal model U_{\mathbb{T}} of a geometric theory \mathbb{T}. He calls this his general nullstellensatz, though I believe it should be called quasi-coherent definability.

The idea is simple and obviously wrong: what if every proposition concerning the universal model were positively definable, and every true proposition provable? Any true proposition about the universal model — even the weird negative ones — would follow from this axiom scheme and the assumption that U_{\mathbb{T}} was a model of \mathbb{T}.

Of course, this axiom scheme can’t hold. Blechschmidt’s genius in qcoh is to find a restricted version of it which does. Suppose \mathbb{T} is a positive theory (in \mathsf{Set}); we can then pull it back to get a positive theory \gamma^{\ast}\mathbb{T} in the classifying topos \mathsf{Set}[\mathbb{T}]. We can then form a new theory, the slice theory U_{\mathbb{T}} \downarrow \gamma^{\ast}\mathbb{T} in \mathsf{Set}[\mathbb{T}] by adding in constant terms c(e) for every e : U_\mathbb{T} (of the correct sorts, when \mathbb{T} is multi-sorted). This is the theory of \mathbb{T}-homorphisms out of U_{\mathbb{T}}; its classifying topos \mathsf{Set}[\mathbb{T}][U_{\mathbb{T}} \downarrow \gamma^{\ast} \mathbb{T}] is, externally, the morphism d : \mathsf{Set}[\mathsf{Hom}_{\mathbb{T}}] \to \mathsf{Set}[\mathbb{T}] from the classifying topos for \mathbb{T}-homomorphisms to the classifying topos of \mathbb{T} which classifies the domain of the universal homomorphism.

This is a special sort of \mathsf{Set}[\mathbb{T}]-theory, since it only ever uses \mathsf{Set}-indexed disjunctions.¹⁶ Blechschmidt calls these “geometric* theories”, but I will call them quasi-coherent theories on account of the following analogy: a theory is coherent when it only uses finitary disjunctions, and a sheaf of modules is coherent when it is locally of finite presentation¹⁷; a sheaf is quasi-coherent when it is locally of \mathsf{Set}-indexed presentation; so, a theory is quasi-coherent when it only uses \mathsf{Set}-indexed disjunctions.¹⁸

Blechschmidt’s updated axiom scheme (see Theorem 5.2 of qcoh) is then that (in the internal logic of \mathsf{Set}[\mathbb{T}]):

1. For every context \Gamma of U_{\mathbb{T}} \downarrow \mathbb{T}, and any suboject P \subseteq \mathsf{id}_{U_{\mathbb{T}}}(\Gamma) of the interpretation of that context at the identity morphism \mathsf{id} : U_{\mathbb{T}} \to U_{\mathbb{T}} (which is a model of the slice theory U_{\mathbb{T}} \downarrow \gamma^{\ast}\mathbb{T}), there is a quasi-coherent formula \Gamma \vdash \varphi in the slice theory whose interpretation at the identity is P: every subset of the universal model is quasi-coherently definable in the slice theory.

2. Let \Gamma \vdash \varphi be a quasi-coherent formula in the slice theory. Then its interpretation \mathsf{id}_{U_{\mathbb{T}}}(\varphi) \subseteq \mathsf{id}_{U_{\mathbb{T}}}(\Gamma) at the identity of U_{\mathbb{T}} holds (that is, \mathsf{id}_{U_{\mathbb{T}}}(\varphi) = \mathsf{id}_{U_{\mathbb{T}}}(\Gamma)) if and only if \varphi is provable in the slice theory.

These two axioms suffice to show that the sheaf of quasi-coherent formulas in context \Gamma in the slice theory, modulo provable equivalence, is isomorphic to the sheaf of subsheaves of the interpretation of \Gamma at the identity of U_{\mathbb{T}}. This really is a universal axiom scheme (Theorem 1.2 of ibid.) for first-order statements about the universal model: if \varphi is a first-order formula, then we can interpret it as a subobject of the universal model; it is therefore quasi-coherently definable by the axiom scheme, and is true if and only if it is provable.

Blechschmidt uses a delicate forcing argument to prove that this axiom scheme holds for any theory \mathbb{T}. The aim of this blog post is to liberate quasi-coherent definability from these sorts of forcing arguments.

4 Dreaming of homotopy types

The difficulty with forcing argument is that they are highly reliant on syntax. This is not so awful when we’re trying to prove theorems about 1-toposes where syntax means first order logic (though, it’s a little awful). But it becomes haltingly difficult when we want to reason about higher toposes, where syntax means “homotopy type theory” and general coherence issues must be taken into account.

Let’s start by sketching a generalization of Blechschmidt’s scheme from logic to types. The main idea of propositions as types is that propositions are the (-1)-truncated types of mathematical objects. Accordingly, we have the following analogy:

Level	Syntax	Semantics
-1	Formula	Proposition
-1	Proof	Truth
\infty	Definition	Type
\infty	Term	Element

I am using “definition” and “term”¹⁹ here for the syntactic analogue of “type” and “element”, taking the role of “formula” and “proof” in relation to “proposition” and “truth”. We might say then that the quasi-coherent definability axiom scheme, in a highly conjectural setting, is that for any positive homotopy type theory \mathbb{T} internal to the \infty-topos of homotopy types \mathsf{Ho} (“positive” in the sense of involving only \mathsf{Ho}-indexed higher inductive types (which include the unit, \Sigma, =, and all \mathsf{Ho}-indexed colimits), and no negative types like functions or universes),

1. For any context \Gamma of U_{\mathbb{T}} \downarrow \gamma^{\ast}\mathbb{T} and any type family X : \mathsf{id}_{U_{\mathbb{T}}}(\Gamma) \to \mathsf{Type}, there is a quasi-coherent definition \Gamma \vdash C in the slice theory which interprets to X.

2. For any element x : \mathsf{id}_{U_{\mathbb{T}}}(\Gamma) \vdash f(x) : \mathsf{id}_{U_{\mathbb{T}}}(C), there is a quasi-coherent term \Gamma \vdash t : C which interprets to f.

Now, a definition should be quasi-coherent if it only uses \mathsf{Ho}-indexed higher inductive types, and not \mathsf{Ho}[\mathbb{T}]-indexed higher inductive types.

Mitchell Riley and I have been chatting for years about quasi-coherent definability. Mitchell observed that it really looks like some sort of path induction principle (itself a form of the Yoneda lemma): To do something for a general map (model of the slice theory), it suffices to do it at the identity. Mitchell and I call this conjectural induction principle quasi-coherent induction, and we’ve been dreaming about a type theory which would interpret into all toposes and for which the axiom scheme would become a rule. More about this later in the blog post.

For now, the scaffolding to work syntactically with internal homotopy type theories doesn’t quite exist (though Uemura-Nguyen \infty-type theories might help). For that reason, let me turn to semantics.

5 Liberating synthetic quasi-coherence from syntax

In this section, I want to liberate quasi-coherent definability from syntax. In fact, I will show that it follows from a delightfully simple lifting property first observed by Ivan Di Liberti in his enlightening exegesis of coherent toposes and ultrastructures. This lifting property will also make it clear that we really are dealing with a form of directed path induction for toposes.

The lifting property we will need appears as Theorem 1.3.1 of Di Liberti’s paper on coherent toposes. It is so clean that I will prove it here in its entirety; this will also make it clear that it should hold just as well for \infty-toposes.²⁰

We work over an arbitary base topos \mathcal{B}, which I will just call the topos of “base types”. In the world of higher toposes, Martini and Wolf have been working out a theory of internal higher toposes. I do not want to fuss with any details (including actually subtle size issues, and careful internalization) in this blog post, so please regard all the rest as conjectural.

Let \kappa be a \Sigma-closed sub-universe of a \mathcal{B} — a “regular cardinal”.

Definition 1 A \mathcal{B}-topos \mathcal{X} is \kappa-presentable if it admits a free, \kappa-ary presentation: a geometric embedding j : \mathcal{X} \hookrightarrow \mathcal{B}[C] into a topos of presheaves on a(\mathcal{B}-)category C with finite limits with j_{\ast} \kappa-accessible: j_{\ast} preserves \kappa-filtered colimits. That is, \mathcal{X} is \kappa-presentable if it admits a presentation as sheaves on a category with finite limits, and \kappa-filtered colimits of sheaves, computed in presheaves, are still sheaves.

Definition 2 A map i : \mathcal{E} \to \mathcal{F} of \mathcal{B}-toposes is \kappa-flat when i_{\ast} preserves \kappa-indexed colimits.

We now prove Di Liberti’s theorem:

Theorem 1 (Di Liberti). Let i : \mathcal{E} \to \mathcal{F} be \kappa-flat. Then every \kappa-presentable topos \mathcal{X} is weakly right Kan injective against i; if i is an embedding, then \mathcal{X} is right Kan injective against i:

• For any x : \mathcal{E} \to \mathcal{X}, there exists a geometric morphism r_x : \mathcal{F} \to \mathcal{X} and an 2-cell \varphi : r_x i \Rightarrow x exhibiting r_x as the right Kan extension of x along i.

• If i is an embedding, then \varphi is an isomorphism.

Proof. Consider a \kappa-ary presentation j : \mathcal{X} \hookrightarrow \mathcal{B}[C]. Consider \hat{x} : \mathcal{F} \to \mathcal{B}[C] determined by the lex functor C \xrightarrow{y} \mathcal{B}[C] \xrightarrow{j^{\ast}} \mathcal{X} \xrightarrow{x^{\ast}} \mathcal{E} \xrightarrow{i_{\ast}} \mathcal{F}. That is, \hat{x}^{\ast} = \mathsf{lan}_{y}(i_{\ast}x^{\ast}j^{\ast}y), and \hat{x}_{\ast} = \mathsf{lan}_{\hat{x}^{\ast}}(1) is its right adjoint. It remains to show that \hat{x} descends to sheaves, or that \hat{x}_{\ast} = j_{\ast}j^{\ast}\hat{x}_{\ast}. For this, we need to compute \hat{x}_{\ast} with some Kan-fu:

\begin{aligned} \hat{x}_{\ast} &= \mathsf{lan}_{\hat{x}^{\ast}}(1) \\ &= \mathsf{lan}_{\hat{x}^{\ast}}(\mathsf{lan}_y y) \\ &= \mathsf{lan}_{\hat{x}^{\ast}y}(y) \\ &= \mathsf{lan}_{\mathsf{lan}_{y}(i_{\ast}x^{\ast}j^{\ast}y)y}(y) \\ &= \mathsf{lan}_{i_{\ast}x^{\ast}j^{\ast}y}(y)\\ &= \mathsf{lan}_{i_{\ast}x^{\ast}j^{\ast}}(\mathsf{lan}_y y) \\ &= \mathsf{lan}_{i_{\ast}}(j_{\ast}x_{\ast}) \end{aligned}

Therefore, \begin{aligned} j_{\ast}j^{\ast}\hat{x}_{\ast} &= j_{\ast}j^{\ast} \mathsf{lan}_{i_{\ast}}(j_{\ast}x_{\ast}) \\ &= j_{\ast}\mathsf{lan}_{i_{\ast}}(j^{\ast} j_{\ast}x_{\ast}) \\ &= j_{\ast}\mathsf{lan}_{i_{\ast}}(x_{\ast}) \\ (!) &= \mathsf{lan}_{i_{\ast}}(j_{\ast}x_{\ast}) \\ &= \hat{x}_{\ast} \end{aligned} This only one of these steps which isn’t abstract nonsense is the one marked by (!). This follows because j_{\ast} preserves \kappa-filtered colimits, and the Kan extension on the right can be expressed as the colimit \mathsf{lan}_{i_{\ast}}(x_{\ast}) = \mathsf{colim}(i_{\ast} \downarrow \mathcal{F} \to \mathcal{E} \xrightarrow{j_{\ast}x_{\ast}} \mathcal{B}[C]) Since i_{\ast} preserves \kappa-ary colimits, the slice category i_{\ast} \downarrow \mathcal{F} is \kappa-filtered, and so this colimit is preserved by j_{\ast}. This shows that \hat{x} : \mathcal{F} \to \mathcal{B}[C] actually lands in sheaves, giving us r_x : \mathcal{F} \to \mathcal{X}; it is straightforward then to check that this is indeed a right Kan extension of geometric morphisms with comparison 2-cell coming from the computation of the direct image as a left Kan extension. Finally, if i is an embedding, then i_{\ast} is fully faithful and therefore the comparison 2-cell of (r_x)_{\ast} = \mathsf{lan}_{i_{\ast}}(j_{\ast}x_{\ast}) is an isomorphism.

Now, let’s free our minds from various internalization anxieties such as the fact that regular cardinals aren’t stable under inverse image and define a quasi-coherent topos.

Definition 3 Let \mathcal{E} be a \mathcal{B}-topos. An \mathcal{E}-topos \mathcal{X} is quasi-coherent when it is \kappa-presentable over \mathcal{E} for a \mathcal{B}-cardinal \kappa. For emphasis, this means that j : \mathcal{X} \hookrightarrow \mathcal{E}[C] for C an \mathcal{E}-category with finite limits where j_{\ast} preserves \kappa-filtered colimits for some \kappa \in \mathcal{B}.²¹

Definition 4 A map f : \mathcal{X} \to \mathcal{Y} between quasi-coherent \mathcal{E}-toposes is quasi-coherent when f_{\ast} is \kappa-accessible (commutes with \kappa-filtered colimits) for \kappa a \mathcal{B}-cardinal.

We might say that a quasi-coherent \mathcal{E}-topos is \mathcal{E}-locally of constant presentation. Note that if \mathcal{B} = \mathcal{E}, then the definition trivializes: every \mathcal{B}-topos is \mathcal{B}-quasi-coherent, because any \mathcal{B}-filtered \mathcal{B}-category has a terminal object and so \mathcal{B}-filtered colimits are just given by evaluation at that terminal object.

Now for any \mathcal{B}-topos \mathcal{E}, we can form the arrow topos \mathcal{E}^{\pitchfork} (the arrow object in the 2-category of \mathcal{B}-toposes). When \mathcal{E} = \mathcal{B}[\mathbb{T}] classifies models of \mathbb{T}, then \mathcal{E}^{\pitchfork} = \mathcal{B}[\mathsf{Hom}_{\mathbb{T}}] is the classifier for \mathbb{T}-homomorphisms. Over \mathcal{B}, we have an adjoint triple d \dashv i \dashv c : \mathcal{E}^{\pitchfork} \to \mathcal{E} where d classifies the domain of the universal \mathbb{T}-homomorphism, c the codomain, and i : \mathcal{E} \to \mathcal{E}^{\pitchfork} the identity of the universal model of \mathbb{T}. This in particular means that d_{\ast} = i^{\ast} and i_{\ast} = c^{\ast} over \mathcal{B}.²²

However, we want to conclude a statement in \mathcal{E}’s internal logic, so we will need to consider \mathcal{E}^{\pitchfork} as a \mathcal{E}-topos. I will always consider \mathcal{E}^{\pitchfork} as a \mathcal{E}-topos via d, and \mathcal{E} as a \mathcal{E}^{\pitchfork}-topos via i. Note that \mathcal{E} can view itself as an \mathcal{E}^{\pitchfork} topos, since di = \mathsf{id}_{\mathcal{E}}: i is an \mathcal{E}-point of \mathcal{E}^{\pitchfork}.

On the other hand, c : \mathcal{E}^{\pitchfork} \to \mathcal{E} doesn’t exist over \mathcal{E} or \mathcal{E}^{\pitchfork}. But it still leaves a trace. All that remains of c, from \mathcal{E}^{\pitchfork}’s point of view, are the following two facts:

1. i_{\ast} preserves \mathcal{B}-indexed colimits (because it has a right adjoint c_{\ast} over \mathcal{B}).

2. i_{\ast} takes values in \beta-presentable objects of \mathcal{E}^{\pitchfork} for some \mathcal{B}-cardinal \beta (because i_{\ast} \dashv c_{\ast} over \mathcal{B}, and c_{\ast} is a right adjoint between \mathcal{B}-presentable categories and so is \mathcal{B}-accessible).²³

We are now ready to prove quasi-coherent induction.

Theorem 2 (Quasi-coherent induction). Let \mathcal{E} be any \mathcal{B}-topos. For any quasi-coherent \mathcal{E}^{\pitchfork}-topos \mathcal{X}, there is an \mathcal{E}^{\pitchfork}-equivalence between (the \mathcal{E}^{\pitchfork}-category of) maps x : \mathcal{E} \to \mathcal{X} and quasi-coherent maps r : \mathcal{E}^{\pitchfork} \to \mathcal{X} given by r \mapsto ri and x \mapsto \mathsf{ran}_i x.

Proof. Since i_{\ast} has a right adjoint c_{\ast} over \mathcal{B}, it preserves all \mathcal{B}-colimits, and since di = \mathsf{id}_{\mathcal{E}}, it is an embedding. Therefore, Di Liberti’s theorem (over the base \mathcal{E}^{\pitchfork}) shows that maps x : \mathcal{E} \to \mathcal{X} form a coreflective subcategory of maps r : \mathcal{E}^{\pitchfork} \to \mathcal{X} via right Kan extension.

It therefore suffices to show that \mathsf{ran}_i x is quasi-coherent for all x. We know that (\mathsf{ran}_i x)_{\ast} = \mathsf{lan}_{i_\ast}(j_{\ast}x_{\ast}). Now, \mathsf{lan}_{i_\ast}(j_{\ast}x_{\ast}) preserves all colimits preserved by \mathcal{E}^{\pitchfork}(i_{\ast} X, -) for all X \in \mathcal{E}, and this includes all \beta-filtered colimits for some \mathcal{B}-cardinal \beta because i_{\ast} takes value in the \kappa-presentable objects of \mathcal{E}^{\pitchfork}.

Let’s now deduce quasi-coherent definability from quasi-coherent induction.

Corollary (Quasi-coherent definability). For any \mathcal{B}-theory \mathbb{T}, let \mathcal{E} := \mathcal{B}[\mathbb{T}]. Then it is true internally to \mathcal{E} that

1. Every object of \mathcal{E} is quasi-coherently presentable (i.e. definable) in the slice theory U_{\mathbb{T}} \downarrow \gamma^{\ast}\mathbb{T}.

2. Every element of every object is quasi-coherently definable in the slice theory U_{\mathbb{T}} \downarrow \gamma^{\ast}\mathbb{T}.

Proof. (Sketch). We will take for granted that quasi-coherence is stable under base change.²⁴ Therefore, d^{\ast} \mathcal{E}[\mathbb{O}] is a quasi-coherent \mathcal{E}^{\pitchfork}-topos, and we may take this for \mathcal{X} in the theorem above. Maps x : \mathcal{E} \to d^{\ast} \mathcal{E}[\mathbb{O}] over \mathcal{E}^{\pitchfork} are equivalent to maps \pi_{\mathcal{E}[\mathbb{O}]}x : \mathcal{E} \to \mathcal{E}[\mathbb{O}] over \mathcal{E} since di = \mathsf{id}_{\mathcal{E}}; these are \mathcal{E}-objects of \mathcal{E}. On the other hand, maps r : \mathcal{E}^{\pitchfork} \to d^{\ast}\mathcal{E}[\mathbb{O}] correspond to maps \mathcal{E}^{\pitchfork} \to \mathcal{E}[\mathbb{O}] over \mathcal{E}; these are \mathcal{E}-objects of \mathcal{E}^{\pitchfork}. Quasi-coherent induction says that \mathsf{ran}_{i} gives an equivalence between \mathcal{E}-objects of \mathcal{E} and quasi-coherent \mathcal{E}-objects of \mathcal{E}^{\pitchfork}.

Let \beta \in \mathcal{B} be such that \mathsf{ran}_i x is \beta-presentable in \mathcal{E}^{\pitchfork} for any x \in \mathcal{E}. By an analogue of the results in D.3.3 of the Elephant, such an object \mathsf{ran}_i x is representable in the \beta-coherent site of presentation of \mathcal{E}^{\pitchfork} over \mathcal{E}; this is the \beta-coherent syntactic category of the slice theory U_{\mathbb{T}} \downarrow \gamma^{\ast}\mathbb{T}, showing that \mathsf{ran}_i x is \beta-coherently definable.

To deduce the second claim, run the argument again but taking \mathcal{X} = d^{\ast}\mathcal{E}[\mathbb{O}_{\bullet}] to be the classifier for pointed objects.

6 The internal logic of all toposes

Quasi-coherent induction resembles path induction in that both express a lifting property of some class of display maps against the inclusion of constants into a sort of path object:

As in cubical approaches to homotopy type theory, \mathcal{E}^{\pitchfork} is a space of functions from an interval object: specfically, the Sierpinski topos which classifies \mathcal{B}-propositions.

If we had a type theory where contexts were interepreted as toposes (and not just objects of a fixed topos), then we could potentially express quasi-coherent induction as an induction principle. If we could also express all the ordinary type theory constructions in a particular topos (considered as the toposes etale over that particular one), then we could have a type theory where synthetic quasi-coherence was provable and not an axiom, for any sort of synthetic mathematics what-so-ever. Mitchell and I have been calling such a potential type theory “theory type theory” or “[\mathbb{T}]\mathsf{TT}”.

Such a type theory would have a number of benefits for synthetic mathematics. First, of course, is that synthetic quasi-coherence should become provable, rather than an axiom. But also, the ability to jump between toposes in the middle of an argument promises a resolution to one of the curious problems of homotopy type theory: despite the fact that all types are now implicitly homotopy types, much of homotopical mathematics (“brave new algebra”) becomes impossibly difficult because combinatorial methods become infeasibly littered with coherence conditions. With a type theory that interprets into all toposes, we could just jump into the topos of simplicial objects of our current topos whenever we wanted to make a simplicial (or categorical) argument.²⁵ I want to give a very rough sketch of what such a type theory could look like.

Here at the Topos Institute, we are interested in declarative modelling: first, the modeller schematizes their models, defining the theory what it means to be a model (this is also known as metamodelling). Then they develop models within that schema. And then they analyze those models computationally. By making the model description explicit, it becomes clear how we could change the model when analysis conflicts with our data or intentions; by making the theory explicit, we extend this fleetness of thought to a change in modelling paradigms.

Declarative modelling underlies the modelling approach of the Algebraic Julia project, where one first schematizes using a generalized algebraic theory (GAT), potentially including base-type valued attributes. Generalized algebraic theories correspond to the lex fragment of positive logic whose classifying toposes are the cofree toposes \mathsf{Set}[C] of presheaves on a finitely complete category C.²⁶

This approach to declarative modelling also underlies the design of CatColab, where a theory is a cartesian double theory and a model within that theory is expressed as a notebook in a structure editor (left below) and analyzed using general computations (right below):

At a very high level, then, the modelling task consists of defining a (positive) theory for models, presenting a model within that theory (via positive definitions), and then analyzing that model using general computation (using the negative notions of streams and functions). I have a lot more to say about this point of view, especially concerning the development of models and the ecology of models (to take a term from Nate Osgood), but I think I’ll save this for another blog post.

Our own Owen Lynch has come up with a 2-level type theory, “Element Model Type Theory (EMTT)” for defining lex theories and their models, named after its four basic judgements. The theory has a simple presentation in the natural model style which I will now include:

Definition 5 A natural model presentation element model type theory consists of:

1. A representable transformation u_{\bullet} : \mathsf{Em} \to \mathsf{Ty} expressing the judgement \Gamma \vdash a : A that a is an element of the type A. We suppose that this type theory supports a unit type, record (\Sigma-)types, and identity types.

2. A representable transformation u_{\circ} : \mathsf{Mod} \to \mathsf{Thy} expressing the judgement \Gamma \vdash M \vDash \mathbb{T} that M is a model of a theory \mathbb{T}. We suppose this type theory supports a unit type and record types.

3. For any type A, we have a theory \mathbb{E}\mathsf{l}(A) of elements of A, expressed as a pullback square:

4. We have \Pi-types for theories indexed by types: that is, theories \forall x : A.\, \mathbb{T}(x) whose models are given by A-indexed families of models of the theories \mathbb{T}(x).

5. Finally, as Owen likes to say, “the first rule of element model type theory is \mathsf{type}\, \mathsf{theory}”: we have a theory \mathbb{T}\mathsf{ype} of types.

This type theory is highly reminiscent of the multi-level type theories in András Kovács’ extraordinary thesis, which goes much further in the exploration of type theories for theories and their models.

Toposes over \mathsf{Set} are a model of EMTT, as presented above. We take the theories over a topos \mathcal{E} to be the bounded geometric morphisms \gamma : \mathcal{X} \to \mathcal{E} and we take the types over a topos \mathcal{E} to be the etale morphisms \mathcal{E} \downarrow A \to \mathcal{E}. The existence of \Pi-theories over types comes from the exponentiability of etale maps, proved in B4.3.1 of the Elephant.

We could then add to the above rules all higher inductive types to u_{\bullet}, since these are all stable under inverse image of geometric morphisms (they are positive). Indeed, such higher inductive types eliminate into all toposes, since colimits of etale maps are etale. To get negative types, and to express quasi-coherence, we need to keep track of the difference between a general extension and an etale extension. Etale maps preserve both positive and negative types; they are logical. Indeed, in higher topos theory, preserving functions and universes characterizes the etale maps (see Proposition 5.10 of ibid.).

Rather than add negative types in one-by-one, we can add in a single negative type former that suffices to construct all of them (I contend): model universes \mathcal{M}\mathsf{od}(\mathbb{T}). If \mathbb{T} is a theory, them \mathcal{M}\mathsf{od}(\mathbb{T}) is the type of models of that theory. Geometrically speaking, this is the (core of the) category of points of the classifying topos of \mathbb{T}. This certainly suffices to give us universes and functions:

• The type \mathcal{M}\mathsf{od}(\mathbb{T}\mathsf{ype}) of models of the theory of types is a type universe.

• Given a dependent type x : A \vdash B(x) \,\mathsf{type}, the type \mathcal{M}\mathsf{od}(\forall x : A.\, \mathbb{E}\mathsf{l}(B(x))) of models of the theory of elements of B(x) indexed by x : A is a type of functions (x : A) \to B(x).

The difficulty is that \mathcal{M}\mathsf{od} is only stable under etale substitution. It is not clear to me how to handle this syntactically in a 2-level type theory. However, in the natural model style, it should be described by a pullback as follows:

where the natural models have been restricted to the category of contexts and etale substitutions.²⁷

Actually expressing the quasi-coherent induction rule in such a setting is difficult for a number of reasons; not the least of which being that defining quasi-coherent is difficult. The notion of quasi-coherence is a bit like “crispness” in Shulman’s cohesive type theory; it means that a theory extension doesn’t use types defined from that theory.

For example, the theory (X \vDash \mathbb{T}\mathsf{ype}), (x : \mathbb{E}\mathsf{l}(X)) is quasi-coherent in the empty context, but the theory \mathbb{E}\mathsf{l}(X) is not quasi-coherent in the context of X \vDash \mathbb{T}\mathsf{ype}. This examples shows that a naive inductive approach to defining quasi-coherence will have to be modified. For this reason, Mitchell and I have also been playing around with a much more involved type theory that includes judgements for definition and term; but nothing has firmed up yet.

The second difficulty concerns the slice theories (and Hom-theories). In principle, these should be observable from the structure of the theory itself. If this is the case, it may be better to understand quasi-coherent induction not as an induction principle, but rather as a fibrancy condition on quasi-coherent theory extensions which enables certain transports.

I’ll leave the elaboration of these ideas to the future. My goal in this blog post is only really to express the possibility of a type theory for all toposes which is complete for all negative properties of all universal models.

Footnotes

1. This introduction is a bit of historical fiction meant to dramatize this blog post and should not be taken too literally. Those interested in the history of categorical logic should check out this article for a more sober retelling.

2. Remember that a function f : A \to B is, in the Bourbakiste style, a subset G_f \subseteq A \times B of the set of pairs satisfying a property.

3. Sure, these other categories have objects which may be described as arrangements of sets themselves, but there’s a big difference between “G is a group (in the category of manifolds)” and “G is a Lie group (in the category of sets)”: these two statements involve two different theories. Thinking of Lie groups as “just” groups, but in another category, lets us work with the comparatively simple theory of groups when we need to, and with the special features of smooth manifolds when we need to, without always having to face the full combined structure. It also makes possible analogies to other structures which may be obscured if we have to think of them only in terms of their set-valued models. For example, it’s a cute (but deep) theorem that a group in the category of groups is an abelian group; we would never notice this by looking at the theory of abelian groups (with set-valued models) alone.

4. For an introduction to one of the many toposes where this is the case, check out this excellent series on Johnstone’s topological topos

5. This case differs a bit from the other two, but we’ll come back to it.

6. I’m not impressing any algebraic geometers here, but I do recommend looking at Blechschmidt’s thesis for more in depth and useful examples. The above examples are specifically from this MathStackExchange answer by Ingo Blechschmidt. I also recommend looking at his excellent talk on the subject.

7. I’m only mentioning a few key instigators for each subject; please see the links for more!

8. These are my papers in synthetic differential geometry.

9. I also wrote a paper in synthetic algebraic topology, giving a notion of fibration adapted to the synthetic setting.

10. This happened to me while writing my paper on orbifolds in SDG; I took Bunge’s axioms, but required another “covering axiom” from an earlier work of her’s and Dubuc’s in order to prove what I needed about compact sets. I didn’t see it coming at the time, though the extra axiom turned out to be a special case of local choice.

11. Though it may be desirable. And possible! At least, in a singular “meta-foundation”. More on that below.

12. See, e.g., Section 4.2 of my paper on orbifolds.

13. Really, this adjoint only appears externally, or internally with a “Frobenius formula”. See Mitchell Riley’s tiny type theory for more.

14. See, e.g. Mac Lane & Moerdijk, Sheaves in Geometry and Logic, §VIII.6..

15. I will remark that this polarity distinction between positive (finite limits and colimits) and negative (limits, functions, (sub)object classifiers) phenomena is something that only makes sense in a first order context.

16. We’ll come back to this in a bit, but there is a major difficulty in internalizing the notion of “only using \mathsf{Set}-indexed disjunctions” to \mathsf{Set}[\mathbb{T}], since “being a \mathsf{Set}” is not a pullback stable notion. Rather, we could use locally constantly indexed disjunctions, which is the internalization of the notion of “being a \mathsf{Set}”, and is more directly comparable to quasi-coherence for sheaves.

17. Over a locally Noetherian scheme…

18. This analogy is somewhat stained by the fact that a coherent sheaf of modules is not just locally of finite presentation over a general base scheme. This difference between “coherence” and “finite presentation” become more severe in higher category theory, where these notions fail to coincide even for bare homotopy types (where the former are the \pi-finite homotopy types (having finite homotopy groups, and only finitely many of them), and the latter are the retracts of finite cell complexes). In this blog post, I will always fall on the side of presentation. In general, we will see quasi-coherence as “locally of constant presentation”; it therefore generalizes finite presentation and quasi-coherence, but not coherence.

19. I would have preferred to use the term construction over definition here. However, “constructible” firmly lies in the coherent (and not quasi-coherent) side of the generalizations from 1-categories to \infty-categories, and I imagine it would cause confusion if I named the principle “quasi-coherent constructibility”. I could also have gone with “presentation”, since the principle also has to do with the \mathsf{Ho}-presentability of \mathcal{E}-toposes.

20. Ivan and I had a pleasant chat over dinner at CT2023 (where he had presented that paper) during which I told him about this quasi-coherent induction idea; he said he expected to see the story told at the next CT. I have certainly kept him wanting. I hope this blog post, prepared in advance of CT2025, suffices for the time being.

21. More precisely, we should say that an \mathcal{E}-topos \mathcal{X} is \gamma-quasi-coherent for \gamma : \mathcal{E} \to \mathcal{B} the global sections maps when \mathcal{X} is \mathcal{E}-\gamma^{\ast}\kappa-presentable for \kappa \in \mathcal{B}.

22. I want to thank Mathieu Anel for a delightful walk in the woods while I was a student at Johns Hopkins where we discussed the importance of the arrow topos for synthetic quasi-coherence.

23. This claim contains an internalization subtlety which needs careful resolution.

24. A major difficulty in turning this conjectural account into a rigorous proof is the fact that regular cardinals (\Sigma-closed subuniverses) do not quite pull back. I’m sure this difficulty is surmountable, but it is a thorn in my toe.

25. It is worth wondering whether \mathcal{E}^{\Delta^{\mathsf{op}}} classifies total orders with distinct top and bottom elements over \mathcal{E} without assuming a classical meta-theory. The enveloping topos arguments of Mathieu Anel makes use of the generation of all simplicial objects as colimits of monomorphisms, which strikes me as the sort of reasoning that led to the adoption of cubical methods over simplicial methods in constructive approaches to homotopy type theory.

26. Roughly speaking, GATs with attributes correspond to the (infinitary) lextensive fragment which allows for the internalization \Delta B of base types B \in \mathsf{Set} as \Delta B := \coprod_{b \in B} \top; attributes valued in the base type B \in \mathsf{Set} correspond to terms \Gamma \,\vdash t : \Delta B.

27. …and I’m ignoring obvious size issues.