Discernible Objects in a Topos

Question

Perhaps an overly elementary question: let $\mathcal{E}$ be a topos and let $X, Y$ be non-isomorphic objects in $\mathcal{E}$. Is it always true that there exists a formula $\phi$ of $\mathcal{E}$'s Mitchell-Benabou language with one free variable which is true of one but not both of $X$ and $Y$ (on the Kripke-Joyal semantics)? If so, what about when $X$ and $Y$ are isomorphic?

Answer 1

Summary: The answer may depends on the choice of a precise interpretation of the question, which is too vague. But for all the interpretations I can think of the Kripke-Joyal semantics do not distinguishes between objects that are "locally isomorphic".

Conversely objects that satisfies the exact same formulas are locally isomorphic simply because the existence of a local isomorphism can be expressed in the Mitchell-Bénabou language. So what you can distinguishes is exactly the equivalence class of object up to the "locally isomorphic" equivalence relation.

---

Let's start with some observations:

• The Mitchell-Bénabou language of a large topos has a proper class formula. For example for any object $X$ of the topos, "$\exists x \in X$" is a formula in the language of the topos, so there is no set theoretic obstruction for formula to distinguish all objects of a large topos.

• The question as asked do not quite make sense. Variables of of formula in the Mitchell-Bénabou language are not object of the topos, and object of the topos cannot be substitued to these variables. Objects of the topos corresponds to the type of the language. Examples of formula of the language are things like:

$$ \forall x,y \in X, (x= y) \quad\text{ (holds if and only if $X$ is subterminal)}$$ $$ \forall y \in Y, \exists x \in X, f(x)=y \quad \text{ (holds if and only if $f$ is an epimorphism)}$$ $$ \forall x,y \in Y, f(x)=f(y) \Rightarrow x = y \quad \text{ (holds if and only if $f$ is monomorphism)}$$

where $X$ and $Y$ are fixed object of the topos and $f: X \rightarrow Y$ a morphism. As you can see, I can try to substitute $X$ by another object in the first formula and it somehow makes sense, but if I try to do it in the other two, "f(x)" no longer means anything. So it is not quite clear how you want to define this in general.

I'll propose a precise meaning of the question below, and answer this precise version of the question. If this is not the meaning you intented, then try to make your question more precise.

In the meantime, here are a few general remarks one can make that should be true for any interpretation of the question and that already almost answers it:

1. The Kripke-Joyal semantics is invariant under isomorphisms. Meaning that if I replace every objects appearing in the topos by an isomorphic one, and translate appropriately all the terms and functions in the formula using these isomorphisms this do not modifiy the validity of the formula. Hence isomorphic objects should be not be discernable by any formula whatever that means.
2. The Kripke-Joyal semantics only see "local" properties. I.e. if $\Phi$ is some formula in the language of $\mathcal{T}$. And if $p:Y \twoheadrightarrow 1 $ is a cover of the terminal object of $\mathcal{T}$, then the formula $\Phi$ is valid in the Kripke-Joyal semantics in $\mathcal{T}$, if and only if $p^* \Phi$ is valid in the Kripke-Joyal semantics in $\mathcal{T}_{/Y}$. This suggest that objects that are "locally isomorphic" should satisfies the same formulas as well, though we are already in the area where one needs to make the question precise as it is not clear what it means that they "satisfies the same formulas", but I can't think of a way to make sense of the question that will be able to distinguish locally isomorphic objects. Of course there are plenty of example of objects of a topos that are locally isomorphic without being isomorphic: any locally trivial structure on a space (like a vector bundle) is locally isomorphic to a trivial one, in the topos of $G$-sets, any $G$-set $X$ is locally isomorphic to $X$ endowed with the trivial $G$-action. The interpretation of the question I will give below will have this property, and it will distinguishes exactly objects that are not locally isomorphic.

---

Here is my proposed interpretation. The goal is to make sense of formulas where one can substitute an abstract type symbol $\mathbb{O}$ by an arbitrary object $X$ of $\mathcal{T}$. For this, I consider the "Free topos $\mathcal{T} \{ \mathbb{O}\}$ over $\mathcal{T}$". Here I am not talking of the object classier of $\mathcal{T}$, but freeness is in the sense of logical morphisms (so that the Mitchell-Bénabou language will be preserved). More precisely I want $\mathcal{T} \{ \mathbb{O}\}$ to have the following universal property: For any other elementary topos $\mathcal{E}$, a logical morphism $\mathcal{T} \{ \mathbb{O}\} \rightarrow \mathcal{E}$ is given by, a logical morphism $\mathcal{T} \rightarrow \mathcal{E}$ together with the choice if an object $X \in \mathcal{E}$ (the image of $\mathbb{O}$).

The existence of $\mathcal{T} \{ \mathbb{O}\}$ is clear if $\mathcal{T}$ is small (because 'elementary topos' is a quasi-algebrique theory). If your topos is not small... justs take a larger universe.

I'm interpreting a formula in "one free object parameters" as a formula in the Mitchell-Bénabou language of $\mathcal{T} \{ \mathbb{O}\}$.

Given $\Phi$ such a formula, and $X$ an object of $\mathcal{T}$, I have a unique logical morphism $ev_X: \mathcal{T} \{ \mathbb{O}\} \rightarrow \mathcal{T}$, I'm calling $\Phi(X)$ the image of the formula $\Phi$ by this logical morphism $ev_X$.

The two observation above applies immediately to this interpreation:

1. If $X \simeq X'$ then I have a natural isomorphism $ev_X \simeq ev_{X'}$ and the validity of the formula $\Phi(X)$ and $\Phi(X')$ will be equivalent.
2. Let $X$ and $Y$ be two objects that are locally isomorphic, i.e. become isomorphic in some étale cover $\mathcal{T}_{/Z} \rightarrow \mathcal{T}$ (for $Z \twoheadrightarrow 1$ a cover). It means that their image by the logical morphism $\mathcal{T} \rightarrow \mathcal{T}_{/Z}$ are isomorphic. It means that the two composites $$ \mathcal{T}\{\mathbb{O}\} \rightrightarrows \mathcal{T} \rightarrow \mathcal{T}_{/Z} $$

are isomorphic, hence the validity of the image of $\Phi$ by these is equivalent. As the second morphism is conservatif (and preserves interpretation of formula), the validity of $\Phi(X)$ in the Kripke-Joyal semantics in $\mathcal{T}$ is equivalent to the validty of $\Phi(Y)$.

So one cannot distinguish between locally isomorphic objects.

Now, given any fixed object $Y \in \mathcal{T}$ consider the following formula the Mitchell-Bénabou Language of $\mathcal{T}\{\mathbb{O}\}$ :

$$\Phi_Y = \exists f: Y \rightarrow \mathbb{O}, \exists g: \mathbb{O} \rightarrow Y,( \forall x : \mathbb{O}, f(g(x)) =x \text{ and } \forall y : Y, g(f(y))=y) $$

Then $\Phi_Y (X)$ is exaclty the formula " there exists an isomorphism between $X$ and $Y$", which holds in the Kripke-Joyal semantics if and only if $X$ and $Y$ are locally isomorphic. Hence if $X$ and $Y$ satisifes the same formula, one has that $X$ satisfies $\Phi_Y(X)$ and hence $X$ and $Y$ are locally isomorphic.

An alternative to make sense of it would be to consider the extention of Mitchell-Bénabou language and the Kripke-Joyal Sémantics introduced by M.Shulman which allows to have object as variable and quantifying on them. I believe it provides a larger class of formula than what I've done here, but it has the same properties of only seeing local properties, so the final answer will be the same.