Characterize constant objects in the internal language of a topos?

A Grothendieck topos $\mathcal{E}$ is equivalent to the category of sheaves on some site $Q$. We say a sheaf $X\colon Q^{\text{op}}\to\mathsf{Set}$ is constant if it is the sheafification of a constant presheaf, i.e. one that factors through the terminal map $Q^{\text{op}}\to \{*\}$.

But what if we forget the site $Q$ and consider $X$ as an object in the topos? Can we characterize the property of $X\in\mathcal{E}$ being constant? More specifically, two questions:

1. Is the property of $X$ being constant dependent on the choice of site $Q$?
2. Is there a way to characterize constant objects in the internal language of $\mathcal{E}$?
• The concept of modality seems appropriate here, given that constant sheaves (in the sense that Mamuka describes) form a coreflective subcategory. You want to express internally that $\Delta\Gamma X\to X$ is an isomorphism. – David Roberts Aug 1 '17 at 16:38
• @DavidRoberts This would only work when $\mathcal E$ is connected. For example if $\mathcal E=\mathsf{Set}\times\mathsf{Set}$, then $\Delta\Gamma(S_1,S_2)=(S_1\times S_2,S_1\times S_2)$, so that the counit is an isomorphism only when both are singletons or both are empty. – მამუკა ჯიბლაძე Aug 1 '17 at 18:10
• Constant sheaves are the same as the colimit of a diagram that maps each object to the final object $1: \mathcal{E}$, since sheaffification commutes with colimits and constant presheaves are of this form. More geometrically, we have a unique geometric morphism $\mathcal E \xrightarrow{p} Set$ and the constant sheaves are object isomorphic to $p^* X$ for $X: Set$. – Anton Fetisov Aug 1 '17 at 18:57
• For one example of what @DavidRoberts mentions, consider the constant objects in simplicial sets considered as a cohesive topos ncatlab.org/nlab/show/cohesive+topos – Bas Spitters Aug 1 '17 at 21:06
• Ah, OK. Just a bare geometric morphism might not be sufficient. But it's a case worth considering. – David Roberts Aug 1 '17 at 21:23

For the first question: no, the notion of "constant object" doesn't depend on the site. The reason is in Anton's comment: every Grothendieck topos comes with a unique geometric morphism $p : \mathcal{E} \leftrightarrows \mathrm{Set}$, and the constant objects are those in the essential image of $p^* : \mathrm{Set} \to \mathcal{E}$. In fact, since every object of $\mathrm{Set}$ is not just a colimit but a coproduct of copies of $1$, the constant objects are even just those that are coproducts in $\mathcal{E}$ of copies of $1$.

However, I don't think there is any way to characterize constant objects purely using the internal language of $\mathcal{E}$. One reason for this is because the notion of constant object does depend on the geometric morphism $p : \mathcal{E} \leftrightarrows \mathrm{Set}$. "Huh?", you say, "didn't you just say that geometric morphism was unique?" Well, yes, so it is... but only once the topos $\mathrm{Set}$ has been fixed! Any bounded geometric morphism $q : \mathcal{E} \leftrightarrows \mathcal{S}$ (even between elementary topoi) allows us to think of $\mathcal{E}$ as a "Grothendieck topos in the world of $\mathcal{S}$", in which case the "constant objects of $\mathcal{E}$ considered in the world of $\mathcal{S}$" are those in the essential image of $q^*$. Clearly different choices of $q$ will give different notions of "constant object". But the (finitary) internal language of $\mathcal{E}$ involves only finitary constructions using the elementary structure of the category $\mathcal{E}$, so it is invariant with respect to a "choice of base $\mathcal{S}$"; thus it can't possibly characterize the constant objects.

Infinitary internal languages, by contrast, do depend on the base topos $\mathcal{S}$ to provide a meaning of "infinitary". There are various choices that one might make regarding what to mean by an "infinitary internal language". The "geometric logic" used to describe classifying toposes is infinitary only in allowing infinite disjunctions, but one might also consider infinite conjunctions or infinite strings of quantifiers. If we allow all of these, then here is an infinitary formula that almost describes the constant objects:

$$\bigvee_{S\in \mathrm{Set}} \exists_{s\in S}\; x_s:X. \left(\left(\forall y:X, \bigvee_{s\in S} y=x_s\right) \wedge \bigwedge_{s, t\in S} (x_s = x_t \to s=t)\right).$$

This is a very infinitary formula: it starts with a disjunction indexed by a proper class! However, Grothendieck toposes are well-powered, so I think one can still make sense of such a formula therein. If you trace through the interpretation of this formula in the natural way, for a fixed set $S$ the infinite quantifier string $\exists_{s\in S} x_s:A$ quantifies over the object $X^{\Delta S}$, where $\Delta S$ denotes the constant sheaf at $S$, and the formula inside this quantifier picks out the subobject of $X^{\Delta S}$ consisting of isomorphisms. Thus this formula is asserting "there exists a set $S$ and an isomorphism $\Delta S\cong X$" --- but because the $\exists$ quantifiers are interpreted by images, the truth of this formula internally doesn't imply that $X$ is constant, only that it is locally constant (i.e. becomes constant upon pullback to some well-supported object).

This is going to be a problem with any internal logic that's based only on proving propositions. We might hope to get around it by using a full internal "infinitary dependent type theory", and replacing the $\exists$ by a $\Sigma$. I don't know exactly what that means, but even if I did, there would now be a problem with the proper-class disjunction $\bigvee_{S\in \mathrm{Set}}$ out front, since well-poweredness only allows us to take proper-class-sized unions of subobjects, whereas now we would no longer have subobjects of anything. Perhaps we could mess around with universes. But overall, it seems that the answer is basically "no".

• This answer, although exhaustively explanatory, raised (for me) a further question: can it happen that $\mathcal E$ is Grothendieck over two essentially different models of set theory? That is, there are two well-pointed toposes with NNO and any other however stringent requirements $\mathcal S_1$ and $\mathcal S_2$ which are incomparable in the sense that no geometric morphisms between them exist in either direction, and, further, Grothendieck toposes $\mathcal E_1\to\mathcal S_1$, $\mathcal E_2\to\mathcal S_2$, such that $\mathcal E_1$ is equivalent to $\mathcal E_2$ as a (abstract) category? – მამუკა ჯიბლაძე Aug 3 '17 at 6:00
• Because if this can happen, then in principle it can also happen that in some $\mathcal E$ there are two different kinds of constant objects... – მამუკა ჯიბლაძე Aug 3 '17 at 6:03
• @მამუკაჯიბლაძე - Trivially, yes: let $\mathcal{E}$ be the terminal category, then it admits a bounded geometric morphism to any other topos. Of course in this case every object is constant. If you formulate the question to eliminate such trivial answers, I think it would be an interesting MO question it its own right; I expect the set-theorists would have something to say about it via what they know about forcing models. – Mike Shulman Aug 3 '17 at 17:55

The answer to your second question is also no: only local properties can be characterised in the internal language of a topos, and it is possible to have locally constant (pre)sheaves that are not constant.

A simple, and well-known, example runs as follows: let $\mathbb C$ be the poset with four elements $n$, $e$, $s$, and $w$, satisfying $w<n$, $w<s$, $e<n$, and $e<s$. Now let $P$ be the presheaf on $C$ which maps: each object to $\{0,1\}$; all but one arrow (say, the one from $w$ to $n$) to the identity; that one other arrow to the non-identity automorphism of $\{0,1\}$. This presheaf is not isomorphic to a coproduct of copies of 1, and therefore not constant. (If you draw it right, $P$ looks like the non-trivial double cover of the circle. In fact, this is not just a metaphor: $\hat{\mathbb C}$ can be construed as the topos of sheaves on a certain non-Hausdorff quotient of the circle.)

Now let $N$ and $S$ denote Yoneda of $n$ and $s$, respectively; then $N+S$ has global support. The slice topos $\hat{\mathbb C}/(N+S)$ is equivalent to $\hat{\mathbb D}$, where $\mathbb D$ is the poset having elements $n,e_N,e_S,s,w_S,w_N$, satisfying $w_N<n$, $w_S<s$, $e_N<n$, and $e_S<s$. Moreover $(S+N)^*:\hat{\mathbb C}\to\hat{\mathbb C}/(N+S)\simeq\hat{\mathbb D}$ maps $P$ to the presheaf (let's call it $Q$) which maps: every element of $\mathbb D$ to $\{0,1\}$; all but one arrow ($w_N \to n$) to the identity; that one arrow to the non-identity automorphism of $\{0,1\}$. Unlike $P$, $Q$ actually is isomorphic to a coproduct of copies of $1$, and therefore constant. (Continuing the parenthetic remark at the end of the previous paragraph: we have trivialised the non-trivial double cover by breaking the circle into two semicircles as usual.)

The larger point here is that $(S+N)^*$, being the inverse image functor of a surjective local homeomorphism, is both logical and faithful; logical functors preserve interpretations of formulas, and faithful ones reflect validity. So if $\Phi$ is a formula which is true for all constant sheaves, its validity for $Q$ entails its validity for $P$. In fact, this applies for infinitary formulae as well, since $(S+N)^*$, having both a left and a right adjoint, preserves arbitrary limits and colimits.

Now one may wonder: can locally constant sheaves be characterised by an internal formula? I think that the answer is yes, but the man to ask is Thomas Streicher. Both he and Richard Squire were (independently) interested in this question in the late '90s and (I think) reached answers in the early '00s. I am relatively sure that Richard did not publish his results, but perhaps Thomas did? This was about the time I was losing interest in topos theory, though I have picked it up again recently.

What I can remember is this:

1. locally constant presheaves are the same as presheaves valued in {sets-with-bijections};

[1.5 decidable presheaves are the same as presheaves valued in {sets-with-injections};]

1. (for presheaves) it is therefore enough to characterise "transition-surjective" presheaves---i.e., presheaves valued in {sets-with-surjections};

[2.5 Kuratowski-finite presheaves are precisely those which are both transition-surjective and finitely-valued;]

1. the problem of characterising transition-surjective presheaves is therefore equivalent to that of characterising finitely-valued presheaves, which is an interesting question in its own right.
• An even simpler example: take the topos T of G-set for G some discrete group. Then $T/G \simeq Set$ so any object of $T$ is locally constant. – Simon Henry Oct 31 '17 at 14:51