8
$\begingroup$

Any small pretopos $C$ can be embedded into a Grothendieck topos by a fully faithful functor that preserves all the pretopos structure (limits, images, finite unions of subobjects, disjoint coproducts, and quotients of equivalence relations). Namely, we may consider the topos of sheaves for the coherent topology on $C$, with the sheafified Yoneda embedding. If $C$ is (locally) cartesian closed, then that structure is also preserved by this embedding.

My question is, what if $C$ also has a natural numbers object, or more general initial algebras for special endofunctors (e.g. "W-types")? Can we embed it into a topos of sheaves in a way that preserves these initial algebras?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
5
$\begingroup$

Sometimes, but not always.

One case when this is possible is given by Proposition D5.1.8 in Sketches of an Elephant. Namely, if $C$ is a small elementary topos with an NNO that is standard, meaning that the family of all numerals $s^n o : 1\to N$ (for external natural numbers $n\in \mathbb{N}$) is epimorphic, then it can be embedded in a Grothendieck topos by a functor preserving both finite limits and finite colimits. Such a functor then necessarily preserves the NNO, by Freyd's characterization of the latter. The Grothendieck topos is the topos of sheaves on $C$ for the topology consisting of all (not necessarily finite) epimorphic families.

Every Grothendieck topos is standard, but Example D5.1.7 gives an elementary topos with NNO that is not standard. It is the filterquotient of $\rm Set/\mathbb{N}$ by a filter containing the cofinite filter, and it contains a global natural number $\omega : 1\to N$ that is disjoint (as a subobject of $N$) from every numeral $s^n o$. Moreover, just after D5.1.7 it is shown that this topos does not admit a functor to any Grothendieck topos preserving finite limits and finite colimits, and the proof actually shows that it does not admit a functor to any Grothendieck topos preserving finite limits and the NNO. The point is that such a functor would preserve the existence of a global natural number disjoint from every numeral, which is impossible in a standard topos.

Thus, the answer to the question is no in general, even if $C$ is an elementary topos; but yes if $C$ is a standard elementary topos. (I don't know if anything can be said about standard pretoposes; the proof of D5.1.8 is impredicative, as is the proof of Freyd's characterization of NNOs.)

Improve this answer
$\endgroup$
2
  • $\begingroup$ Given that in a Grothendieck topos the NNO is always the coproduct of all the $s^n(0) :1 \to N$, if you can embed a pretopos in a Grothendieck topos in a way that preserves the NNO then the NNO in your pretopos already need to be this colimits. In a pretopos, this condition seem to be stronger than being "standard" (?) $\endgroup$
    – Simon Henry
    May 20, 2021 at 20:16
  • $\begingroup$ @SimonHenry It does seem that way, but I don't have a counterexample, do you? And I guess that if a pretopos does satisfy that condition, then embedding it into the topos of sheaves for the topology of the families of injections into all disjoint and stable coproducts would suffice (even if the pretopos isn't countably extensive)? $\endgroup$
    – Mike Shulman
    May 20, 2021 at 21:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.