Re: functors defined by well-founded induction

["Oosten, J. van" <j.vanoosten@uu.nl>]

Dear Mike,

is the following too simple-minded?

Given a well-founded poset (X,<), a category C and a function F which,
to every functor G from an initial segment of X to C, assigns a cocone
for G.
Then there is a unique functor H:X-->C with the property that for every
x\in X, H(x) is the vertex of the cocone which is F applied to the
restriction of H to {y|y<x}.

Jaap van Oosten

On 7/9/14, 7:39 PM, Michael Shulman wrote:
> Actually, my question is much more basic.
>
> On Wed, Jul 9, 2014 at 2:39 AM, Paul Taylor <cats@paultaylor.eu> wrote:
>> The simple answer is that the recursion has to define the functor,
>> ie the morphisms corresponding to instances of the order relation,
>> and not just the values at individual ordinals, in order to make sense
>> of defining the values at limit ordinals as colimits.
> That's exactly what I said:
>
>>> since we have to define the value of the functor on morphisms too,
>>> and its value at a given object may depend on its value at morphisms
>>> between previous objects.
> All I'm looking for is a general theorem of the form "given a
> well-founded relation < on a set X, and a category C, and
> such-and-such data, there is an induced functor X -> C."  I don't care
> about set-theoretic issues right now, I'm just looking for a place
> where someone has written out exactly how to construct such a functor
> using the well-foundedness of <.  It seems like it should be a
> well-known thing, so that I can just cite it rather than having to
> write out my own proof.
>
> Mike
>


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