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 x, y. 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.