Michael Abbott asked whether Set is lfp, intuitionistically.
Or, I hope this is the same question, is an elementary topos with a natural numbers object internally locally finitely presentable? Are there any references for this?
Peter Johnstone said that
the answer is yes, but (like a great many such things) I don't think it is written down anywhere. Finite cardinals are internally finitely presentable (the proof of this is similar to the proof that they are internally projective, see 6.25 in "Topos Theory"), and the fact that every object is internally a filtered colimit of finite cardinals is implicit in the construction of the object classifier (cf. 6.32 in the same reference).
Regarding the notion of LFP category as one way (amongst many) of formulating a generalised (but finitary) algebraic theory, Set is the category of models of the theory with one sort, no operations and (of course) no equations. However, one must be careful. Is the category Set^N lfp? The idea is that an object X is finitely presentable if homming from it preserves filtered colimits. (It is also interesting to investigate directed unions, and filtered colimits of surjections.) But which homming functor do we mean? - the external one C(X,-) : C -> Set - or the internal one (-)^X : C -> C (if C is a CCC or a topos). An object X=(X_n) of Set^N is - externally FP iff sum_n X_n is finite, so Some m.All n>n. X_n=0, - internally FP iff each X_n is finite. So there are far more internally FP objects than externally FP ones. This comes from Section 6.6 of "Practical Foundations of Mathematics", http://www.dcs.qmul.ac.uk/~pt/Practical_Foundations/html/s66.html Paul
One more variation on the ``internal lfp'' theme. Continuing Paul Taylor's
The idea is that an object X is finitely presentable if homming from it preserves filtered colimits. (It is also interesting to investigate directed unions, and filtered colimits of surjections.)
But which homming functor do we mean?
, one might also ask - which filteredness do we mean? In other words, in the condition `all finite diagrams can be coned', there might be several inequivalent finiteness notions to consider. For example, several such notions appeared in early works by Kock, Lecouturier and Mikkelsen, by Johnstone and Linton; Japie Vermeulen was investigating embeddability into a K-finite object; and, as far as I know, Richard Squire has discovered a whole infinite sequence of (intuitionistically, but not classically) inequivalent finiteness notions. I would appreciate references to any other investigations of finite presentability in this context. Mamuka Jibladze
(I meant to send this to "categories" last week - by mistake it only went to Mamuka. Sorry if it's now out of context.) Mamuka Jibladze added to my comments on finite presentability,
one might also ask - which filteredness do we mean? In other words, in the condition `all finite diagrams can be coned', there might be several inequivalent finiteness notions to consider.
Indeed so. That's why I cited Section 6.6 ("Finiteness") of my book - I should have been more explcit about that. Not, of course, that I mean that to be an exhaustive account of the various notions of finiteness. There was a stress on "intuitionistic" in Michael Abbott's original email, which has perhaps got lost in the ensuing discussion. I remember getting very worried about being careful about this, and for example my unpublished paper "The Synthetic Plotkin Powerdomain" with Wesley Phoa was more complicated than it needed to be because I didn't at the time have his confidence in discussing finiteness intuitionistically (= in an elementary topos). However, what I found in writing "Practical Foundations" (with regard to many things but especially) about finiteness is that the traditional ("classical") idioms of mathematical argument are perfectly valid, once one understands the way in which they are idioms for using the rules of natural deduction. The rules for the existential quantifier apparently look very different from the vernacular use of the phrase "there exists" (in which one goes on to make use of the witness), but the correspondence is very clear and natural when you think about it - see Section 1.6. Paul
participants (2)
-
Mamuka Jibladze -
Paul Taylor