Practical Foundations of Mathematics

Paul Taylor

7.1  Examples of Universal Constructions

Because of the importance of universal properties, we devote this section to collecting examples of them. As usual, the purpose of this is to give the flavour of the many ways in which this concept can behave, rather than to advance or rely on any particular mathematical specialisation. The most directly useful formulation of universal properties is one of the oldest; it is also the one which can most readily be generalised, idiomatically expressing factorisation systems, function-spaces and many other notions. Compare, for example, the next diagram and that in Definition  7.1.7 with the one for orthogonality in Definition  5.7.1.

DEFINITION 7.1.1 We say that h:X® UA is a universal map from the object X Î obS to the functor  U:A® S if, whenever f:X® UQ is another morphism with Q Î obA, there is a unique A-map p:A® Q such that h;U p = f ( cf Remark 3.6.3 for posets).

omitted diagram environment

If every object X has a universal map to U then the latter is called an adjunctible functor.

As we showed for the terminal object in Theorem 4.5.6, the universal property determines A up to unique isomorphism. So it is a description, but in the interchangeable sense which we discussed at the end of Section 1.2. Of course this is why we generalised Russell's theory. Although any description allows us to introduce a function (indeed a funct or, the left adjoint) there is a loss of logical clarity here because of the choices; we prefer to shift the balance of the formulation back from algebra to logic.

EXAMPLES 7.1.2 Adjoint monotone functions.

(a)
Let U:A Ì S = P(S) be the inclusion of the lattice of closed subsets for a system of closure conditions on a set S. Then h:X® UA is the inclusion of an arbitrary subset X Ì S in its closure (Section  3.7).

(b)
The possibility modal operator < > , existential quantifier $ and direct image \funf! in Section  3.8. These will be developed in Section  9.3.

(c)
In general, let U:A® S be a monotone function with F\dashv U. Then h:X® U(FX) is one of the inequalities in Lemma 3.6.2.

Colimits   Examples 3.6.10 gave meets as adjoint monotone functions.

EXAMPLES 7.1.3

(a)
Let U:A® 1 be the unique functor to the category with one object (*) and only its identity morphism. Then h = \id* :*® U0 is the universal map iff 0 Î obA is the initial object. The mediating homomorphism p:0® Q is the unique map, cf Example 3.6.10(a), Definition 4.5.1ff and Definition  5.4.1(a).

(b)
Let U:A® AxA be the diagonal functor A® A,A, and N and Y two objects of A. Then the pair h = n0,n1:N,Y® A,A is universal iff it is a coproduct diagram. Given maps f:N® Q and g:Y® Q, the mediator is p = [f,g], cf Example 3.6.10(b), Definitions 4.5.7ff and 5.4.1(b) . omitted diagram environment

(c)
Let U:A® A\rightrightarrows be the diagonal functor to the category whose objects are parallel pairs;

h = (q,r) is universal iff r = u;q = |;q and q is the coequaliser (Definition 5.1.1(a) and Proposition  5.6.8ff).

(d)
Let Á be any diagram-shape and U:A® AÁ the diagonal or constant functor ( X® l i.X) into the functor category AÁ (Theorem 4.8.10). Then for \typeX(-):Á ® A and A Î obA, h: \typeX(-)® UA is universal iff it is a colimiting cocone. For any cocone f, the mediator p in Definition  7.1.1 is that from the colimit, cf Example 3.6.10(c).

We shall treat general limits and colimits fully in Section  7.3.

Free algebras   Besides coequalisers, the new feature which arises when we move from posets to categories is the free algebra (Chapter VI).

EXAMPLES 7.1.4

(a)
Let U:A® S be the forgetful functor CRng® Set. Then A is Z[X], the ring of polynomials in a set X of indeterminates, and p evaluates polynomials using the assignment f:X® Q.

(b)
With A = Vsp, let A Ì RX consist of those functions a:X® R with non-zero values at only finitely many elements of X. The unit h(x) is the xth basis vector and p(åi\argaixi) = åi\argaif(xi).

(c)
Let U:Rng® Mon, forgetting addition. The free ring A consists of linear combinations of elements of a monoid. When X = G is a group this is called the group ring Z G. Similarly, with K any ring, for the coslice U:K ¯ Rng® Mon (the objects of K¯ Rng are called K- algebras), we get the group ring KG.

(d)
Let A = Rel, Pos, Sp, Graph or Cat and S = Set, with U the forgetful functor. Then A is X with the discrete structure (the empty relation, equality, all subsets open, no arrows, and only identity maps).

Section 7.4 discusses techniques for constructing free algebras.

Completions   An important special case of universal maps arises from ``completing'' an object, so that when it is complete (re-)applying the construction has no (further) effect. This is most the direct analogue of a closure operation (Section 3.7, but see also Section 7.5).

LEMMA 7.1.5 Following Definition 4.4.8, any functor U:A® S is

(a)
full and faithful iff id:UA® UA is a universal map from UA to U for each A Î obA, and

(b)
an equivalence functor iff for every X Î obS there is an invertible universal map h:X º UA.

A (full, and often by convention replete) inclusion A Ì S which is adjunctible is called a reflective subcategory (Corollary  7.2.10(b)).

PROOF:

(a)
[[a]] Both conditions say that "f:UA® UQ . $!p:A® Q.f = id;U p.

(b)
[[b]] For equivalence we also need, for each X Î ob S, some isomorphism h:X º UA. The issue is therefore to show that any such h is a universal map. For any f:X® UQ there is a unique p:A® Q with Up = h-1;f :UA® UQ, since U is full and faithful. []

EXAMPLES 7.1.6 Reflections are sometimes completions (the universal map is injective) and sometimes quotients (where it is surjective).

(a)
Pos Ì Preord is reflective, the quotient h:X\twoheadrightarrow X/ ~ described in Proposition 3.1.10 being the universal map.

(b)
Let S be the category of metric spaces and isometries (functions that preserve distance) and A Ì S the full subcategory of spaces in which every Cauchy sequence (Definition  2.1.2) converges. This is reflective, and the universal map h:X\hookrightarrow A is an inclusion.

(c)
The functor U:Set\hookrightarrow Graph which treats a set as a discrete graph (Example  7.1.4(d)) is the inclusion of a reflective subcategory, where h:X\twoheadrightarrow X/ ~ is given by the set of (zig-zag) components (Lemma 1.2.4 ). Similarly we have the components of a preorder, groupoid or category.

(d)
Imposing laws such as distributivity or commutativity on algebras, for example the reflections of DLat\hookrightarrow Lat, CMon\hookrightarrow Mon and AbGp\hookrightarrow Gp, results in a quotient.

(e)
The reflection of AbGp in CMon adjoins negatives, but unless the monoid has the cancellation property "x, y, z.x+z = y+zÞ x = y (as with N® Z ) there is also identification.

(f)
Let S be the category of integral domains and monomorphisms and Fld Ì S be the full subcategory of fields. Then h:X\hookrightarrow A is the inclusion of X in its field of fractions, for example Z\hookrightarrow Q .

(g)
Let S be the category of well founded relations and simulations, so S º Coalg(P) by Remark 6.3.5. Let A be the full subcategory which consists of the extensional relations; set-theorists call its objects transitive sets, and its maps are set-theoretic inclusions [Osi74]. Then A Ì S is reflective; Andrzej Mostowski (1955) used Definition  6.7.5 to find the extensional quotient set- theoretically. See Exercise 9.62 and [ Tay96a] regarding the axiom of replacement.

Co-universal properties  

DEFINITION 7.1.7 A map e:FX® A is said to be co-universal from the functor F:S® A to the object A if for every map p:FG® A in A there is a unique map f:G® X in S such that Ff;e = p.

omitted diagram environment

EXAMPLES 7.1.8

(a)
Coclosures, universal quantifiers ("), necessity ([]) and other right adjoint monotone functions, analogously to Examples 7.1.2.

(b)
Limits, X = lim\typeAi, the duals of Examples  7.1.3. The co-unit e is the family of projections (pi).

(c)
((-)Ùf)\dashv (fÞ ( = )) in a Heyting semilattice (Proposition 3.6.14).

(d)
Let S be a cartesian closed category and F = (Yx(-)): S® S. Then e:F X® A is universal iff X = AY and e is evaluation.

(e)
For the forgetful functor F:Set® Rel, X = P(A) and e(a) = {a}.

(f)
For F:Set® Pfn, X = Lift A and e(a) = lifta (Definition  3.3.7).

(g)
The co-reflection of Gp into Mon gives the group of units.

(h)
Set, again with the discrete structure, is co-reflective in Bin, Sp, Graph , Preord, Gpd and Cat. Co-universality of e:F X® A says that X is A with the indiscriminate structure (also called indiscrete or chaotic), which cannot distinguish between points. So x® y, x £ y, X(x,y) = {*} , etc for all xy. Classically, the indiscriminate topology only has Æ and X as open sets.

(i)
For any set (``alphabet'') G, the set G of G- streams carries a map read:G® GxG, so it is a coalgebra for the functor (-)xG (Lemma  6.1.8). Let F be the underlying set functor. Then FX® 1 is co-universal from F to 1 ( ie X is the terminal coalgebra) iff X = GN º GNxG, this structure being induced by N+1 º N.

There are also examples of symmetrically adjoint contravariant functors, generalising Galois connections (Proposition  3.8.14). Recall in particular that negation, (-)Þ ^, is symmetrically self-adjoint (Exercise 3.50).

EXAMPLES 7.1.9

(a)
The Lineland Army is a monoid equipped with a symmetric self-adjunction (Example 1.2.7 and Exercise  7.8).

(b)
Let S be any object of a cartesian closed category S, such as W in Set. Then X® SX, as a functor S® Sop, is symmetrically adjoint to itself on the right. omitted diagram environment

(c)
Let S be a field, say R. For a vector space V, the dual space V* consists of the linear maps V® S . Then (-)*:S® Sop defines a self- adjoint functor on the category of vector spaces, whose unit was the original natural transformation (Example 4.8.8(b)).

EXAMPLES 7.1.10

(a)
The inclusion BA Ì HSL of Boolean algebras in the category of Heyting semilattices has both a reflection and a co-reflection, and these functors are the same. Exercise 7.12 shows that this situation always arises from a natural idempotent, in this case \lnot \lnot .

(b)
The inclusion Gp Ì Mon is also both reflective and co-reflective, but now the two adjoints are different, as they are for the inclusion of any complete sublattice (Remark  3.8.9).

Classifying categories   We have constructed the preorder or category of contexts and substitutions Cn[]L for various fragments [] of logic.

REMARK 7.1.11 There is an analogy between Z[[(x)\vec]] and Cn[]L:

(a)
Extensionally, each of them is the system of well formed formulae built up from some indeterminates ([(x)\vec] or L) using certain operations, namely addition and multiplication, or the logical connectives of the fragment []. (Recall also that the hom-set Cn×L([[(x)\vec]:[(X)\vec]],Y) is the free algebra on generators [(x)\vec], modulo the laws.)

(b)
Any sequence [(a)\vec] Î R of elements of another ring, or any model M of L in a semantic world E, may be substituted for the indeterminates, and the syntactic formulae `` evaluated'' using structural recursion. omitted diagram environment

(c)
Intensionally, this is a universal property, because Z[[(x)\vec]] and Cn[]L have the same structure as R or E and [[-]] is the unique homomorphism of this structure taking the generic object to the concrete one.

EXAMPLES 7.1.12 This analogy is precise for propositional logic.

(a)
Let [] be unary propositional logic. Then L® \CloneL is inclusion of (a set with) a binary relation (unary closure condition, Section 3.8) in its reflexive-transitive closure. This is the universal map from L to the forgetful functor U:Preord® Bin; in fact Preord is reflective in Bin (an object of which is a set with a binary endorelation).

(b)
Let [] be Horn logic (propositional algebraic); then U is the forgetful functor from SLat. For propositional geometric and intuitionistic logic, the category A is Frm or HSL (Section 3.9).

(c)
Let [] be classical propositional logic, so A = BA (Boolean algebras), and let X be a finite set. Then Cn booleX = 22X is the set of disjunctive or conjunctive normal forms (Remark 1.8.4) in the set X of atomic propositions, together with their negations.

(d)
U:CSLat® Pos. Then A = shv(X) = [Xop® W], the lattice of lower sets, ordered by inclusion (Definition 3.1.7), with h(x) = X¯ x and p(I) = ÚQ {f(x)|x Î I} by Proposition 3.2.7(b).

It also works at the level of types for unary algebraic theories.

(e)
The classifying monoid for a free single-sorted unary theory gives the universal map to U º List:Mon ® Set. In Section 2.7 we wrote [[l]] = fold(e,m,f,l).

(f)
A many-sorted free unary theory is described by an oriented graph; the classifying category is composed of paths ( U:Cat ® Graph).

(g)
Finally, elementary sketches present equational many-sorted unary theories, and the classifying category is free on the sketch.

REMARK 7.1.13 The intuition that Cn[]L has a polynomial structure is a valuable one, but there are three technical problems.

(a)
For an ``adjunction'' Cn[](-)\dashv L[] we need a category of languages, but there seems to be no convincing notion of map L1® L2, even for elementary sketches. In Sections I §10and II §14of [LS86], Joachim Lambek and Philip Scott define language morphisms to match their semantic interpretation, Cn[]L1® Cn[]L2. However, this is not consistent with our use of Bin and Graph above, and so loses the dynamic aspect of the language which was the theme of Sections 3.7-3.9 and also of Chapter VI. See also Remark  7.5.2.

(b)
The semantic structure corresponding to the type theory (products, exponentials, etc ) is itself characterised categorically by universal properties. In defining the classifying category, should we require [[-]] to preserve them on the nose (and to be unique up to equality), as we expect from syntax, or only up to isomorphism, as is the case for semantics? This question itself is the subject of Section  7.6. If we take the semantic option, then the universal property of the classifying category is more complicated than Definition  7.1.1: the interpretation functor [[-]] is only unique up to unique isomorphism - if it is defined at all, as some Choice is to be made.

(c)
The axiom-scheme of replacement is needed to construct [[-]].

The second question also arises when we define limits and colimits of categories; we shall return to this point at the end of the next section.

REMARK 7.1.15 Historically, these intuitions emerged from algebraic geometry in the form of a classifying topos. The fragment of logic which is classified by toposes (known as geometric logic) includes products, equalisers and arbitrary pullback-stable colimits, the coproducts being disjoint and the quotients effective (Chapter V). In particular it allows existential quantification and infinitary disjunction.

By analogy with polynomials, the classifying topos for, say, groups was written Set[G]. Given a group G in another topos E, [[-]]:Set[G]® E evaluates type-expressions by substituting the particular group G for the generic G. Being a homomorphism of the categorical structure, [[-]] preserves finite limits and has a right adjoint, written \nearrow * º [[-]]\dashv \p*. Such an adjoint pair is called a geometric morphism, and is the analogue for toposes of the inverse and direct image operations on open sets that arise from a continuous function \nearrow between spaces. Then groups in E correspond to continuous functions \nearrow :E® Set[G]; in particular the ``points'' of the topos Set[G] are ordinary groups, since the topos Set denotes a singleton space. Hence Set[G] is thought of as the ``space of groups,'' not to be confused with the category Gp - homomorphisms are in fact the ``specialisation order'' (Example  3.1.2(i)) on this space.

This analogy between model theory and topology explains why both subjects depend so heavily on Choice: it is necessary to find points, models or prime ideals with certain properties. However, propositional geometric logic is only special in so far as its model theory has this familiar points-and- open-sets form, whereas the categorical model theory of full first order logic has not yet been fully worked out. Classifying gadgets may be constructed in a uniform way for any fragment of logic, although we have considered simpler ones; besides, we have been interested in toposes as models of higher order logic, the relevant homomorphisms being logical functors, ie those that preserve W.