categories - Category Theory list
 help / color / mirror / Atom feed
* functors defined by well-founded induction
@ 2014-07-08  3:11 Michael Shulman
  0 siblings, 0 replies; 6+ messages in thread
From: Michael Shulman @ 2014-07-08  3:11 UTC (permalink / raw)
  To: categories

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


^ permalink raw reply	[flat|nested] 6+ messages in thread
* functors defined by well-founded induction
@ 2014-07-09  9:39 Paul Taylor
  0 siblings, 0 replies; 6+ messages in thread
From: Paul Taylor @ 2014-07-09  9:39 UTC (permalink / raw)
  To: categories; +Cc: Michael Shulman

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


^ permalink raw reply	[flat|nested] 6+ messages in thread
[parent not found: <e7a7f6a0218b48329967ebf0349ac528@CHEWY.ad.sandiego.edu>]

end of thread, other threads:[~2014-07-30 22:43 UTC | newest]

Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2014-07-08  3:11 functors defined by well-founded induction Michael Shulman
2014-07-09  9:39 Paul Taylor
     [not found] <e7a7f6a0218b48329967ebf0349ac528@CHEWY.ad.sandiego.edu>
2014-07-09 17:39 ` Michael Shulman
2014-07-10 12:40   ` Oosten, J. van
2014-07-30 12:37     ` Tadeusz Litak
     [not found] ` <40aa4cd3ea004811957c877001b40f5e@LANDO.ad.sandiego.edu>
2014-07-30 22:43   ` Michael Shulman

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).