Does "cheap nonstandard analysis" take place in a topos?

Terence Tao's A cheap version of nonstandard analysis describes a way to do analysis halfway between ordinary analysis and nonstandard analysis which, if I'm not mistaken, cashes out to working in the following category $C$ instead of $\text{Set}$. To construct $C$, start with the category $\text{Set}^{\mathbb{N}}$. An object of this category is a sequence $X_i$ of sets indexed by the natural numbers. Say that two sequences $x_i, x_i' \in X_i$ of elements in the sets $X_i$ are eventually equal, written $x \sim x'$, if $x_n = x_n'$ for sufficiently large $n$. The objects of the category $C$ are the same as those in $\text{Set}^{\mathbb{N}}$, but the morphisms are equivalence classes of functions $f_i : X_i \to Y_i$ such that if $x \sim x'$ then $f(x) \sim f(x')$ in the sense that $f_n(x_n) = f_n(x_n')$ for sufficiently large $n$. The equivalence relation on functions is also eventual equality.

Question: Is $C$ a topos?

What I really want to know is if the above construction is a special case of a more general construction that's known to output topoi.

Solution 1:

Let $\mathcal{S} = \mathbf{Set}^{\mathbb{N}}$. Notice that the Heyting algebra of subobjects of $1$ in $\mathcal{S}$ is isomorphic to the powerset $\mathscr{P}(\mathbb{N})$, so the Fréchet filter $\Phi$ of all cofinite subsets of $\mathbb{N}$ can also be considered as a filter of subobjects of $1$ in $\mathcal{S}$.

I will now describe the filter-quotient construction for a generic elementary topos $\mathcal{S}$ and filter $\Phi$ of subobjects of $1$ in $\mathcal{S}$. Given any subobject $U \rightarrowtail 1$, we can consider the category $\mathcal{S}_U$ whose objects are those of $\mathcal{S}$ but whose morphisms $X \to Y$ are morphisms $X \times U \to Y$ in $\mathcal{S}$. (This is the Kleisli category of the comonad ${-} \times U$.) Note that $\mathcal{S}_U$ is equivalent to the slice category $\mathcal{S}_{/ U}$ and hence is an elementary topos. (This is where we use the assumption that $U$ is subterminal.)

We can make the assignment $U \mapsto \mathcal{S}_U$ into a strict functor $\mathrm{Sub}(1)^\mathrm{op} \to \mathbf{Cat}$: given $U \le V$, the induced functor $\mathcal{S}_V \to \mathcal{S}_U$ is the identity on objects and is defined on morphisms by pulling back along $U \hookrightarrow V$. These functors $\mathcal{S}_V \to \mathcal{S}_U$ are logical functors, i.e. preserve finite limits and power objects. Restricting the diagram to $\Phi$, we can form the filtered colimit $\mathcal{S}_{\Phi} = {\varinjlim}_{\Phi^\mathrm{op}} \mathcal{S}_{\bullet}$ in $\mathbf{Cat}$. The theorem is that $\mathcal{S}_{\Phi}$ is an elementary topos, and the cocone components $\mathcal{S}_U \to \mathcal{S}_{\Phi}$ are all logical.

So what does this mean in your example? Well, given a subset $U \subseteq \mathbb{N}$, the topos $\mathcal{S}_U$ is equivalent to $\mathbf{Set}^U$, and for $U \subseteq V$, the induced functor $\mathcal{S}_V \to \mathcal{S}_U$ can be identified with the obvious functor $\mathbf{Set}^V \to \mathbf{Set}^U$ obtained by forgetting components. Thus, the filter-quotient (or filter-power) $\mathcal{S}_{\Phi}$ has as objects equivalence classes of (partial) sequences of sets under "eventual equality" and morphisms are equivalences classes of (partial) sequences of maps under "eventual equality". This is easily seen to be equivalent to the construction you describe.

The filter-quotient construction does not necessarily preserve the property of being a Grothendieck topos. In fact, Adelman and Johnstone [1982] have shown that a filter-power of a Grothendieck topos is again a Grothendieck topos if and only if the filter is principal. In some sense this is not surprising: Grothendieck toposes are defined relative to a set-theoretic universe (or, if you like, a "base topos"), but the filter-quotient construction is akin to forcing, which changes the set-theoretic universe.