* NNOs in different toposes "the same"? @ 2014-11-10 1:42 David Roberts 2014-11-11 13:01 ` Claudio Hermida 2014-11-12 11:37 ` Peter Johnstone 0 siblings, 2 replies; 4+ messages in thread From: David Roberts @ 2014-11-10 1:42 UTC (permalink / raw) To: categories@mta.ca list 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/ ] ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: NNOs in different toposes "the same"? 2014-11-10 1:42 NNOs in different toposes "the same"? David Roberts @ 2014-11-11 13:01 ` Claudio Hermida 2014-11-11 22:14 ` David Roberts 2014-11-12 11:37 ` Peter Johnstone 1 sibling, 1 reply; 4+ messages in thread From: Claudio Hermida @ 2014-11-11 13:01 UTC (permalink / raw) To: David Roberts, categories@mta.ca list 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/ ] ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: NNOs in different toposes "the same"? 2014-11-11 13:01 ` Claudio Hermida @ 2014-11-11 22:14 ` David Roberts 0 siblings, 0 replies; 4+ messages in thread From: David Roberts @ 2014-11-11 22:14 UTC (permalink / raw) To: Claudio Hermida; +Cc: categories@mta.ca list 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/ ] ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: NNOs in different toposes "the same"? 2014-11-10 1:42 NNOs in different toposes "the same"? David Roberts 2014-11-11 13:01 ` Claudio Hermida @ 2014-11-12 11:37 ` Peter Johnstone 1 sibling, 0 replies; 4+ messages in thread From: Peter Johnstone @ 2014-11-12 11:37 UTC (permalink / raw) To: David Roberts; +Cc: categories@mta.ca list 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/ ] ^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2014-11-12 11:37 UTC | newest] Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2014-11-10 1:42 NNOs in different toposes "the same"? David Roberts 2014-11-11 13:01 ` Claudio Hermida 2014-11-11 22:14 ` David Roberts 2014-11-12 11:37 ` Peter Johnstone
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).