nLab terminal coalgebra for an endofunctor

Redirected from "terminal coalgebras".
Terminal coalgebras

Context

Algebra

Induction

Terminal coalgebras

Introduction

A terminal coalgebra, also called final coalgebra, for an endofunctor FF on a category CC is a terminal object in the category of coalgebras of FF.

If FF has a terminal coalgebra α:XF(X)\alpha\colon X \to F(X), then XX is isomorphic to F(X)F(X) (see below); in this sense, XX is a fixed point of FF. Being terminal, XX is the largest fixed point of FF in that there is a map to XX from any other fixed point (indeed, any other coalgebra), and this map is an injection if CC is Set.

The dual concept is initial algebra. Just as initial algebras allow for induction and recursion, so terminal coalgebras allow for coinduction and corecursion.

Details

Given two coalgebras (x,η:xFx)(x, \eta: x \to F x), (y,θ:yFy)(y, \theta: y \to F y), a coalgebra map is a morphism f:xyf: x \to y which respects the coalgebra structures:

θf=F(f)η\theta \circ f = F(f) \circ \eta

A terminal coalgebra (usually called a final coalgebra in the literature) is of course a terminal object in the category of coalgebras. Many data structures can be expressed as terminal coalgebras of suitable endofunctors; a simple but useful theorem says that terminal coalgebras xx are “fixed points” of their endofunctors, in that FxxF x \cong x. This is the dual form of a theorem discovered long ago by Lambek:

Theorem

If (x,θ:xFx)(x, \theta: x \to F x) is a terminal object in the category of FF-coalgebras, then θ\theta is an isomorphism.

Proof

Define a coalgebra structure on FxF x by Fθ:FxFFxF\theta: F x \to F F x. By terminality of xx, there is a unique coalgebra map f:Fxxf: F x \to x. We claim this is inverse to θ\theta. Indeed, by how we defined the coalgebra structure on FxF x, it is tautological that θ\theta is a coalgebra map. By terminality of xx again, this gives an equation of coalgebra maps:

fθ=1 x.f \circ \theta = 1_x.

On the other hand,

θf=F(f)F(θ)=F(fθ)=F(1 x)=1 Fx\theta \circ f = F(f) \circ F(\theta) = F(f \circ \theta) = F(1_x) = 1_{F x}

where the first equation holds because ff is a coalgebra map. This completes the proof.

To construct terminal coalgebras, the following result is useful and practical. See Adámek's theorem on terminal coalgebras? for an extension of this result.

Theorem

(Adámek) If CC has a terminal object 11 and the limit LL of the diagram

F 31F 2!F 21F!F1!1(1)\ldots F^3 1 \stackrel{F^2 !}{\to} F^2 1 \stackrel{F !}{\to} F 1 \stackrel{!}{\to} 1 \qquad (1)

exists in CC and FF preserves this limit, then the limit carries a structure of terminal coalgebra.

Proof

Let π n:LF n1\pi_n: L \to F^n 1 be the n thn^{th} projection of the limiting cone. Then we have a cone from FLF L to the diagram (1) whose components are

FLFπ nF n+11F n!F n1F L \stackrel{F\pi_n}{\to} F^{n+1} 1 \stackrel{F^n !}{\to} F^n 1

and the induced map FLLF L \to L to the limit is invertible by hypothesis; let θ:LFL\theta: L \to F L be the inverse. We claim the coalgebra (L,θ)(L, \theta) is terminal.

Indeed, suppose (x,η:xFx)(x, \eta: x \to F x) is any coalgebra. We recursively define maps f n:xF n1f_n: x \to F^n 1: let f 0:x1f_0: x \to 1 be the unique map, and

f n+1=F(f n)ηf_{n+1} = F(f_n) \circ \eta

It is easily checked by induction that we have a commutative diagram

F n+11 F n! F n1 Ff n f n+1 f n Fx η x\array{ F^{n+1}1 & \stackrel{F^n !}{\to} & F^n 1 \\ ^\mathllap{F f_n} \uparrow & \nwarrow ^\mathrlap{f_{n+1}} & \uparrow ^\mathrlap{f_n} \\ F x & \underset{\eta}{\leftarrow} & x }

defining a cone from xx to the diagram (1), and inducing a map f:xLf: x \to L such that the following diagram commutes:

FL θ 1 L Ff f Fx η x\array{ F L & \stackrel{\theta^{-1}}{\to} & L \\ ^\mathllap{F f} \uparrow & & \uparrow ^\mathrlap{f} \\ F x & \underset{\eta}{\leftarrow} & x }

This diagram gives the fact that ff is a coalgebra map. Moreover, any coalgebra map f:xLf: x \to L leads to a sequence f n=π nff_n = \pi_n \circ f that satisfies f n+1=F(f n)ηf_{n+1} = F(f_n) \circ \eta, by gluing the second diagram to the commutative diagram

F n+11 F n! F n1 Fπ n π n+1 π n FL θ 1 L\array{ F^{n+1}1 & \stackrel{F^n!}{\to} & F^n 1 \\ ^\mathllap{F \pi_n} \uparrow & \nwarrow ^\mathrlap{\pi_{n+1}} & \uparrow ^\mathrlap{\pi_n} \\ F L & \underset{\theta^{-1}}{\to} & L }

so that we were forced to define the f nf_n by recursion as we did, and the coalgebra map f:xLf: x \to L is therefore uniquely determined.

Examples

Unit interval in the real line

As first observed by Peter Freyd, the unit interval [0,1][0, 1] \hookrightarrow \mathbb{R} inside the real line can be characterized as a suitable terminal coalgebra. There are various ways of realizing this; we give one (but see remarks below).

Consider the category of intervals IntInt, i.e., linearly ordered sets with separate top and bottom elements 11 and 00, and let

F:IntIntF: Int \to Int

be the endofunctor which takes an interval XX to XXX \vee X, the linear order obtained by taking two copies of XX and gluing the top element of the first copy to the bottom element of the second. The real interval [0,1][0, 1] becomes a coalgebra if we identify [0,1][0,1][0, 1] \vee [0, 1] with [0,2][0, 2] and consider the multiplication-by-2 map [0,1][0,2][0, 1] \to [0, 2] as giving a coalgebra structure.

Theorem

The interval [0,1][0, 1] is terminal in the category of coalgebras.

Proof (sketch)

Given any coalgebra structure f:XXXf: X \to X \vee X, any value f(x)f(x) lands either in the “lower” half (the first XX in XXX \vee X), the “upper” half (the second XX in XXX \vee X), or at the precise spot between them, where the top element in the first copy is glued to the bottom element of the second. Intuitively, one could think of a coalgebra structure θ:XXX\theta: X \to X \vee X as giving an automaton where on input x 0x_0 there is output of the form (x 1,h 1)(x_1, h_1), where h 1h_1 is either “upper”, “lower”, or “between”. By iteration, this generates a behavior stream (x n,h n)(x_n, h_n). Interpreting upper as 1 and lower as 0, the h nh_n form a binary expansion to give a number between 0 and 1, and therefore we have an interval map X[0,1]X \to [0, 1] which sends x 0x_0 to that number. Of course, should we ever hit (x n,between)(x_n, between), we have a choice to resolve it as either (bottom X,upper)(bottom_X, upper) or (top X,lower)(top_X, lower) and continue the stream, but these streams are identified, and this corresponds to the identification of binary expansions

.h 1...h n1100000...=.h 1...h n1011111....h_1... h_{n-1} 100000... = .h_1... h_{n-1}011111...

as real numbers. In this way, we produce a unique well-defined interval map X[0,1]X \to [0, 1], so that [0,1][0, 1] is the terminal coalgebra.

Remarks

(More material can be found at coalgebra of the real interval.)

  1. The same proof shows that we could have considered instead the category of posets with separate top and bottom, or even the category of sets with separate top and bottom, with an analogous endofunctor. The reason we chose the category of intervals is (besides the availability of the succinct term ‘interval’) to indicate that choice of interval [0,1][0, 1], as the model which classifies the geometric realization functor, can be justified on the grounds of a universal property, as shown by this theorem.

  2. Freyd, in his original post on this result, was inspired by a similar theorem due to Pavlovic and Pratt, that the half-open interval [0,)[0, \infty) can be described as the terminal coalgebra for the endofunctor that sends a linearly ordered set XX to ω×X\omega \times X with the dictionary order.

  3. The theorem holds in an arbitrary topos (with [0,1][0, 1] being the interval of Dedekind reals), provided that the word “separate” is interpreted correctly:

    p:P(¬(0=p)¬(1=p))\forall p\colon P\; (\neg(0 = p) \vee \neg(1 = p))

    and provided that the process of gluing endpoints is given correctly. See Johnstone’s Elephant, section D.4.7, for an extended discussion.

Categorified example: Trees

The notion of terminal coalgebra may be categorified. For example, given a 2-category CC and a (pseudo) functor F:CCF: C \to C, one may speak of a 2-terminal (pseudo) coalgebra.

A theoretically important example is the category of trees, seen as a 2-terminal coalgebra for the endofunctor on CatCat which takes a locally small category CC to its small-coproduct cocompletion. Further discussion of this point is given at pure set.

The small-coproduct cocompletion of CC is given by a comma category construction: objects are pairs (X,F:X dC)(X, F: X_d \to C) where XX is a set and FF is a functor whose domain is the discrete category on XX, denoted X dX_d. A morphism from (X,F)(X, F) to (Y,G)(Y, G) is a pair (f,Φ)(f, \Phi) where f:XYf: X \to Y is a function and Φ:FGf d\Phi: F \to G \circ f_d is a natural transformation. This category is denoted SetCSet \wr C; it is called a “categorical wreath product” (see also the discussion at club).

Adámek’s theorem may be adapted to this 2-categorical situation. The iterated wreath product (Set) n1(Set \wr)^n 1 may be identified with the category of nn-stage trees:

(Set) n1=Set [n] op(Set \wr)^n 1 = Set^{[n]^{op}}

where [n][n] is the linear order 12n1 \leq 2 \leq \ldots \leq n. Or, what is the same, the category of presheaves T:[n+1] opSetT: [n+1]^{op} \to Set with the condition that T(0)=1T(0) = 1 is terminal; the element of T(0)T(0) is considered to be the root of the tree.

Indeed, we realize an explicit equivalence

Σ:SetSet [n] opSet [n+1] op\Sigma: Set \wr Set^{[n]^{op}} \simeq Set^{[n+1]^{op}}

by defining Σ(X,F:XSet [n] op)\Sigma(X, F: X \to Set^{[n]^{op}}) to be the functor T:[n+1] opSetT: [n+1]^{op} \to Set that on the object level takes 11 to XX, and i+1i+1 to

xXF(x)(i).\sum_{x \in X} F(x)(i).

On the morphism level, T(i+1i)T(i+1 \to i) is the coproduct of morphisms

xXF(x)(ii1)\sum_{x \in X} F(x)(i \to i-1)

(and this makes sense for all 1in1 \leq i \leq n under the convention F(x)(0)=1F(x)(0) = 1).

The morphism

(Set) n!:(Set) nSet(Set) n1(Set \wr)^n !: (Set \wr)^n Set \to (Set \wr)^n 1

used in Adámek’s theorem is identified with the restriction functor

Set [n+1] opSet [n] opSet^{[n+1]^{op}} \to Set^{[n]^{op}}

which restricts presheaves along the inclusion [n][n+1][n] \hookrightarrow [n+1].

The 2-limit of the diagram in Adámek’s theorem is then

Set ω op,Set^{\omega^{op}},

aka the category of trees, where ω\omega is the colimit of the finite ordinals [n][n]. The statement that the category of trees is equivalent to its small-coproduct cocompletion says that the category of trees is equivalent to the category of forests.

Fractals

There is a category theoretic treatments of the self-similarity found in fractals in terms of terminal coalgebras, see Leinster 10, Bhattacharya-Moss-Ratnayake-Rose.

Further examples

Example

A list of notable endofunctors, and their initial algebras/terminal coalgebras.

Nonexistent (co)algebras are labelled with ‘/’, and unknown ones with ‘?’.

Base categoryEndofunctorInitial AlgebraFinal CoalgebraNote, reference
SetConst AAAAAA
SetXXX \mapsto X\varnothing11
SetX1+XX \mapsto 1 + X\mathbb{N}Conatural numbers \mathbb{N}^\inftyextended natural number
SetXA+XX \mapsto A + XA×A \times \mathbb{N}A×+1A \times \mathbb{N} + 1, ie conatural numbers “terminated” (when they aren’t \infty) with AApartial map classifier
SetXX+XX \mapsto X + X or X2×XX \mapsto 2 \times X\emptyset2 2^\mathbb{N} (i.e. one definition of Stream 22)
SetXA×XX \mapsto A \times X\emptysetA A^\mathbb{N} (i.e. one definition of Stream AA)sequence, writer monad, stream
SetXX×XX \mapsto X \times X or X[2,X]X \mapsto [2, X][2,]\emptyset \simeq [2, \emptyset]1 (the unique infinite unlabelled binary tree)
SetX[A,X]X \mapsto [A, X][A,][A, \emptyset]1reader monad
SetX1+A×XX \mapsto 1 + A \times XList AAanother definition of Stream AA; i.e. potentially infinite List AAlist, stream
SetX1+A×X 2X \mapsto 1 + A \times X^2Finite binary tree with AA-labelled nodesPotentially infinite binary tree with AA-labelled nodestree
SetXB+A×X nX \mapsto B + A \times X^nFinite nn-ary tree with AA-labelled nodes and BB-labelled leavesPotentially infinite nn-ary tree with AA-labelled nodes with and BB-labelled leaves
SetXB+A×List(X)X \mapsto B + A \times \text{List}(X)Finite tree with AA-labelled nodes and BB-labelled leavesPotentially infinite tree with AA-labelled nodes with and BB-labelled leavesThe number of subtrees is not fixed to a particular nn, it could be any number
SetXO×[I,X]X \mapsto O \times [I, X]O×[I,]O \times [I, \emptyset]Potentially infinite Moore machine
SetX[I,O×X]X \mapsto [I, O \times X][I,][I, \emptyset]Potentially infinite Mealy machine
SetX𝒫(X)X \mapsto \mathcal{P}(X)//
SetX𝒫 fin(X)X \mapsto \mathcal{P}_{\text{fin}}(X)Finite rooted forestsPotentially infinite finitely-branching rooted forests
Setpolynomial endofunctorW-typeM-type
Bipointed SetsXXXX \mapsto X \vee Xdyadic rational numbers in the interval [0,1][0,1]The closed interval [0,1][0,1] \subseteq \mathbb{R}coalgebra of the real interval
linearly ordered setsXωXX \mapsto \omega \cdot X, where ωX\omega \cdot X is the cartesian product of the natural numbers with the underlying set of XX, equipped with the lexicographic order.\emptysetThe non-negative real numbers 0\mathbb{R}_{\geq 0}real number
Archimedean ordered fieldsXXX \mapsto X the identity functorThe rational numbers \mathbb{Q}The real numbers \mathbb{R}
Archimedean ordered fieldsX𝒟(X)X \mapsto \mathcal{D}(X) where 𝒟(X)\mathcal{D}(X) is the Archimedean ordered field of two-sided Dedekind cuts of XXThe real numbers \mathbb{R}The real numbers \mathbb{R}
Archimedean ordered fieldsX𝒞(X)X \mapsto \mathcal{C}(X) where 𝒞(X)\mathcal{C}(X) is the quotient of Cauchy sequences in the Archimedean ordered field XXThe HoTT book real numbers H\mathbb{R}_HThe Dedekind real numbers \mathbb{R}These are the same objects in the presence of excluded middle or countable choice.
Any categoryThe constant functor XAX \mapsto A given object AAAAAA
Any categoryThe identity functor XXX \mapsto Xinitial objectterminal object
Any extensive categoryX1+XX \mapsto 1 + X given terminal object 11 and coproduct ++natural numbers object?
Any closed abelian categoryXI(AX)X \mapsto I \sqcup (A \otimes X) given tensor unit II, tensor product \otimes, coproduct \sqcup, and object AAtensor algebra of AAcofree coalgebra over AAtensor algebra, cofree coalgebra
\infty -GrpdXΣXX \mapsto \Sigma Xsphere spectrum 𝕊\mathbb{S}?suspension

Terminal coalgebras are the categorical semantics of coinductive types, for instance M-types.

References

Cross-relations between algebraic and coalgebraic aspects of real numbers may be found in this article:

  • Peter Freyd, Algebraic Real Analysis, Theor. Appl. Cat., vol. 20, no. 10 (2008), 215-308. (link)

For category theoretic treatments of the self-similarity found in fractals in terms of terminal coalgebras, see

  • Tom Leinster, A general theory of self-similarity, (arXiv:1010.4474)

  • Prasit Bhattacharya, Lawrence S. Moss, Jayampathy Ratnayake, and Robert Rose, Fractal Sets as Final Coalgebras Obtained by Completing an Initial Algebra, (pdf)

Last revised on January 3, 2024 at 22:23:15. See the history of this page for a list of all contributions to it.