Coalgebraically Thinking

November 27, 2008

Posted by David Corfield

$MathML-enabled post (click for more details).$

Having come across Peter Freyd’s coalgebraic characterisation of the reals, I’ve been spending some time of late trying to understand coalgebras. Where an algebra for an endofunctor $F : C \to C$ is an object $A$ of $C$ together with an arrow $α : F (A) \to A$ , a coalgebra for $F$ requires an object $A$ with an arrow $β : A \to F (A)$ .

I’ve traced out what seemed to me an interesting path. First I stumbled upon Bart Jacob’s book Introduction to Coalgebra: Towards Mathematics of States and Observations. This I’d thoroughly recommend. Let me give you some nuggets from it:

The duality with algebras forms a source of inspiration and of opposition: there is a “hate-love” relationship between algebra and coalgebra. (p. v)

As already mentioned, ultimately, stripped to its bare minimum, a programming language involves both a coalgebra and an algebra. A program is an element of the algebra that arises (as so-called initial algebra) from the programming language that is being used. Each language construct corresponds to certain dynamics, captured via a coalgebra. The program’s behaviour is thus described by a coalgebra acting on the state space of the computer. (p. v)

$MathML-enabled post (click for more details).$

There are many similarities (or dualities) between algebras and coalgebras which are often useful as guiding principles. But one should keep in mind that there are also significant differences between algebra and coalgebra. For example, in a computer science setting, algebra is mainly of interest for dealing with finite data elements – such as finite lists or trees – using induction as main definition and proof principle. A key feature of coalgebra is that it deals with potentially infinite data elements, and with appropriate state-based notions and techniques for handling these objects. Thus, algebra is about construction, whereas coalgebra is about deconstruction – understood as observation and modification.(p. 47)

A rule of thumb is: data types are algebras, and state-based systems are coalgebras. But this does not always give a clear-cut distinction. For instance, is a stack a data type or does it have a state? In many cases however, this rule of thumb works: natural numbers are algebras (as we are about to see), and machines are coalgebras. Indeed, the latter have a state that can be observed and modified. (pp. 47-8)

Now, just as initial algebras are a vital part of mathematics, so a key property for coalgebras is finality.

Initial algebras are special, just like final coalgebras. Initial algebras (in Sets) can be built as so-called term models: they contain everything that can be built from the operations themselves, and nothing more. Similarly, we saw that final coalgebras consist of observations only. (p. 48)

If a functor has an initial algebra or final coalgebra, then it’s isomorphic to its image under the functor. Indeed, an initial algebra is like a minimal fixed point of the functor, whereas a final coalgebra is like a maximal fixed point.

Take the functor $F (X) = 1 + A \times X$ , for a fixed set $A$ . Searching for the smallest fixed point, we put in as little as possible. So we build up from the empty set, taking any existing set of lists to a new set which includes the empty list and all lists generated by adding an element of $A$ to the old lists. All finite lists of $A$ elements are generated this way and nothing else, so these lists form the elements of the initial algebra for $F$ . But a larger set is fixed by $F$ , namely, the set of $A$ -streams, or finite and infinite lists of $A$ elements. This in fact is the final coalgebra.

Coalgebras are about observation. We can think of our $F$ as observing about an entity whether it contains something $A$ -detectable or not, and if so which element of $A$ it detects. Have observed something it modifies it. The final coalgebra has as elements all possible outcomes of the behaviour you might observe. Do you still have list elements? If ever no, we have a finite list. If always yes, we have a infinite list. And there’s no other behaviour that can be detected.

Now, this talk of maximality put me in mind of a chapter in a book edited by Donald Gillies, my PhD supervisor, called Revolutions in Mathematics. In ‘A Restoration that Failed’, Herbert Breger argues that where Hilbert presented his style of mathematics as the established norm, it was in fact a very novel way of proceeding. Apparently Finsler (of Finsler geometry fame) promoted an older style of mathematics, where one captures what is taken to be an already existing system by writing a list of properties satisfied by that system, such that the system is maximal with respect to the properties.

When it comes to sets then, rather than worry about the set theoretic paradoxes by controlling their construction, building them bottom up from the empty set and various constructions, instead Finsler defines the system of sets to be that collection which is maximal with respect to certain properties. Breger tells us the story of how by 1928 Finsler’s approach was thoroughly misunderstood, allowing Reinhold Baer to dismiss Finsler’s set theory in a four page paper as inconsistent. Baer showed that any system satisfying Finsler’s axioms can be extended, hence that there is a no maximal such system. But in doing so he is using a different rules of set formation from Finsler.

To Zermelo, Fraenkel, Baer, and others, the idea of definite property is inseparably connected with the notion of set, the underlying philosophy being that well-formed definitions create the object.

Finsler is left to face a lonely battle, and we hear about him still writing in 1969, the year before his death, on how the continuum hypothesis is still open in his set theory, in what he calls ‘classical mathematics’. The neglected Finsler doesn’t even have a Wikipedia entry, and the MacTutor history is as brief as possible.

But there’s no need to feel too sorry for Finsler as his ideas, or something similar, did later see the light of day. In his Non-well-founded Sets, Peter Aczel describes a range of ways of developing a set theory which does not obey well-foundedness, the condition that membership chains must be finite.

If this, as Finsler puts it, is “classical mathematics”, perhaps it is odd that Aczel was inspired by computer science:

The original stimulus for my own interest in the notion of a non-well-founded set came from a reading of the work of Robin Milner in connection with his development of a mathematical theory of concurrent processes. (p. xix)

On the other hand, perhaps we could say that computer scientists are dealing with already existing systems – the program-running computers before them.

Certainly we hear the sound of maximality in Aczel’s book:

Thus, in the case of the axiom system for the natural numbers, the extremal axiom is the principle of mathematical induction, which is a minimalisation axiom, as it expresses that no objects can be subtracted from the domain of natural numbers while keeping the truth of the other axioms. The axiom systems for Euclidean Geometry and the real numbers involve on the other hand completeness axioms. These are maximalisation axioms; i.e. they express that the domain of objects cannot be enlarged while preserving the truth of the other axioms. (p. 106)

Aczel proposes his own anti-foundation axioms, AFA, and discusses it in relation to other such axioms, including FAFA (for Finsler) and SAFA (for Dana Scott). He notes that

It is suprising that it has taken over 50 years for this “success” to come about, whereas Fraenkel only had to wait a handful of years. It is worth recording here that Finsler’s axiom system uses a notion of isomorphism of sets which is different to the one introduced by Mirimanoff. If he had used Mirimanoff’s notion the resulting anti-foundation axiom would have been what I have called Scott’s AFA. (p. 107)

But what has this to do with coalgebra? Well there’s a project called algebraic set theory. In his introduction to the field, Steve Awodey writes:

The new insight taken as a starting point in AST is that models of set theory are in fact algebras for a suitably presented algebraic theory, and that many familiar set theoretic conditions (such as well-foundedness) are thereby related to familiar algebraic ones (such as freeness).

So what about the coalgebras? Well, consider the functor from the category of classes of sets to itself, which sends a class $A$ to the class of subclasses of $A$ which are sets. This restriction must be made, otherwise there would be no fixed points. Now, this functor has as initial algebra the class of sets and as final coalgebra the class of non-well-founded sets. An excellent article here is Rutten and Turi’s On the Foundations of Final Semantics: Non-Standard Sets, Metric Spaces, Partial Orders

So now I’m left wondering what would be possible were we to follow Finsler and opt for a more coalgebraic approach to mathematics. There’s plenty of coalgebraic thinking in mathematics, and you can do no better than to pay a visit to Tom Leinster’s coalgebraic topology for examples, including the category of strict $∞$ -categories as a coalgebra for an enrichment functor on finite product categories.

Then Pavlovic and Escardó tell us about Calculus in Coinductive Form:

Coinduction is often seen as a way of implementing infinite objects. Since real numbers are typical infinite objects, it may not come as a surprise that calculus, when presented in a suitable way, is permeated by coinductive reasoning. What is surprising is that mathematical techniques, recently developed in the context of computer science, seem to be shedding a new light on some basic methods of calculus. We introduce a coinductive formalization of elementary calculus that can be used as a tool for symbolic computation, and geared towards computer algebra and theorem proving. So far, we have covered parts of ordinary differential and difference equations, Taylor series, Laplace transform and the basics of the operator calculus.

But do algebraic blinkers prevent us from doing more coalgebraic thinking? Jacobs tells us that

Coalgebra is still in its infancy.

When it grows up it is expected to help unite

the theory of differential equations with automata and process theory.

While we’re waiting we can enjoy playing the Game of Life coalgebraically.

Posted at November 27, 2008 4:23 PM UTC

TrackBack URL for this Entry: http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/1860

47 Comments & 0 Trackbacks

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

Peter Freyd’s coalgebraic characterisation of the reals

Interesting. This is something I should try to better understand.

I definitely need to find a copy of

Peter J. Freyd: Path Integrals, Bayesian Vision, and Is Gaussian Quadrature Really Good? Electr. Notes Theor. Comput. Sci. 29: (1999)

In physics one notices that globally hyperbolic Lorentzian manifolds naturally carry the structure of a poset (where for points $x$ , $y$ we have $x \leq y$ if and only if “ $y$ is in the future of $x$ ”) and notices that this underlying poset structure remembers a surprising amount of information: every map between globally hyperbolic Lorentzian manifolds which induces a functor on the underlying posets is automatically a conformal isometry of Lorentzian spaces.

In other words: the poset structure on a Lorentzian manifold remembers everything about its pseudo-Riemannian geometry except the volume density.

In this sense, posets which have a top and bottom element, i.e. which have one point that is in the future of all other points, and one point which is in the past of all other ones, are in particular given by the causal subsets $\begin{matrix} (1,1) \\ ↗ & ↖ \\ (1,0) & O & (0,1) \\ ↖ & ↗ \\ (0,0) \end{matrix},$ on which the co-presheaves of observable algebras of the quantum field theory on our Lorentzian spacetime are defined.

Observations like this have made some people play with the idea that all causal subsets of spacetime might have finite cardinality (third item in the definition of a causal set/cause here).

But in any case Peter Freyd’s theorem tells us that the continuum is nicely encoded in the poset language itself:

the endofunctor $Duplicate : {Posets}_{t \neq b} \to {Posets}_{t \neq b}$ on posets with distinct top and bottom element which takes a causal subset $O$ and attaches it to itself $O \mapsto O \lor O$

$\begin{matrix} ↗ & ↖ \\ O \\ ↖ & ↗ \\ ↗ & ↖ \\ O \\ ↖ & ↗ \end{matrix}$ has as “maximal fixed point”, i.e. as final coalgebra the interval $\begin{matrix} ↑ \end{matrix}$ with the continuum ( $≃ ℝ$ ) of points in it.

That’s nice.

Posted by: Urs Schreiber on November 27, 2008 8:29 PM | Permalink | Reply to this

Re: Coalgebraically Thinking

Yes, Freyd’s paper – Path Integrals, Bayesian Vision, and Is Gaussian Quadrature Really Good? – sounds fascinating:

Physicists know how to integrate over all possible paths, computer-vision experts want to assign probabilities to arbitrary scenes, and numerical analysts act as if some continuous functions are more typical than others. In these three disparate cases, a more flexible notion of integration is being invoked than is possible in the traditional foundations for mathematics. If allowed to enter a highly speculative mode, such as the intersection of category theory and computer science, we may bump into some solutions to the problem.

But it does’t seem to have been written up. It only takes up a single page in the journal.

Posted by: David Corfield on November 28, 2008 9:34 AM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

Algebraic or categorical set theory as in

van den Berg, Moerdijk: A unified approach to algebraic set theory

sounds fascinating, but I am confused about the way it is supposed to get started:

I understand the idea seems to be to regard categories somehow as more fundamnetal as sets. But how do we say “category” before first having said “set”?

From p. 5 of the above article it seems one first says “class” then “category” then “set”. Is that so?

Posted by: Urs Schreiber on November 27, 2008 9:13 PM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

I don’t think the idea is to regard categories as more fundamental than sets. I think the idea is more to elucidate the structure of models of certain forms of set theory (ZF), as arising from initial algebras of a certain form. I’m not an expert on this, but here’s my take on it.

Really roughly speaking, one starts with an ambient category of “classes” $C$ , with enough structure to permit one to interpret a certain amount of first-order logic inside, and which also comes equipped with a notion of “smallness” in the form of a “small-power-set” functor

P_{s} : C \to C

which intuitively maps a class $c$ to the class of “small subclasses” [or let us just say “subsets” for short] of $c$ . Under some appropriate assumptions, it is shown that an initial algebra of $P_{s}$ (which would be a class $V$ isomorphic to $P_{s} (V)$ , the class of all subsets of $V$ ) plays the role of a “cumulative hierarchy” of sets that can be used to precisely model the ZF axioms, or at least an intuitionistic version of ZF.

[Technically, the category of “classes” should be a pretopos: that gives enough structure with which to internalize first-order logic. It helps me to think of it as saying that certain number of set-theoretic operations are perfectly “safe” for classes as well. Heck, the category of classes $C$ could be a topos as well, but of course we can’t go too crazy – for example, we can’t then go around contemplating an initial algebra for the power-class functor $P : C \to C$ , otherwise we’d get a fictitious universe $v$ such that $v ≅ P v$ , violating Cantor’s theorem. We can however contemplate an initial algebra for a small-power-set functor $P_{s}$ , and thereby speak of a universe or cumulative hierarchy of “sets”, closed under $P_{s}$ .]

Anyway, I for one think one has to be able to say “collection” before one can say “category”, but that’s not what this is about. Rather, it’s using categorical ideas to get a deeper understanding of the structure of formal ZF, demystifying ZF if you will and laying it bare as a certain form of algebra.

Posted by: Todd Trimble on November 28, 2008 12:31 AM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

Thanks, Todd. I probably know too little about this foundational stuff to really appreciate what’s going on.

My naive impression had been that to get started at the beginnin mathematics has to pull itself on its own bootstraps (in the German original: on its own hair ;-) out of the swamp of unprecise thinking and somehow define what a “collection” is and which axioms that is supposed to fullfill.

In your comment you seem to imply that one can talk about classes before having set up set theory. How does this work? When I look up definitions of “classes” I see that they are formulated in “the context of set theory”, where probably my understanding of that is not good enough to appreciate some subtle differences.

So, concretely, you say:

one starts with an ambient category of “classes” $C$ , with enough structure to permit one to interpret a certain amount of first-order logic inside

Can you give more details about how this works? Can the quotation marks around “”classes”” be removed?

Suppose I made you write a survey article “Foundations of mathematics from a modern topos-theoretic point of view”, how would you start?

Sorry if these questions sound dumb. I’d really like to better understand this.

Another thing I’d like to know is: Jacob Lurie in his “Higher topos theory” adsvertizes working internal to “accessible categories” as a means to avoid most set-theoretical issues. I have only a very rough level of understanding of that, too.

Posted by: Urs Schreiber on November 28, 2008 10:45 AM | Permalink | Reply to this

Re: Coalgebraically Thinking

Suppose I made you write a survey article “Foundations of mathematics from a modern topos-theoretic point of view”, how would you start?

No need to make him – he’s already done so, followed up by this.

Posted by: David Corfield on November 28, 2008 11:03 AM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

he’s already done so, followed up by this.

These are beautiful expositions. If any series of blog posts ever deserved to be repreinted as a book, this does.

I also looked a bit at Sets for mathematics, which, I suppose, is an exposition of this very approach.

And I am very happy with this way of thinking of sets and set theory through the category of sets and its properties. I very much appreciate one of the main points that Todd emphasizes, namely that conceiving membership of elements in sets in terms of morphisms into sets heals one of the main deficiencies of classical set theory.

So if this is the point here, that sets, like any other structure, are best studied in terms of properties of the category they form, I am following.

But I still feel a bit confused, even then: when Todd (or Lawvere-Rosebrugh, I suppose) speaks about the category of sets which is supposed to define what sets are, he uses languge like “given two morphisms xyz there is a morphisms abc such that we have a universal morphism rst” and the like.

Isn’t that, at its basis, circular? In order to say what such language means, don’t we already need to have an idea of what sets are? Or “collections” at least?

I know one has to start somewhere and that starting to talk about mathematics probably has to involve this circularity at some point. We need to pull ourselves on our bootstraps out of the swamp.

So I am wondering about what the state-of-art of thinking about this bootstrap process is. From Todd’s account and from what I have seen in Lawvere-Rosebruch (just the first chapters), is it right that the attitute is this:

we assume there is a “naive notion of collections” which we don’t try to axiomatize. We assume “everybody knows” what it means to say things like “given this” and “there is” and “exists uniquely” etc.

Using such language, we then describe a certain category and then declare: this is the category of sets.

Is that what we do?

Posted by: Urs Schreiber on November 28, 2008 12:02 PM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

This is getting closer to how I look at it. Okay, here’s how I look at it: the word “set” or “collection” is never actually defined (and if we tried, we’d certainly run into the problem of the dictionary, that is, the problem that defining words using other words is bound to be circular). So, for instance, when you use a phrase like “model of set theory”, you have to refer to something like “a collection $V$ together with a binary relation $\in$ on $V$ such that the following axioms are satisfied…”.

What a set theory like ZF does is give a formal language which is sufficiently rich to express all the things mathematicians would like to be able to do with “sets” in practice. [This shift from ontological questions (what sets are) to more operational ones (how are sets used) is a very important one in my mind.]

It should be said that a formal theory like ZF doesn’t use words like “set”: it just puts down first-order logical formulas (with one non-logical symbol, $\in$ , not itself defined but axiomatized) to express the essential properties of things like an infinite set, power sets, and so on. (Naturally, good books on the subject will include some handwaving ancillary comments about “sets”, much as computer code is interlaced with comments addressed to the user.) As a backdrop to this theory, there is first-order logic itself, which the user of the theory must somehow learn the rules for, and there too there can be instances of built-in circularity, as when one uses the word “and” to discuss how the symbol $\land$ works. But the problem is not too serious, since no mathematician worthy of the name ever misunderstands how the rules work in practice [even if that understanding is partly subconscious]. We can even computerize the rules through clever use of logic gates in circuits.

Same with categories-based theories of sets, such as Lawvere’s ETCS which I’ve been blogging about. Once one has mastered the underlying logical apparatus of categories (which you certainly don’t need a full-fledged set theory like ZF for, since the first-order definition of “category” is pretty simple: just look at the opening pages of Freyd & Scedrov’s book Categories, Allegories for instance), you can begin writing down axioms for “the category of sets” [as in ETCS] which pretty much cover any mathematical use you’d like to make of sets.

Not to belabor the point, but one doesn’t need a full-fledged Theory of the Category of categories (as Lawvere and a few others have tried to write down) before using the first-order notion of category as preamble to category-based set theory. Such a Theory would try to include axioms which encompass all the various uses categories are put to, and would include existential axioms like existence of certain functor categories, but that’s asking far more than working familiarity with the notion of category.

Posted by: Todd Trimble on November 28, 2008 2:41 PM | Permalink | Reply to this

Elementary theories

$MathML-enabled post (click for more details).$

when [one] speaks about the category of sets which is supposed to define what sets are, [one] uses language like “given two morphisms xyz there is a morphisms abc such that we have a universal morphism rst” and the like.

Isn’t that, at its basis, circular? In order to say what such language means, don’t we already need to have an idea of what sets are? Or “collections” at least?

No, absolutely not! Do you see words like ‘set’ and ‘collection’ there? No, you only see words like ‘given’ and ‘there is […] such that’, which indicate quantification in first-order logic. That is, you do not need a set theory (or collection theory or whatever), only a logic.

This is true even for Zermelo-Fränkel set theory, which says things like ‘given a and b there is c such that a ∈ c and b ∈ c’ (the axiom of pairing). So ETCS is no more circular than ZF.

This is the situation in which one can justifiably use the word ‘elementary’. Thus, the elementary theory of the category of sets needs no external set theory, just a predicate logic. And you need only a logic to define an elementary topos (as opposed to the earlier concept of Grothendieck topos, which requires a set theory). Perhaps more familiarly, you can do elementary group theory (which has axioms like ‘given a there is b such that ab = 1’) and prove some theorems (such as ‘if all elements have order 2 then commutativity holds’) but not others (such as ‘a group of prime order is cyclic’, which requires an external natural-number arithmetic to state and prove, although still not a full-fledged set theory). Really, ETCS is not much more involved than that.

Posted by: Toby Bartels on November 28, 2008 10:34 PM | Permalink | Reply to this

Re: Elementary theories

$MathML-enabled post (click for more details).$

No, you only see words like ‘given’ and ‘there is […] such that’, which indicate quantification in first-order logic. That is, you do not need a set theory (or collection theory or whatever), only a logic.

I see what you mean. However, if I try hard enough I can still get myself confused about this:

When we say “there is” here, don’t we reall mean: “there is in the collection of morphisms of the category of Sets which we are in the process of defining”.

I mean, for instance we don’t want to say just generally “given two morphisms with coinciding codomain, their pullback exists”. We want to say that this is true in the collection of morphisms of $Sets$ .

So ETCS is no more circular than ZF.

Okay. I was maybe hoping for a moment it would be less circular. But all right.

And I don’t want to be a pain here, but since I am not an expert on these matters, I have further questions:

From the way it is built up, it seems now that large categories are more fundamental than small ones:

if I understand you all correctly, the idea is that one assumes the definition of the category $Sets$ of sets is something we just all happen to understand by grace and which cannot be further questioned without running into circularities.

Given that, we will next define a small category to be a category internal to $Sets$ , I suppose.

This just makes me wonder, because usually when we heare at conferences somebody talk about categories somebody from the audience will interrupt and ask “but your category is not small, so everything is much more involved than you suggest”, and the speaker will usually reply “sure, but, as usual, I will assume that these set-theoretical issues can be dealt with by universe-enlargement, or by invoking accessible categories or by playing some other boring tricks”.

Why is that happening if it’s the large categories which we “understand by grace” and the small ones which require axiomatization??

(I am playing devil’s advocate here. I am not really puzzled by these questions. On the other hand, I wouldn’t mind if some day I could feel that I really know what’s going on in these subtle matters.)

Posted by: Urs Schreiber on November 29, 2008 1:52 PM | Permalink | Reply to this

Re: Elementary theories

$MathML-enabled post (click for more details).$

On the other hand, I wouldn’t mind if some day I could feel that I really know what’s going on in these subtle matters.)

Don’t know if this has already been mentioned in this thread, but have you read Mike Shulman’s Set theory for category theory?

Abstract: Questions of set-theoretic size play an essential role in category theory, especially the distinction between sets and proper classes (or small sets and large sets). There are many different ways to formalize this, and which choice is made can have noticeable effects on what categorical constructions are permissible. In this expository paper we summarize and compare a number of such “set-theoretic foundations for category theory,” and describe their implications for the everyday use of category theory. We assume the reader has some basic knowledge of category theory, but little or no prior experience with formal logic or set theory.

Posted by: Bruce Bartlett on November 29, 2008 2:18 PM | Permalink | Reply to this

Re: Elementary theories

$MathML-enabled post (click for more details).$

Urs writes:

When we say “there is” here, don’t we really mean: “there is in the collection of morphisms of the category of Sets which we are in the process of defining”.

It may not matter what we “really mean” — Toby is talking about formal mathematics here, not psychology!

One of the great advantages of Hilbert’s strategy of formalizing mathematics is that it lets us separate the question “what are the rules of the game?” from the question “what do we think the game means?” Both questions are important, but the first one is much easier, so it’s nice to be able to treat it separately.

When trying to formalize mathematics, people often use first-order logic as an infrastructure for setting up more complicated theories like set theory, category theory and so on. First-order logic is a formalism that includes the usual logical connectives (‘and’, ‘or’, ‘not’, and ‘implies’ are already more than enough), variables which can be quantified over (using $\forall$ and $\exists$ ), and predicates which cannot be quantified over. Typically we include equality as one of the predicates. Finally, there are a few ‘deduction rules’ that say how we can prove things.

First-order logic lets us write down various axioms of set theory. But, we can also go ahead and use first-order logic to write down axioms for category theory or topos theory, skipping the set theory!

This was one of Lawvere’s great realizations: we don’t need to do category theory on top of set-theoretic foundations.

Sadly, this realization was not embraced by many ‘traditional’ logicians — namely, those who held set theoretic foundations as sacred. There was a heated debate, a lot of misunderstanding, and a sad split in the community of logicians.

Luckily, we are blessed here by the presence of Toby and Todd, who are experts on both sides of logic: the ‘traditional’ and the ‘category-theoretic’ approaches.

Posted by: John Baez on November 29, 2008 11:04 PM | Permalink | Reply to this

Re: Elementary theories

$MathML-enabled post (click for more details).$

When we say “there is” here, don’t we reall mean: “there is in the collection of morphisms of the category of Sets which we are in the process of defining”.

Not if you don’t want to. In fact, you don’t have to mean anything about collections, morphisms, or categories at all! Secretly we know what we want these things to mean (the intended semantics), but the actual list of axioms itself makes no reference to this. You may know that David Hilbert said (perhaps apocryphally) ‘It must be possible to replace in all geometric statements the words point, line, plane by table, chair, beer mug.’. So while we know that these are supposed to be functions between sets, and this may inspire our choice of axioms, the axioms themselves make no reference to this fact. You know this, but you what you may not have noticed is that they also make no reference to the fact that these functions are supposed to form a collection (if you even believe that they do).

By the way, as the reference to Hilbert should remind us, we are not defining the category of Sets; we are only axiomatising it!

[I]f I understand you all correctly, the idea is that one assumes the definition of the category Sets of sets is something we just all happen to understand by grace and which cannot be further questioned without running into circularities.

Maybe the guy that came up with the axioms understands the category Sets by grace, but there is no reason why we all should! All that we need to know about sets to use them is the axioms hold, not by grace but by fiat: here are the axioms, now what follows?. And it’s quite possible to question the axioms further (say, to consider whether one axiom follows from the others and is therefore irrelevant, or whether the axioms might in fact be inconsistent, or whether all of the theorems that we’re interested in might follow from a weaker system of axioms, and so on) if we wish, although we certainly don’t have to. What we can’t do, of course, is to try to prove that the axioms are correct for the actual category Sets —unless of course already have some other set theory (say, ZF) and want to see if these axioms (say, of ETCS) hold for that other set theory (which in this case, they do). Or, of course, if we have some intuitive concept of sets, we can see if the axioms seem correct for that, but then there is no question of proof.

You do need to understand something by grace, however: first-order classical logic, the language in which both ETCS and ZF are written. (Actually, you can analyse that a bit further, in a metalogic in which only the so-called ‘negative’ logical operators —⊤, ∧, →, ∀— are used. But I don’t know any way to proceed without those.)

From the way it is built up, it seems now that large categories are more fundamental than small ones:

No, no!

Given that, we will next define a small category to be a category internal to Sets, I suppose.

You can if you want to, and with a little more work you can define a large category and even show how Sets is large and cannot be small.

But tell me this: Until you accept that Sets (as axiomatised, let’s assume, by ETCS) is the basis for defining terms like ‘small’ and ‘large’, why do you say that Sets is large!? These terms ‘small’ and ‘large’ only make sense relative to some standard of size, some particular set theory that tells us what they mean.

Before you have a set theory, and in particular while you are writing down the axioms of ETCS, the most fundamental kind of category is a metacategory: a system of objects and arrows satisfying the axioms of a category, without any assumption as to how many of these there are, whether they form a collection, or even how to state such questions. (Actually it is possible to state in first-order logic such things as ‘There are exactly 5 objects that have exactly 7 endomorphisms apiece.’, but that doesn’t get you very far.) Then once you have some notion of arithmetic (full-fledged set theory is not yet necessary), you get the concepts of finite and infinite category (as well as things like ‘There are exactly a prime number of objects that have exactly a perfect number of endomorphisms apiece.’). And once you have a set theory, you get the concepts of small and large category (or even countable and uncountable category). But until you adopt some set theory to define ‘small’ and ‘large’, your categories are neither. (By default, I use the simple word ‘category’ even for a metacategory, since that is the fundamental concept.)

This just makes me wonder, because usually when we heare at conferences somebody talk about categories somebody from the audience will interrupt and ask “but your category is not small, so everything is much more involved than you suggest”, and the speaker will usually reply “sure, but, as usual, I will assume that these set-theoretical issues can be dealt with by universe-enlargement, or by invoking accessible categories or by playing some other boring tricks”.

If the speaker is only discussing that one category, then they can simply reply that they are discussing a metacategory, and concepts of size do not apply. (But if the objection is that the category actually is large, then there should be some set theory relative to which the category in question is large, and if the speaker is using this, then a more involved answer is necessary.)

Posted by: Toby Bartels on November 29, 2008 11:26 PM | Permalink | Reply to this

Re: Elementary theories

Thanks to everyone for the comments above. I found them really helpful, though I’m still far from comfortable with these things.

Posted by: James on November 30, 2008 12:34 AM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

Here’s a nice introduction to terminal coalgebras, from a talk by Eugenia Cheng at the CT08 conference.

(Incidentally, I don’t usually hear people talk about ‘final’ rather than ‘terminal’ objects — except in the case of coalgebras. I have no idea how this situation came about. Just in case anyone’s confused: final $=$ terminal.)

Eugenia’s talk was about the definition of weak $n$ -category proposed by Todd Trimble in 1999. (See here or here, or Eugenia’s talk, for details.) Todd’s definition only applied for finite $n$ . However, Eugenia and I discovered that by using terminal coalgebras, you can extend the definition to $n = ∞$ .

This is an example of a general principle on initial algebras vs. terminal coalgebras, more or less mentioned by David. One often thinks of the initial algebra for an endofunctor as being the collection of all ‘finite’ objects, and the terminal coalgebra as the collection of all ‘possibly infinite’ objects.

Example The endofunctor $X \mapsto X + 1$ of $Set$ has $ℕ$ as its initial algebra (‘finite’ natural numbers), and $ℕ \cup {∞}$ as its terminal coalgebra (‘possibly infinite’ natural numbers).

There are many other similar examples. The point is that taking terminal coalgebras allows us to ‘leap to $∞$ ’.

Let me mention one more example of this phenomenon, as it’s relevant to the Freyd continuum thing.

Let $C$ be the category of bipointed spaces, by which I mean topological spaces $X$ equipped with two distinct, closed basepoints $x_{-}, x_{+}$ . You can wedge together any two bipointed spaces $X$ , $Y$ to form a new bipointed space $X \lor Y$ . So there’s an endofunctor $X \mapsto X \lor X$ of $C$ .

Fact One (a version of Freyd’s theorem): its terminal coalgebra is the space $[0, 1]$ with the endpoints as basepoints.

Fact Two (easier): its initial algebra is the set of dyadic rationals in $[0, 1]$ , again with $0$ and $1$ as basepoints.

So the initial algebra consists of all numbers in $[0, 1]$ with finite binary expansions, $0 . b_{1} b_{2} \dots b_{n},$ whereas the terminal coalgebra consists of all numbers in $[0, 1]$ with any (possibly infinite) binary expansions, $0 . b_{1} b_{2} \dots .$

Posted by: Tom Leinster on November 28, 2008 12:26 AM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

Can we get all the reals into the picture here, rather than just $[0, 1]$ ? I see Pavlovic and Pratt characterise the $[0, 1)$ interval as the final coalgebra with respect to both

$X \to ℕ \times X,$

and

$X \to 1 + ℕ \times X .$

They also speculate about an intriguing analogy

induction : arithmetic :: coinduction : analysis.

It looks like something necessarily can’t go smoothly for the reals. As above with Tom’s binary expansions, there’s the

$0.011111 . . . = 0.1$

problem.

Pratt and Pavlovic explain how the continuum is not coinductively continuous with respect to addition and multiplication.

Posted by: David Corfield on November 28, 2008 9:00 AM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

Can we get all the reals into the picture here, rather than just $[0, 1]$ ?

It’s an interesting question. In some work on self-similarity, I showed that any given compact metrizable space has a terminal-coalgebra characterization. This can be regarded as a big extension of Freyd’s result. But $ℝ$ is not, of course, compact.

You can cheat. $[0, 1]$ is homeomorphic to the extended real line $[- ∞, ∞]$ . In that sense, we already have a characterization of the extended reals. What’s the coalgebra structure on $[- ∞, ∞]$ ? Well, any endpoint-preserving bijection $[- ∞, ∞] \to [- ∞, ∞] \lor [- ∞, ∞]$ will do, but perhaps the most natural choice is $x \mapsto {\begin{aligned} - \log (- x) \in first copy of [- ∞, ∞], & if x \leq 0 \\ \log x \in second copy of [- ∞, ∞], & if x \geq 0 . \end{aligned}$ I don’t know how useful that observation is.

Posted by: Tom Leinster on November 28, 2008 3:49 PM | Permalink | Reply to this

Re: Coalgebraically Thinking

The question regarding the real line reminds me of something that’s been bugging/intriguing me since PSSL83: is there a similar characterization of R not just as a topological space, but as a group? The characterization of [0,1] gives a categorical point of view on the space L¹[0,1]; what would be very nice is a categorical perspective on the algebra L¹(R)…

Posted by: Yemon Choi on November 28, 2008 6:03 PM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

Yemon, I recently gave another talk in which I mentioned that initial-algebra characterization of $L^{1} [0, 1]$ (the one you saw at PSSL83), and someone asked the same thing: what about the algebra structure? But I’m completely confused. What’s the algebra structure on $L^{1}$ ? It can’t be pointwise multiplication, because (for instance) the function $x \mapsto {\begin{aligned} 1 / \sqrt{x} & if x \in (0, 1) \\ 0 & otherwise \end{aligned}$ is in $L^{1}$ , but its pointwise square isn’t.

Posted by: Tom Leinster on November 29, 2008 8:12 PM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

Hi Tom,
Yes, you’re right that L¹[0,1] isn’t an algebra wrt pointwise product. I was referring to the structure that L¹(R) possesses as a convolution algebra. That is, suppose f and g are continuous, scalar-valued functions on R with compact support, and define f*g by the usual formula for convolution

(1)

(f * g) (t) = \int_{s} f (s) g (- s + t) ds

Then this extends to give a continuous algebra product on L¹(R). (Aside: the same construction works for any locally compact hausdorff group G, so that every such G gives rise to an algebra L¹(G). This is almost a covariant functor from groups to algebras, but not quite, unless we restrict ourselves to certain kinds of morphisms…)

Now: the characterization of L¹[0,1] as `initial in a suitable sense’, seems to be a contravariant version of the characterization of [0,1] as `terminal in a suitable sense’. So we are using the rule of thumb (spaces)^op <—> algebras. But if we want to look at L¹(R) as an algebra, this lives in a world where you want to be covariant in the base space… and this is my confusion.

Actually, I’ve just thought of a variant on the question. Suppose that we fix a locally compact group G, and now try and G-enrich that category of Banach-widgets, i.e. give all objects a G-action and require all morphisms to be G-maps. Would we still get an initial object?

(Puzzle for the unoccupied: what might be my motivation for asking this?)

Posted by: Yemon Choi on November 30, 2008 2:03 AM | Permalink | Reply to this

Re: Coalgebraically Thinking

Thanks, Yemon. I understand the question now. Unfortunately, I’m not even close to an answer.

Posted by: Tom Leinster on December 1, 2008 5:27 AM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

Just to clarify something here: from what I saw on those old 1999 messages on the categories list, Pavlovic and Pratt characterize the interval $[0, 1)$ as the terminal coalgebra of the endofunctor on posets given by ordinal product with $ω$ , that is, with the functor

X \mapsto ℕ \times X

but where the right side is given the dictionary order, not the usual product order. If you use the product order, then the terminal coalgebra is the exponential $ℕ^{ℕ}$ (as in Example 1 of those nice notes of the talk by Eugenia Cheng and Tom Leinster that Tom mentioned).

(Incidentally, I wasn’t able to access that paper by Pavlovic and Pratt. Is the link correct?)

Posted by: Todd Trimble on November 28, 2008 5:29 PM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

Can the $p$ -adic (integers or numbers) be understood coalgebraically, not just in terms of their topology but also their arithmetic?

Posted by: David Corfield on November 28, 2008 9:20 AM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

Interesting question. The $p$ -adic integers $\hat{ℤ_{p}}$ certainly have that kind of coalgebraic flavor to me; here is a guess about how that might work at least additively.

Working with the co-slice category

C = ℤ ↓ Ab

define an endofunctor given by taking the coproduct with the object $ℤ ↪ \frac{1}{p} ℤ$ . As an abelian group, this coproduct would just be the pushout construction

A \mapsto A \oplus_{ℤ} \frac{1}{p} ℤ .

I am conjecturing that the additive group of $p$ -adic integers is the terminal coalgebra for this endofunctor. Roughly, a coalgebra structure

f : A \to A \oplus_{ℤ} \frac{1}{p} ℤ

can be used to generate, for each $a \in A$ , a stream of $p$ -based digits in $\frac{1}{p} ℤ \mod ℤ$ , which I am hoping would glue coherently to form a $p$ -adic integer, thus producing a coalgebra map

A \to \hat{ℤ_{p}} .

Posted by: Todd Trimble on November 28, 2008 6:52 PM | Permalink | Reply to this

Re: Coalgebraically Thinking

Before anyone wastes any time trying to make sense of the preceding comment, I’d better admit that it’s embarrassingly flawed. I’ll see if I can repair it.

Posted by: Todd Trimble on November 29, 2008 1:31 AM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

Hm, now that I’ve slept on it, the original idea I had for constructing the $p$ -adic integers as a terminal coalgebra doesn’t seem so bad after all. There is a repair to be made in what I said earlier, but the rough idea would be just to follow Adamek’s theorem cited in the notes of Eugenia’s talk, with fingers crossed.

So: Adamek’s theorem says that if $C$ is a category with a terminal object $1$ , then a terminal coalgebra for an endofunctor $F : C \to C$ exists, provided that the limit of

\dots \to F^{n + 1} 1 \overset{F^{n}!}{\to} F^{n} 1 \to \dots F 1 \overset{!}{\to} 1

exists and $F$ preserves it.

Again, taking $C$ to be the co-slice $ℤ ↓ Ab$ , the terminal object has as its underlying abelian group the zero group. Repairing slightly what I suggested before, let us take the endofunctor

F : ℤ ↓ Ab \to ℤ ↓ Ab

to be the functor “push out along the arrow $p \cdot - : ℤ \to ℤ$ ”. (That is, if a category $A$ has pushouts, then for any morphism $f : x \to y$ in $A$ there is a functor from the co-slice under $x$ to the co-slice under $y$ , and here we are taking an instance of that.)

Then $F 1$ is the surjection $ℤ \to ℤ_{p}$ . One may check by induction that $F^{n}!$ is the standard surjection

ℤ_{p^{n + 1}} \to ℤ_{p^{n}} .

The limit of the Adamek diagram is then the $p$ -adic integers ${\hat{ℤ}}_{p}$ (clearly that’s true at the abelian group level, and then we use the easy general fact that the underlying functor $x ↓ A \to A$ creates limits).

The only thing left to check is that $F$ preserves this limit. Indeed, the pushout of the exact sequence

0 \to ℤ \overset{p \cdot -}{\to} ℤ \to ℤ_{p} \to 0

0 \to {\hat{ℤ}}_{p} \overset{p \cdot -}{\to} {\hat{ℤ}}_{p} \to ℤ_{p} \to 0 .

There is a morphism from this sequence to

0 \to ℤ_{p^{n}} \to ℤ_{p^{n + 1}} \to ℤ_{p} \to 0

where the first arrow is the standard projection $π_{n} : {\hat{ℤ}}_{p} \to ℤ_{p^{n}}$ and the third arrow is the identity $1 : ℤ_{p} \to ℤ_{p}$ . The middle arrow of this morphism of sequences, which by definition is

F (π_{n}) : F ({\hat{ℤ}}_{p}) \to F (ℤ_{p^{n}}),

does indeed match the standard projection

π_{n + 1} : {\hat{ℤ}}_{p} \to ℤ_{p^{n + 1}}

and I believe we are done. As a slight extra bonus, one could rewrite the entire argument replacing $Ab$ by the category of locally compact Hausdorff abelian groups, and get the compact abelian group of $p$ -adics as a terminal coalgebra.

Posted by: Todd Trimble on November 29, 2008 4:50 PM | Permalink | Reply to this

Re: Coalgebraically Thinking

Cool!

Posted by: Tom Leinster on November 29, 2008 8:18 PM | Permalink | Reply to this

Re: Coalgebraically Thinking

Mac Lane gives a construction of the p-adics using the limit of a diagram that I think is equivalent to yours (taking Z mod p^n+1 down to Z mod p^n) in the category of rings as a n example of creation of limits. (Bottom of page 110 of Mac Lane’s “Categories for the Working Mathematician” (second edition))

Posted by: Robert Furber on December 4, 2008 3:01 AM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

That’s right, and that was the seed diagram that got me started. From there, it was more or less the problem of figuring out how that diagram could be seen to be of the form

\dots \to F^{n + 1} 1 \overset{F^{n}!}{\to} F^{n} 1 \to \dots \to F 1 \overset{!}{\to} 1

i.e., what functor $F : C \to C$ (on which category $C$ ) do we use so that the $n$ -th projection $ℤ_{p^{n + 1}} \to ℤ_{p^{n}}$ arises by applying $F$ to the $(n - 1)$ -st projection.

Unfortunately, I didn’t see how to do this in the category of rings (or something like the category of rings) – that is, I didn’t see how to get the ring of $p$ -adic integers as a terminal coalgebra.

However, I’ll bet one can exploit the terminal coalgebra structure I did find to recover the ring multiplication

m : {\hat{ℤ}}_{p} \otimes {\hat{ℤ}}_{p} \to {\hat{ℤ}}_{p}

coalgebraically, by putting a suitable coalgebra structure on the tensor product (so that $m$ comes about as the unique coalgebra map to the terminal coalgebra). There is in fact a coalgebra structure on the tensor product which I claim is pretty obvious. Then to check that $m$ is the coalgebra map, one thing to do would be to check that its restriction to the coalgebra conclusion

ℤ \otimes ℤ \to {\hat{ℤ}}_{p} \otimes {\hat{ℤ}}_{p}

factors as

ℤ \otimes ℤ \overset{m}{\to} ℤ \to {\hat{ℤ}}_{p} .

I’m hoping that’s enough, by working in the topologized setting mentioned at the end of my prior post, and using a uniform continuity argument plus the fact that the integers in the $p$ -adic topology are dense in the $p$ -adic integers. Well, I’m writing this at a strange time in the morning for me, so I should really look into this carefully when I’m properly awake.

Posted by: Todd Trimble on December 4, 2008 10:38 AM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

The Prüfer group is the Pontryagin dual of the $p$ -adics. Does that duality force the group to be an initial algebra?

Or is this a case of formal duality and concrete duality failing to coincide, as Lawvere and Rosebrugh discuss.

Posted by: David Corfield on December 4, 2008 11:17 AM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

I believe the argument dualizes perfectly: the initial algebra for the functor

F : ℤ ↓ LCHAb \to ℤ ↓ LCHAb

that pushes out along multiplication by $p : ℤ \to ℤ$ is the Prüfer group, constructed as the colimit of

0 \to F (0) \to \dots \to F^{n} (0) \overset{F^{n}!}{\to} F^{n + 1} (0) \to \dots

In fact, the main hypothesis of the dual of Adamek’s theorem becomes even simpler to verify: $F$ preserves this colimit because it is left adjoint to pulling back along multiplication by $p$ .

I still don’t know how to get the topological group $ℚ_{p}$ of $p$ -adics as an initial algebra or final coalgebra in some way (noting in passing that it is Pontryagin dual to itself).

Posted by: Todd Trimble on December 4, 2008 1:03 PM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

One often thinks of the initial algebra for an endofunctor as being the collection of all ‘finite’ objects, and the terminal coalgebra as the collection of all ‘possibly infinite’ objects.

If you want necessarily infinite objects, then you use a functor F such that F(0) = 0, so that there are no finite objects.

Examples:

For x ↦ Ax + 1, the initial algebra consists of lists (finite sequences) of elements of A;
For x ↦ Ax + 1, the final coalgebra consists of streams (finite or infinite sequences) of elements of A;
For x ↦ Ax, the inital algebra is empty;
For x ↦ Ax, the final coalgebra consists of (infinite) sequences of elements of A.

Posted by: Toby Bartels on November 28, 2008 11:15 PM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

This theme has come up before, to what extent is the mathematics we use in physics a reflection of what can be measured about the system, rather than about the system itself? Of course, you might want to say there’s nothing more to a system than the totality of measurements which can be made of it.

In A Tutorial on (Co)Algebras and (Co)Induction, Jacobs and Rutten give the example of

a machine with two buttons $〈 value, next 〉 : X \to A \times X$ , with autonomous activity in time… The possible observations that we can make of the situation are of the form: after pushing the $next$ button $n \in ℕ$ times with intervals $α_{1}, \dots, α_{n}$ , we see a certain value in $A$ after an interval of length $β$ .

The space of observations will be a certain terminal algebra.

The question I’m vaguely trying to feel for is whether certain mathematical constructions arise as holders for all possible observations.

I wonder how quantum systems might be seen in this light.

Posted by: David Corfield on November 28, 2008 11:31 AM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

to what extent is the mathematics we use in physics a reflection of what can be measured about the system, rather than about the system itself

[…]

I wonder how quantum systems might be seen in this light.

I haven’t thought about this in terms of coalgebras. When we discussed the Isham-Döring and Heunen-Spitters approach # my impression had been that the main underlying point they promoted is:

a physical theory is a “pointed topos”, namely a topos $E$ with a single out object $Σ$ , called the “space of states”.

States of the system are morphisms $ψ : 1 \to Σ$ and possible observations are morphsims $P : Σ \to Ω$ . The degree to which it is true that $P$ holds onm the state $ψ$ is given by the morphism $1 \overset{ψ}{\to} Σ \overset{P}{\to} Ω$ .

Of course that’s just the standard underlying idea of toposes, retold using physics terminology.

Posted by: Urs Schreiber on November 28, 2008 12:17 PM | Permalink | Reply to this

Re: Coalgebraically Thinking

“to what extent is the mathematics we use in physics a reflection of what can be measured about the system, rather than about the system itself”

meaning?? non-quantitative aspects?
how do you get a hold on `the system itself’??

Posted by: jim stasheff on November 29, 2008 10:36 PM | Permalink | Reply to this

Re: Coalgebraically Thinking

$MathML-enabled post (click for more details).$

From the computer science point of view, this is the idea of the black box. Maybe all I can find out about the workings of some black boxes is by repeatedly pressing a button and reading off a value from set $A$ .

If that’s all I can possibly know, I may say that my state space is the set of infinite streams of elements of $A$ , with ‘dynamics’ given by $〈 head, tail 〉$ .

Posted by: David Corfield on November 30, 2008 1:27 PM | Permalink | Reply to this

Re: Coalgebraically Thinking

When you observe a quantum system you whack it with a hermitian operator and get back a probability distribution on the set of eigenvalues for that operator. Speaking loosely, if H is the set of hermitian operators on your state space V, then from an observ

The n-Category Café

Skip to the Main Content

November 27, 2008