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/ ]