Re: NNOs in different toposes "the same"?

[Claudio Hermida <claudio.hermida@gmail.com>]

On 2014-11-09, 10:42 PM, David Roberts wrote:
> Hi all,
>
> If have a geometric morphism f: E -> F, what's the/a sensible way to
> say that the natural number objects of E and F are 'the same'? If f is
> local, then f_* preserves colimits, and so both f^* and f_* respect
> natural numbers objects up to iso. But this is a little too strong,
> perhaps, since we only need f_* to respect finite limits to use the
> characterisation of |N by Freyd to show preservation. What other
> conditions could I impose, other than simply that f_* preserves the
> NNO?
>
> Secondly, what if E is the externalisation of an internal topos in F?
> For instance, F = Set and E the externalisation of a small topos, not
> necessarily an internal universe (in fact I don't want this to be the
> case!). Then if I can say what it means for the NNO in E to be 'the
> same as' that in F, I can say that the internal topos has the same NNO
> as the ambient category.
>
> Regards,
>
> David
>
>
Dear David,

The short answer is: the inverse image functor f*:F -> E preserves NNO.

The argument goes as follows: an NNO is an initial (1+)-algebra, that
is, initial for the endofunctor [X] -> [1+X]. Since f* preserves 1 and
+, it induces an isomorphism f*(1+) = (1+_)f*, which in turn induces a
functor

(f*)-alg: (1 +)- alg -> (1+)-alg

Fact (++): The right adjoint f_* induces a right adjoint to f*-alg

Hence (f*)-alg preserves initial objects, aka, NNO.

The Fact (++) can be easily calculated, but a more formal argument is
given as Thm A.5 in

Hermida, Claudio, and Bart Jacobs. "Structural induction and coinduction
in a fibrational setting." Information and Computation 145.2 (1998):
107-152.

Regards,

Claudio


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]