functors defined by well-founded induction

functors defined by well-founded induction

[Michael Shulman]

Suppose I have a well-founded poset W, regarded as a category, and I
would like to define a functor W -> C into some other category by
well-founded recursion.  Is there written out anywhere in the
literature a general schema for doing this?  It's a little more subtle
than defining an ordinary function by well-founded recursion, 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.

Mike


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

functors defined by well-founded induction

[Paul Taylor]

Mike Shulman asked:

> Suppose I have a well-founded poset W, regarded as a category, and
> I would like to define a functor W -> C into some other category
> by well-founded recursion.  Is there written out anywhere in the
> literature a general schema for doing this?  It's a little more
> subtle than defining an ordinary function by well-founded recursion,
> 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.

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.

I suspect, however, that Mike is looking for a more sophisticated
answer than this.

(The particular reason why I suspect this is that he solved the
problem of how to define Conway numbers without using excluding
middle at every level, in the final chapter of the Homotopy Type
Theory book.  Although he apparently discovered this independently,
his solution turned out to be the two-sided analogue of my notion
of "plumpness" for intuitionistic ordinals.)

The well founded recursion is a routine matter if the categories
W and C in Mike's notation are small ones, ie structures within
some ambient universe.   However, if C is Set or any other familiar
large category, even if W is small, we have to invoke some part
of the Axiom-Scheme of Replacement.   For example, if W=omega
and the values are the interated powersets P^n(N) then we cannot
form the colimit of the diagram (or turn the diagram itself into
a fibration) in an arbitrary elementary topos.  This is because,
in set theory, the result is the cardinal aleph_omega and its
members form an elementary topos.

In the mid 1990s I investigated not only intuitionistic ordinals
in a quasi-set theoretic style but also a categorical one.  The
results are summarised in sections 6.3, 6.7 and 9.6 of my book,
"Practical Foundations of Mathematics".

Gerhard Osius showed how one can regard a "set" (epsilon-structure)
as a coalgebra in a topos for the covariant powerset functor.
This structure is extensional if the coalgebra structure map
is mono.  The definition of a "well founded coalgebra" is given
in my book.

One can also apply the same ideas in other categories, varying
the notion of "mono".  Several kinds of intuitionistic ordinals
are obtained by doing this in the category of posets, with the
lattice-of-lower-subsets functor in place of the powerset.

This leads to a purely categorical way of defining transfinite
iterates F^alpha of a functor F and of expressing the Axiom-Scheme
of Replacement.

First, we can encode an ordinal-indexed family of objects,
along with morphisms for the order, by a fibration (internal
to the ambient topos).  Then by standard fibrational methods
we can apply the functor F to the family.  Again by standard
methods we can compute the colimit of F^beta over the "elements"
beta of alpha that are specified by the structure map of the
coalgebra.

Such an internal fibration is the family of iterates of the
functor iff a certain square is a pullback.  The relevant
diagram is in the final pages of the text of my book.

Beware that this is a characterisation not a construction.
We may take the existence of such pullback diagrams as a
purely categorical formulation of (part of) the Axiom-Scheme
of Replacement.

Note also that pullbacks of this kind then form a reflective
subcategory of a category composed of squares.   We therefore
have examples of subcategories that are closed under all
available limits but only have reflectors if Replacement
holds.

Unfortunately, not only is the summary in my book the
only published account of these ideas,  but I do not really
have any more coherent private notes.   I had hoped that
this work might contribute to a categorical debate about
Replacement, but that went off in other directions without me.

Paul Taylor






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

Re: functors defined by well-founded induction

[Michael Shulman]

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/ ]

Re: functors defined by well-founded induction

[Oosten, J. van]

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/ ]

Re: functors defined by well-founded induction

[Tadeusz Litak]

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/ ]

Re: functors defined by well-founded induction

[Michael Shulman]

Dear Jaap,

I also overlooked this email somehow.  (-:

On Thu, Jul 10, 2014 at 5:40 AM, Oosten, J. van <j.vanoosten@uu.nl> wrote:
> 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}.

I think my desired application is probably a bit more complicated than
this, but if you have

>> a place
>> where someone has written out exactly how to construct such a functor

for the simpler version, then I'd love to see it too!

Mike


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