Re: NNOs in different toposes "the same"?

[David Roberts <david.roberts@adelaide.edu.au>]

Hi Claudio

yes, I know this. One can prove it from Freyd's characterisation of N
by finite colimits, as I hinted in my first message. What I'm after is
the other situation, when the direct image functor preserves the NNO.
I believe the geometric morphism being local is enough, but much more
than needed, so I was after weaker/alternative conditions.

David

On 11 November 2014 23:31, Claudio Hermida <claudio.hermida@gmail.com> wrote:
>
> 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/ ]