nLab algebraically compact category

Contents

Context

Category theory

Algebra

Contents

Idea

A category is called algebraically compact if for every endofunctor on it the respective initial algebra coincides with the final coalgebra.

Under categorical semantics of programming languages this condition ensures the existence of inductive-recursive types (e.g. Zamdzhiev 20). For that, recall:

In computer science, a data type is often defined by an isomorphism of types XT(X)X\cong T(X) for some construction TT (an endofunctor on the category of types), namely as a fixed point of an endofunctor. (For example, the natural numbers may be defined – see there – as being fixed +1\mathbb{N} \cong \mathbb{N} + 1 by the operation of disjoint union with a singleton.) These are inductive types.

However, in a language with general recursion (including partial recursive functions), the data types have properties in addition to as the usual inductive ones, which allow coinductive reasoning. For example, in a lazy language such as Haskell, there is an infinity element in \mathbb{N}, which is a fixed point for the successor operation.

In general, it is common to allow the construction TT to be mixed-variance. For example, X(XX)X\cong (X\to X) is a recursive data type whose inhabitants are expressions of the untyped lambda calculus. Thus recursive data types are a generalization of reflexive objects. On the semantic side, recursive data types are sometimes called “recursive domain equations”.

Definition

Definition

A category is algebraically complete if every endofunctor FF has an initial algebra F(A)AF(A) \to A. A category is algebraically cocomplete if every endofunctor FF has a final coalgebra ZF(Z)Z\to F(Z).

By Lambek's lemma, an initial algebra is an isomorphism, and so is a final coalgebra, thus they can be regarded as coalgebras and algebras respectively. This gives rise to a canonical morphism from the initial algebra to the final coalgebra, AZA\to Z.

An algebraically complete and cocomplete category CC is algebraically compact if this canonical morphism from the initial algebra to the final coalgebra is an isomorphism.

Remark

In classical set theory, very few categories are algebraically compact. Thus it is common to restrict attention to certain endofunctors. One might then say that this class of endofunctors is algebraically compact. A leading example is where CC is VV-enriched, in which case we might restrict attention to VV-endofunctors. For example, the cpo\mathbf{cpo}-enriched category of pointed cpo‘s and strict maps is cpo\mathbf{cpo}-algebraically compact.

Recall that a cpo is an ω\omega-chain-complete partial order. The category cpo\mathbf{cpo} comprises cpo’s and continuous maps. A cpo is pointed if it has a bottom element, and a continuous map is strict if it preserves the bottom elements.

Proposition

The category cpo !\mathbf{cpo}_{\bot!} of pointed cpo‘s and strict continuous maps is algebraically compact as a cpo\mathbf{cpo}-enriched category.

Proof sketch.

In a poset-enriched category, an embedding-projection pair is a retract e:XYe:X \to Y, p:YXp: Y\to X such that pe=idp e=id and epide p\leq id.

Let F:cpo !cpo !F:\mathbf{cpo}_{\bot!}\to \mathbf{cpo}_{\bot!} be an endofunctor. Consider the chain of projections

1pF(1)F(p)F(F(1))F(F(p))1 \xleftarrow{p} F(1) \xleftarrow{F(p)} F(F(1)) \xleftarrow{F(F(p))} \dots

We consider the limit DD of this sequence of projections as a poset, which is already a pointed cpo.

Because 11 is also an initial object, each of these projections in the chain forms an embedding-projection pair, and we have a sequence

1eF(1)F(e)F(F(1))F(F(e))1 \xrightarrow{e} F(1) \xrightarrow{F(e)} F(F(1)) \xrightarrow{F(F(e))}\dots

One can show that DD can also be regarded as a colimit of this sequence of embeddings.

Now we use the universal properties of limits and colimits to show that DD is an initial algebra and final coalgebra of FF.

Mixed variance domain equations and minimal solutions

Let T:C op×CCT:C^{op}\times C\to C be a bifunctor. A solution for TT is an object XX together with an isomorphism

a:XT(X,X)a:X \cong T(X,X)

In general there may be many solutions. One approach to comparing them is via retractions. If an object YY is a retract of XX, and YY forms a solution b:YT(Y,Y)b:Y\cong T(Y,Y), then we can ask that the retraction respects the solution, i.e.

Y i X b a T(Y,Y) T(r,i) T(X,X) and X r Y a b T(X,X) T(i,r) T(Y,Y) \array{& Y & \overset{i}\rightarrow & X & \\ b & \downarrow &&\downarrow & a&\\ &T(Y,Y) & \underset{T(r,i)}\rightarrow& T(X,X) & \\ } \quad and \quad \array{& X & \overset{r}\rightarrow & Y & \\ a & \downarrow &&\downarrow & b&\\ &T(X,X) & \underset{T(i,r)}\rightarrow& T(Y,Y) & \\ }
Proposition (Freyd)

If CC and DD are algebraically compact, so is C×DC\times D. If CC is algebraically compact, so is the dual category C opC^{op}.

As a result of this proposition, we solve a mixed-variance domain equation XT(X,X)X \cong T(X,X) for T:C op×CCT:C^{op}\times C\to C on an algebraically compact category by considering the initial algebra / final coalgebra of the endofunctor T¯:C op×CC op×C\bar{T}:C^{op}\times C\to C^{op}\times C given by T¯(X,Y)=(T(Y,X),T(X,Y))\bar{T}(X,Y)=(T(Y,X),T(X,Y)).

Proposition (Freyd, Fiore)

For a bifunctor T:C op×CCT:C^{op}\times C\to C on an algebraically compact category, the solution from the initial algebra / final coalgebra is minimal in the sense that it is uniquely a retract of every solution.

References

The notion is due to:

Barr proposed to look at certain functors as algebraically compact, and gave basic facts about building algebraically compact functors and numerous examples. Fiore and Plotkin looked enriched functors and proved “adequacy” results about data types in programming languages.

Pitts gives a survey and discussion, together with further reasoning principles.

  • Andrew Pitts, Relational properties of domains, Information and Computation, 1996. pdf.

See also:

  • Vladimir Zamdzhiev, Reflecting Algebraically Compact Functors, EPTCS 323, 2020, pp. 15-23 (arXiv:1906.09649)

Last revised on February 17, 2021 at 13:40:59. See the history of this page for a list of all contributions to it.