Re: functors defined by well-founded induction

[Tadeusz Litak <tadeusz.litak@gmail.com>]

Dear Jaap (and Mike),

sorry for reacting so late to this, we sort of overlooked the discussion...

I'm curious if Jaap's suggestion is a folklore thing and/or whether one can find it in the literature. As it happens,
in a recent work with Stefan Milius we did something very similar defining a "delay" endofunctor on generalized
presheaves over well-founded posets. By "generalized presheaves" I mean presheaves which are not necessarily set-valued,
but can have arbitrary (small) complete category as codomain.

The publicly available version so far is our FiCS 2013 workshop paper:

http://arxiv.org/abs/1309.0895v1

The construction in question is Example 2.4(5).

However, it does not contain too many details. We also have a journal version submitted a few months ago with full
development. As category mailing list does not allow attachments, I'll send it to you separately.

If there are any references we are missing, please let us know (any other comments also very much welcome, of course!)

Regards,
t.




On 10/07/14 14:40, Oosten, J. van wrote:
> 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/ ]