well founded coalgebras and recursion

well founded coalgebras and recursion

[Paul Taylor]

[Note from moderator: Further categories posts will not be sent out until 
July 28. Sorry for the interruption.]


Well founded coalgebras and recursion

www(dot)paultaylor(dot)eu(slash)ordinals

This is a thorough reworking and generalisation of much
of the work that I did on this topic in the 1990s.

It has been with journal referee(s) since November,
so if that means you, please contact the editor asap.

This was in turn inspired by that of Christian Mikkelsen
and Gerhard Osius in the 1970s (but I mis-attributed
Mikkelsen's work to Osius).  Osius's papers are readily
available, but Mikkelsen's thesis was hard to obtain;
he has now re-typed it himself in LaTeX and put it on
his own website:

www(dot)chrisjuul(dot)dk(slash)math(slash)LL(dot)pdf

Well-orderings were of course introduced by Georg Gantor.
So far as I can gather, the classical notion of well-
foundedness is due to Ernst Zermelo 1935, but I have
been unable to identify who first used the induction scheme
to give the intuitionistic definition.  I would welcome
help with these two historical points.

The principal theorem derives recursion for functions
from induction for predicates.  This appears in most set
theory textbooks, usually without attribution, but
I believe it is due to John von Neumann 1928.

For the generalisation in this paper over the 1990s work
I needed to use Dito Pataraia's 1997 fixed point theorem
for dcpos.   However, I needed a special adaptation of
this, as described in Section 2 of the paper.  (I tried
to discuss it on MathOverflow, but was bullied by a
ring theorist who lectured me on ordinal recursion.)

I found myself drawn into the complicated history of the
classical result of this kind, called the Bourbaki--Witt
theorem, which is intertwined with the history of Zorn's
Lemma, the Axiom of Choice and the Well-Ordering Principle.
It turns out that the Bourbaki--Witt idea was already in
Zermelo's second proof in 1908.

There is some historical discussion in Section 2 of my
paper, but I have a lot of other bibliographical notes
and partial translations of papers from German that
I can share, if anyone wants to take this up as a research
topic in mathematical history.

Turning at last to the category theory:

Osius represented (membership) relations as coalgebras
X-->PX for the covariant powerset functor. Extensionality
is that this structure map is mono and recursion is
given by a "coalgebra-to-algebra" homomorphim (in Adam
Eppendahl's later terminology).

Well-foundedness was implicitly in Mikkelsen's work but
defined explicitly as a "broken pullback" by mine in the
1990s.   I replaced P by any endofunctor that preserves
inverse images (pullbacks of monos) and proved the
recursion theorem (well founded implies recursive)
based on von Neumann's proof.

In the present work, the functor need only preserve monos,
not necessarily their pullbacks.   It is this that
requires fixed points in dcpos instead of lattices.

However, the generalisation goes a lot further than
this: the "monos" themselves are replaced by a
factorisation system.  The "epis" and factorisation
are exploited in Section 8 to define adjoints that
impose well-foundedness and extensionality on any
coalgebra.

The result for extensionality is my version of Mostowski's
theorem and I hope to use the idea to give a categorical
version of the Axiom-Scheme of Replacement.

The final section considers the parts of the theory
that require the functor to preserve inverse images.
This includes the most familiar fact about well-foundedness.
It is also needed for pushouts of extensional well-
founded coalgebras, which for P are the "overlapping
unions" of set theory.

In future work I intend to apply this general theory,
in particular the factorisation systems, to categories
such as those of posets and various kinds of lattices.
This will show how the various kinds of intuitionistic
ordinals that were identified in my work and the Algebraic
Set Theory of Andr? Joyal and Ieke Moerdijk in the 1990s
may be seen as extensional well founded coalgebras.

Paul Taylor

I am now in Birmingham, as an Honorary Senior Research
Fellow in the research group that includes Achim Jung,
Steve Vickers, Mart?n Escardo, Paul Levy and Anupam Das.


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