[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

categories: is Set LFP?



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