nLab well-founded coalgebra

Contents

Contents

The notion of well-founded coalgebra is due to Paul Taylor (with antecedents in the work of Gerhard Osius). Our account is largely based on (Taylor, section 6.3)), and on his paper The General Recursion Theorem, although in some cases we work with slightly different hypotheses.

Definition

Let CC be a finitely complete category, and let TT be an endofunctor on CC. We will suppose that TT is taut, i.e., preserves pullbacks of monomorphisms (preserves limits of cospans in which one of the cospan arrows is monic). In particular, this implies that TT preserves monos. A helpful example to keep in mind is the covariant power-set functor P:SetSetP: Set \to Set.

Definition

Let θ:XTX\theta: X \to T X be a TT-coalgebra structure on XX. A subobject i:UXi: U \hookrightarrow X in CC is θ\theta-inductive if in the pullback

H j X θ TU Ti TX\array{ H & \stackrel{j}{\to} & X \\ \downarrow & & \downarrow^\mathrlap{\theta} \\ T U & \underset{T i}{\to} & T X }

the map jj factors through ii (note that jj is monic since TT preserves monos).

A coalgebra (X,θ)(X, \theta) is well-founded if the only inductive subobject of XX is XX itself.

Example: Suppose XX is an initial algebra for the endofunctor TT, with algebra structure map α:TXX\alpha: T X \to X. By Lambek’s theorem, α\alpha is invertible, so that XX carries a coalgebra structure θ=α 1:XTX\theta = \alpha^{-1}: X \to T X. It is easy to check that an inductive subobject gives a subalgebra i:UXi: U \to X, but a subalgebra of an initial algebra must be the initial algebra itself. Hence (X,θ)(X, \theta) is well-founded.

Our goal in this article is to show that one can perform inductive arguments and recursive constructions in the abstract context of well-founded coalgebras. An interesting challenge is to make precise what is meant by a recursive construction of a map ϕ:XA\phi: X \to A, where the problem is to show how to build ϕ\phi from the ground up, as it were. Stages in the recursive construction of a morphism will be partial maps, defined as usual as spans

D i f A B\array{ & & D & & \\ & ^\mathllap{i} \swarrow & & \searrow^\mathrlap{f} \\ A & & & & B }

for which the arrow ii is monic. Composition of partial maps is effected by span composition, for which we need only finite cocompleteness (we do not need CC to be a regular category, as we would if we were composing general relations between AA and BB). Notice that since TT preserves the pulling back of monos, it carries partial maps to partial maps and also preserves partial map composition.

We denote a partial map by a dashed arrow

f:ABf: A \dashrightarrow B

(generally without explicitly mentioning the domain DD of ff), or sometimes by a harpoon notation.

Connection with initial algebras

One way of constructing the initial algebra of an endofunctor, (X,α:TXX)(X, \alpha: T X \to X), is by constructing first some fixed point of TT, that is, an object YY together with an isomorphism ξ:YTY\xi: Y \cong T Y. (For example, it might be the terminal coalgebra, whose existence is sometimes easy to establish.) Then, inside YY consider the system of well-founded subcoalgebras of ξ\xi. The colimit of this system, assuming it exists, will be the initial algebra. (More theory to develop here.)

The connection with initial algebras goes a little further. Firstly, an initial TT-algebra is a Peano TT-algebra in the sense of the following definition:

Definition

A TT-algebra (X,α:TXX)(X, \alpha: T X \to X) is semi-Peano if every TT-subalgebra inclusion i:YXi: Y \hookrightarrow X is an isomorphism, and Peano if in addition α\alpha is an isomorphism.

If XX is initial and i:YXi: Y \to X is a subalgebra, then there is a unique algebra map r:XYr: X \to Y, and ir=1 X:XXi r = 1_X: X \to X by initiality, whence iri=ii r i = i and then ri=1 Y:YYr i = 1_Y: Y \to Y as ii is monic. Hence initial algebras are semi-Peano, and Peano by Lambek’s theorem.

Secondly, a functor T:EET: E \to E induces, for any object XX of EE, a functor between slices T *:E/XE/TXT_\ast: E/X \to E/ T X, and so if (X,θ:XTX)(X, \theta: X \to T X) is a coalgebra, we may form an endofunctor on E/XE/X:

E/XT *E/TXθ *E/XE/X \stackrel{T_\ast}{\longrightarrow} E/ T X \stackrel{\theta^\ast}{\longrightarrow} E/X

and of course the terminal object 1 X:XX1_X: X \to X is automatically and uniquely a θ *T *\theta^\ast T_\ast-algebra. The next two propositions then follow immediately from the definitions of inductive subobject and well-founded coalgebra:

Proposition

A subobject i:UXi: U \to X of a TT-coalgebra (X,θ)(X, \theta) is inductive precisely when ii is a θ *T *\theta^\ast T_\ast-subalgebra of the terminal object 1 X1_X of E/XE/X.

Proposition

A TT-coalgebra XX is well-founded precisely when the terminal θ *T *\theta^\ast T_\ast-algebra 1 X1_X is semi-Peano.

Examples

Well-founded relations

The prototype of the notion of well-founded coalgebra is a well-founded relation, which is essentially the same thing as a well-founded coalgebra over the covariant power-set functor P:SetSetP: Set \to Set. In brief, a binary relation \prec on a set XX corresponds to a coalgebra θ:XPX\theta: X \to P X, by saying yxy \prec x if and only if yθ(x)y \in \theta(x). See well-founded relation for more information.

Most of the constructions of this article are well-illustrated by checking them against the background of this prototypical case.

Induction and recursion

“One proves things by induction; one defines things by recursion.” This slogan is not mere pedantry; it is meant to underline a difference between these processes.

A proof by induction, say a proof of a property or predicate R(x)R(x) where xx varies over a domain XX, proceeds by showing that the subobject i:UXi: U \hookrightarrow X defined by RR is an inductive subset with respect to a relation on XX. It follows that RR is universally true on XX, if the relation is well-founded. The same idiom applies more generally to well-founded coalgebras.

A recursive construction on the other hand involves a dependency on prior stages of the construction. A typical application is to define a map f:XAf: X \to A by recursion with respect to a well-founded relation, where f(x)f(x) is specified in three stages:

  • Consider the collection θ(x)={y:yx}\theta(x) = \{y: y \prec x\} of all elements preceding xx;

  • Pass to the values f(y)f(y) defined earlier in the construction, giving a subset P(f)(θ(x))={f(y):yx}P(f)(\theta(x)) = \{f(y): y \prec x\} of AA;

  • Apply a given operation ϕ:P(A)A\phi: P(A) \to A to this subset (P(f)θ)(x)(P(f) \circ \theta)(x), to obtain f(x)f(x).

In the last step, the operation may be only partially defined on P(A)P(A). In fact, the map ff itself may be only partially defined; f(x)f(x) is defined only if ϕ((P(f)θ)(x))\phi((P(f) \circ \theta) (x)) is defined “when we call for it”.

An inductive argument is used to show that ff, so far as it is defined, is uniquely determined. The recursive equation that uniquely determines ff (to the extent that it exists, of course) is

f=ϕP(f)θ.f = \phi \circ P(f) \circ \theta.

Letting x\downarrow x denote the down-closure of an element xXx \in X with respect to \prec (and containing xx), we may then form the set

{xX: g:xA(g=ϕP(g)θ)}\{x \in X: \exists_{g: \downarrow x \to A} (g = \phi \circ P(g) \circ \theta)\}

whence the existence of a map f:XAf: X \to A satisfying the recursive equation might indeed be proven by appeal to an inductive argument.

However, notice that this set is defined by a construction in dependent type theory. For other categories CC, we might not have the luxury of interpreting dependent types, so there it wouldn’t be right to conflate recursion with induction.

It is nevertheless true that one can prove, in rather considerable generality, both an induction principle and recursion theorem for well-founded coalgebras; this will occupy us in the following sections.

References

  • Paul Taylor, Practical Foundations of Mathematics , Cambridge University Press (1999).
  • Paul Taylor, Towards a unified treatment of induction , I: the general recursion theorem (1996). (pdf)

Last revised on January 31, 2016 at 21:46:56. See the history of this page for a list of all contributions to it.