From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10774 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Paul Taylor Newsgroups: gmane.science.mathematics.categories Subject: well founded coalgebras and recursion Date: Sat, 23 Jul 2022 12:00:03 +0100 Message-ID: Reply-To: Paul Taylor Mime-Version: 1.0 Content-Type: text/plain; format=flowed; charset="ISO-8859-15" Content-Transfer-Encoding: 8BIT Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="3107"; mail-complaints-to="usenet@ciao.gmane.io" To: Original-X-From: majordomo@rr.mta.ca Sat Jul 23 13:57:14 2022 Return-path: Envelope-to: gsmc-categories@m.gmane-mx.org Original-Received: from smtp2.mta.ca ([198.164.44.40]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1oFDkw-0000ct-4M for gsmc-categories@m.gmane-mx.org; Sat, 23 Jul 2022 13:57:14 +0200 Original-Received: from rr.mta.ca ([198.164.44.159]:35388) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1oFDj9-0002HL-Eb; Sat, 23 Jul 2022 08:55:23 -0300 Original-Received: from majordomo by rr.mta.ca with local (Exim 4.92.1) (envelope-from ) id 1oFDik-0004A1-A2 for categories-list@rr.mta.ca; Sat, 23 Jul 2022 08:54:58 -0300 Precedence: bulk Xref: news.gmane.io gmane.science.mathematics.categories:10774 Archived-At: [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/ ]