# Pullback-stability of internally projective objects

An object $X$ of a category $C$ is said to be projective if the hom-functor $C(X,-)$ preserves epimorphisms (or, in general, some restricted class of epimorphisms such as the regular or effective ones). The axiom of choice is equivalent to the assertion that all objects of Set are projective. In general, a "projective set" $X$ is one such that we can make $X$-indexed families of choices.

In section D4.5 of Sketches of an Elephant, an object $X$ of a topos $C$ is said to be internally projective if the right adjoint $\Pi_X : C/X \to C$ preserves epimorphisms, and $C$ is said to satisfy the internal axiom of choice if all objects are internally projective. The latter definition is found in many other places; I haven't seen the former elsewhere, but I don't know its actual origin.

My question is, if $X$ is internally projective in this sense in $C$, is $X\times Y$ internally projective in $C/Y$ for another object $Y$? This seems to be a necessary condition for the definition to be sufficiently "internal", but I haven't been able to prove it yet.

A similar question is, if $C$ satisfies the internal axiom of choice, does the functor $\Pi_f : C/X \to C/Y$ preserve epimorphisms for any morphism $f:X\to Y$?

-
Your 'similar question' looks very much like a hypothetical definition for internal projectivity of a map, and something that algebraic geometers might have studied. – David Roberts Aug 20 '13 at 6:56
It's exactly internal projectivity of $f$ as an object of $C/Y$, so the question is equivalent to: if $C$ satisfies the internal axiom of choice, does every slice category also do so? – Mike Shulman Aug 20 '13 at 20:57
If I recall correctly MacLane and Moerdijk define "$X$ is internally projective" as "${-}^X$ preserves epis", so that is like a non-dependent version of your definition. Does that make a difference? Probably not in a topos. – Andrej Bauer Aug 20 '13 at 21:18
Mike - I know :-) I read your post at the nForum. @AndrejBauer - I'm guessing Mike doesn't just want to assume $C$ is a topos, since his stack semantics paper deals in the ambient setting of a pretopos. – David Roberts Aug 20 '13 at 22:06
The reason I would expect an "internal" statement to be preserved by slicing is that if you extend the Kripke-Joyal semantics for internal logic to quantifiers over all objects (arXiv:1004.3802), or embed the topos in a category of sheaves or ideals as in algebraic set theory, then the resulting interpretation of any statement will be stable under pullback/slicing, just like ordinary statements in the internal logic. So a statement which is not so stable cannot be expresed "internally" in such a way. – Mike Shulman Aug 23 '13 at 15:09

For toposes, the stability property of your first question does hold. Suppose $X$ is internally projective in $\mathbb{C}$. And suppose $q: B \to A$ is an epimorphism from $v : B \to I$ to $u: A \to I$ in $\mathbb{C}/I$, hence an epimorphism in $\mathbb{C}$. Write $X^*$ for the object $X \times I$ of $\mathbb{C}/I$. The exponential $u^{X^*}$ in $\mathbb{C}/I$ has underlying object: $$\{(i,f) : I \times A^X \mid \forall x:X.\, u(f(x))=i\}$$ And the map $q^{X^*}$ is a pullback in $\mathbb{C}$ of the map $$I \times q^X: I \times B^X \to I \times A^X$$ along the embedding of $u^{X^*}$ in $I \times A^X$. Since the displayed map above is an epi by internal projectivity of $X$, so is its pullback $q^{X^*}$.
It is also true that the internal axiom of choice (IAC) is preserved by slicing. (I haven't managed to see that this follows as a direct consequence of the previous.) Suppose IAC holds in a topos $\mathbb{C}$. Consider an arbitrary object $w: Z \to I$ in $\mathbb{C}/I$, and an epimorphism $q$ as above. The exponential $u^w$ in $\mathbb{C}/I$ has underlying object $$\{(i,f): I \times (1+A)^Z \mid \forall z:Z.\, (w(z)= i \to \exists a:A. f(z) = \text{inr}(a) \wedge u(a) = i) \wedge (w(z) \neq i \to f(z) = \text{inl}(*)) \}$$ This uses a standard representation of slice-category exponentials in toposes in terms of partial map classifiers, with the simplification that, since $\mathbb{C}$ is boolean (using Diaconescu's theorem that IAC implies boolean), the partial map classifier for $A$ is $1 + A$. Similar to the previous argument, one now observes that $q^w$ is a pullback in $\mathbb{C}$ of the map $$I \times (1+q)^Z : I \times (1+B)^Z \to I \times (1+A)^Z$$ along the subobject inclusion of $u^w$. And once again the map displayed above is an epi, by internal projectivity of $Z$.
Very nice, thank you! Does the second argument actually depend on Booleanness? It seems that it ought to work just as well with $1+A$ replaced by whatever the partial map classifier happens to be. If so, then it would imply that $w:Z\to I$ is internally projective in $\mathbb{C}/I$ whenever $Z$ is internally projective in $\mathbb{C}$. – Mike Shulman Aug 24 '13 at 3:12