Practical Foundations of Mathematics

Paul Taylor

7.4  Finding Limits and Free Algebras

Simply as applications of Theorem 7.3.5, we shall show how to find limits and colimits in topology and algebra, and conversely how coequalisers may be used to find initial algebras. As in Chapter  V, this approach quickly identifies many of the basic features of an area of mathematics.

Limits and colimits in topology and order theory   We do not ask that the spaces be T0, the preorders antisymmetric or the groupoids skeletal, as this destroys the adjunction (g) - a quotient such as that in Proposition 3.1.10 must be applied to the colimits.

1     (#1) ^

THEOREM 7.4.1 These categories have limits and colimits.

Any limit of preorders is the limit of the underlying sets, equipped with some order; similarly the vertex classes of a limit of relations, graphs, categories or groupoids (from b).

Moreover the hom-sets are also calculated as limits, and the order relation as a conjunction (from d).

Any limit of spaces is the limit of the underlying sets, equipped with some topology (from b).

The limit of a diagram of discrete relations, etc is discrete (from a). This is not so for spaces, as it is not possible to define the connected components of an arbitrary topological space.

omitted diagram environment omitted diagram environment omitted diagram environment

A colimit of preorders is the colimit of the underlying sets, equipped with some preorder; also the vertex classes of graphs, etc (from g).

A colimit of spaces is the colimit of the underlying sets, equipped with some topology or preorder (from g).

W:Sp Frmop and pts:Frm Spop (Exercise 4.14) are symmetrically adjoint on the right, so they send colimits to limits. The frame of open sets of a colimit is the limit of the frames of open sets of the spaces; in particular the Aleksandrov topology (whose open sets are the upper sets) on a colimit of preorders and the Scott topology (Proposition 3.4.9) on dcpos are found as limits (from e).

A colimit of discrete spaces is discrete (from b).

The set of connected components of a colimit of graphs etc is the colimit of those of the graphs in the diagram (from a).

The space of points of a limit of locales is the limit of the spaces of points of the locales themselves (from e). []

REMARK 7.4.2 It remains to find the topology on a limit.

As we know the underlying set of a limit of spaces, identifying the topology is reduced to a lattice-theoretic problem: it is the coarsest that makes the projections continuous.

Similarly, a colimit carries the finest topology making the inclusions continuous. (In fact these properties may also be expressed in pure category theory, by observing that the points functor Sp Set is a bifibration, Definition  9.2.6(e).)

Limits of locales (colimits of frames) are not in general the same as the corresponding limits of spaces; they must be found using generators and relations, as below. Nuclei (Example  3.9.10(a)) give the most efficient technique; see [Joh82] for more detail. []

REMARK 7.4.3 Van Kampen's Theorem 5.4.8 may also be formulated as the preservation of colimits by a left adjoint. The right adjoint takes a groupoid or category to its nerve, which is a simplicial complex whose 0- and 1-cells are the objects and morphisms, and whose higher n-cells are composable sequences of length n (so Theorem  4.2.12 described the two-dimensional skeleton).

Generators and relations   We can exploit the relationship between left adjoints and colimits to construct free algebras using coequalisers and vice versa .

THEOREM 7.4.4 Every finitary equational algebraic theory L has a free algebra FX/R on any set X of generators for any set R of relations.

PROOF: We can only really sketch this complicated construction.

Forget the sorts and laws of L and the relations R;

add the generators X as nullary operation-symbols to the theory;

Proposition 6.1.11 and Example  6.2.7 give equationally free algebras;

the minimal subalgebra of an equationally free algebra, consisting of raw terms, is well founded and parsable; recall that it may also be constructed either as the colimit Tn(), or as the union of all extensional well founded T-coalgebras (Section  6.3);

it satisfies the recursion scheme by Theorem 6.3.13;

the sorts are restored by restricting to the well formed formulae (Proposition 6.2.6); let \LeftAdjoint0X be the free algebra for the theory L0 (known as the signature) obtained by forgetting the laws of L;

the congruence K is generated from the laws and relations R;

the required free algebra FX/R is the quotient Q = \LeftAdjoint0X/K by this equivalence relation.

Let us spell out the last step; notice that it treats ``general'' laws and ``particular'' relations in the same way, so without loss of generality R includes the laws of L. Each member of R relates two raw terms, so we have a parallel pair of functions R\rightrightarrows \LeftAdjoint0X. Let K be the congruence generated from R in step (g), and Q its quotient in SetS .

omitted diagram environment

For Theorem 5.6.9, the theory must be finitary in order to define the operations on the quotient, making it a coequaliser in Mod(L). Any algebra Q for the equational theory L is a fortiori a model of the free theory L0, and so it has a unique homomorphism \LeftAdjoint0X Q. That it satisfies the laws is exactly to say that the composites with R\rightrightarrows \LeftAdjoint0 X are equal. The composite homomorphisms with K\rightrightarrows \LeftAdjoint0X are also equal because K is the congruence-closure of R. Hence there is a mediating function Q Q, and this is a homomorphism. []

We shall discuss the way in which K is generated shortly.

EXAMPLE 7.4.5 Recall from Example 4.6.3(i) that a category with a given set O of objects is an algebra for a theory with O2 sorts, O+O3 operation-symbols and O2+O2+O4 laws. Theorem  6.2.8(a) constructed the free such algebra on an oriented graph (with the same set O of nodes). By Theorem  7.4.4 we now have the free category on any elementary sketch (Theorem 4.2.12). []

EXAMPLE 7.4.6 Every algebra presents itself by its multiplication table. It is generated by its own elements a A, subject to the relations that each depth 1 expression r([(a)\vec]) TA (Definition  6.1.1) is identified with its value \oprA([(a)\vec]) \evA(r([(a)\vec])) A ( cf the ambiguity in the usage of the word law mentioned in Remarks 1.2.2 and 6.6.4).

omitted diagram environment

This is the canonical language for the algebra A. It has the same operation-symbols as the single-sorted theory for which A is an algebra, plus a constant for each element of A, and a law for each \oprA([(a)\vec]). We shall generalise the canonical language to larger fragments of logic in Section 7.6. []

Daniel Kan's original example of an adjoint derived the tensor product M(-) à la Remark 7.2.4 from the internal hom ( = )M. As such it is constructed from generators and relations.

EXAMPLE 7.4.7 The tensor product of two modules M and N for a commutative ring R is the free R-module generated by symbols \qq (m,n) (for m M, n N) subject to relations such as r\qq (m,n) = \qq (rm,n) and \qq (m,\argn1+\argn2) = \qq (m,\argn1)+\qq (m,\argn2) ( cf Example 3.9.10(e)). []

Computing colimits   Conversely, we may exploit the self-presentation of algebras for finitary algebraic theories. If we had a convincing notion of morphism of languages ( cf Remark 7.1.13(a)), these results would simply be applications of the fact that Cn×(-), being a left adjoint, preserves colimits. Indeed the first is plausibly the coproduct of theories.

LEMMA 7.4.8 Let A and B be generated by X and Y respectively, subject to the relations R and S.

omitted diagram environment

Then the algebra-coproduct A+AB is generated by the disjoint union X+SY modulo R+SS. []

LEMMA 7.4.9 With similar notation, the algebra-coequaliser of B\rightrightarrows A is generated by X subject to relations R+P.

omitted diagram environment

PROOF: The relations S for B are irrelevant: Q is also the coequaliser of FY\rightrightarrows A, where FY is the algebra freely generated by the given generators of B. Then Y may be viewed as an additional system of relations, but these are on A, not FX as required, so let P (FX)2 be the pullback of Y A2. (See Exercise 5.53 for why this is not just the pullback of Y\rightrightarrows A.) []

Some of these manipulations of colimits have been implemented in ML by David Rydeheard [RB88].

Treating relations as another theory   These constructions are not very tractable: they mix the fundamentally incompatible techniques of structural recursion and quotients by equivalence relations. We cannot expect any better (such as from the General Adjoint Functor Theorem 7.3.12), because while programs can be interpreted with coequalisers. From the point of view of machine representation, we have to accept generators and relations as a legitimate way of naming objects. We must also resort to these methods to find coproducts of groups, and so the fundamental groupoids of spaces obtained by surgery à la van Kampen (Theorem 5.4.8) .

Nevertheless some unification is possible, by treating both the creation of raw terms and their identifications under the laws in the same way, as generative processes, but at different levels. (We shall have to do this for generalised algebraic theories in Remark 8.4.2.) We should take the principle of interchangeability more seriously, adding a categorical dimension below that which we're used to considering in mathematics: individuals can only be represented by tokens, with interchange arrows between them, cf the comments in Definition  1.2.12 and Example  2.4.8.

REMARK 7.4.10 The congruence K may be generated in various ways:

It is the closure of (the image of) R A2 = (\LeftAdjoint0X) 2 under
{(\arga1,\argb2),(\arga2,\argb2),,(\argak, \argbk)} \triangleright (\oprA(
), \oprA(
)) (r W)
\triangleright (a,a)       {(a,b)}\triangleright (b,a)       {(a,b),(b,c)}\triangleright (a,c).
It is not possible to separate this into two processes of generating an equivalence relation and generating an L-subalgebra.

It is the free algebra on R for a more complicated theory than L, namely with operation-symbols for each of the closure conditions above, including reflexivity, symmetry and transitivity.

This theory may be chosen to have all of the laws induced by being a congruence on this particular algebra A, or may instead have no laws at all ( cf Lemma 7.4.9), making it a free theory. Another option is the theory of groupoids in Mod(L0). []

Definition 8.1.11 and Example  9.2.4(h) suggest a framework in which such a theory can be formulated, using dependent types and indexed categories. The next section uses self-presentation to give a concise functorial description of algebraic theories. Section 7.6 defines the self- presentation or canonical language of any semantic category using the type theory corresponding to the structure it has.