Fibration of contexts beget fibrations of toposes

Published in School of Computer Science, University of Birmingham, 2018

Abstract: We introduce a notion of (op)fibration in the 2-category Con of contexts. We give a new characterization of weak fibrations internal in 2-categories. Using this characterization, we establish that a context extension $\thT_1 \to \thT_0$ with (op)fibration property and a model $M$ of $\thT_0$ in an elementary topos S with natural number object gives rise to an (op)fibration of elementary toposes with codomain $\CS$.

Introduction: For many special constructions of topological spaces (which for us will be point-free, and generalized in the sense of Grothendieck), a structure preserving morphism between the presenting structures gives a map between the corresponding spaces. Two very simple examples are: a function $f \maps X \to Y$ between sets already is a map between the corresponding discrete spaces; and a homomorphism $f\maps K \to L$ between two distributive lattices gives a map in the opposite direction between their spectra. The covariance or contravariance of this correspondence is a fundamental property of the construction. In topos theory we can relativize this process: a presenting structure in an elementary topos $\CE$ will give rise to a bounded geometric morphism $p\maps \CF \to \CE$, where $\CF$ is the topos of sheaves over $\CE$ for the space presented by the structure. Then we commonly find that the covariant or contravariant correspondence mentioned above makes every such $p$ an opfibration or fibration in the 2-category of toposes and geometric morphisms.

If toposes are taken as bounded over some fixed base $\CS$, in the 2-category $\BTopos/S$, then there are often easy proofs got by showing that the generic such p, taken over the classifying topos for the relevant presenting structures, is an (op)fibration. See [SVW13] for some simple examples. In the 2-category $\ETopos$ of arbitrary elementary toposes with nno, the properties are stronger (because there are more 2-cells) and harder to prove – see [Joh02]. In this paper our main result (Theorem 7.2) is to show how to use the arithmetic universe techniques of [Vic17] to get simple proofs in the generic style of the sharper, base-independent (op)fibration results in ETop. Our starting point is the following construction in [Vic17], using the 2-category $\Con$ of AU-sketches in [Vic16]. Suppose $U \maps \thT_1 \to \thT_0$ is an extension map in $\Con$, and $M$ is a model of $\thT_0$ in $\CS$, an elementary topos with nno. Then there is a geometric theory $\thT_1/M$, of models of $\thT_1$ whose $\thT_0$-reduct is $M$, and so we get a classifying topos $p\maps S[\thT_1/M] \to \CS$. We prove that if $U$ is an (op)fibration, then so is $p$ in the sense of [Joh93].

Fibration of contexts beget fibrations of toposes , arXiv:1808.08291
joint with Steve Vickers, submitted to Theory and Application of Categories (TAC)