NNOs in different toposes "the same"?

NNOs in different toposes "the same"?

[David Roberts]

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


-- 
Dr David Roberts
Research Associate
School of Mathematical Sciences
University of Adelaide
SA 5005
AUSTRALIA


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

Re: NNOs in different toposes "the same"?

[Claudio Hermida]

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

Re: NNOs in different toposes "the same"?

[David Roberts]

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

Re: NNOs in different toposes "the same"?

[Peter Johnstone]

As Claudio has said, inverse image functors always preserve the NNO,
but David's question was: when does the direct image f_* preserve
the NNO? A sufficient condition for this which is weaker than being
local is that f should be connected, i.e. that f^* should be full
and faithful, since then the unit map N -> f_*f^*N is an isomorphism.
But this is certainly not necessary: for example, the inclusion from
sheaves to presheaves on any locally connected internal site in a
topos preserves N (see C3.3.10 in the Elephant). I don't know any
necessary and sufficient condition (other than the condition that
f_* preserves N!); if you restrict to countably cocomplete toposes
(where N is always a countable copower of 1), then f_* preserves N
iff it preserves all countable coproducts, iff f^* is full and faithful
on morphisms with codomain N. But it's not clear to me what significance
this latter condition has.

Peter Johnstone

On Mon, 10 Nov 2014, 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
>

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