Characterize constant objects in the internal language of a topos?

Question

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}$?

Answer 1

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".

Answer 2

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};]

2. (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;]

3. 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.