• Nebyly nalezeny žádné výsledky

A quotient of a category by a congruence relation on the arrows is very similar to the concept of the quotient of a monoid by a congruence relation.

We will describe the construction from scratch; you need not know about congruence relations to understand it. The construction we describe is not the most general possible: it merges arrows, but not objects.

3.5 Quotient categories 89 The constructions of this section are used in 4.1.13 and in the chapters on sketches.

3.5.1 Definition An equivalence relation ∼ on the arrows of a category C is acongruence relationif:

CR–1 Wheneverf ∼g, then f andg have the same domain and the same codomain.

CR–2 In this setting,

A h

−−→B f

−−→−−→g C k

−−→D iff ∼g, thenf h∼ghandkf ∼kg.

We denote the congruence class containing the arrowf by [f].

3.5.2 Definition Let∼be a congruence relation on the arrows ofC. De-fine thequotient categoryC/∼as follows.

QC–1 The objects ofC/∼are the objects ofC.

QC–2 The arrows ofC/∼are the congruence classes of arrows ofC. QC–3 Iff :A−→B inC, then [f] :A−→B in C/∼.

QC–4 Iff :A−→B and g:B−→C in C, then [g][f] = [gf] :A−→C in C/∼.

It follows from Exercise 1 that QC–4 is well defined and that the result is indeed a category.

3.5.3 Definition LetC/∼be the quotient of a categoryC by a congru-ence relation ∼. Define Q: C −→C/∼ by QA=A for an object A and Qf= [f] for an arrowf ofC.

It is immediate from QC–4 thatQis a functor.

3.5.4 Proposition Let ∼be a congruence relation on a category C. Let F:C −→Dbe any functor with the property that iff ∼gthenF(f) =F(g).

Then there is a unique functorF0:C/∼ −→D for which F0Q=F.

The proposition says that every way of passing from C to some other category which merges congruent arrows factors throughQ uniquely. This can be perceived in another way:C/∼ is the category constructed fromC by making the fewest identifications consistent with forcing two congruent arrows inC to be the same arrow.

3.5.5 Factorization of functors Every functor factors through a faith-ful one in the following precise sense. Let F : C −→D be a functor. The relation ∼ induced by F on arrows of C is defined by requiring that f ∼g if and only if f and g have the same domain and codomain and F(f) =F(g).

3.5.6 Proposition The relation∼induced byF is a congruence relation onC, and the functor F0:C/∼ −→D induced by Proposition 3.5.4 is faith-ful.

The proof is contained in Exercise 4 below.

A faithful set-valued functor (see 3.3.2) is one for which two different arrows act differently on at least one state. In the special case of monoid actions this is precisely the definition of ‘faithful’ used in the literature (not a coincidence), and the preceding proposition is a well-known fact about monoid actions.

3.5.7 The intersection of any set of congruence relations on a category is also a congruence relation (Exercise 2). This means that ifαis any relation on C with the property that if f αg then f and g have the same domain and the same codomain, then there is a unique smallest congruence relation generated byα.

Thus in particular given two arrows f : A−→B and g :A −→B in a categoryC, there is a quotient category by the congruence relation generated by requiring thatf =g. This is calledimposing the relationf =g. Two arrows in C are merged in the quotient category if requiring that f =g forces them to be merged.

3.5.8 The category of a programming language We described in 2.2.6 the categoryC(L) corresponding to a simple functional programming lan-guageLdefined there. We can now say precisely whatC(L) is.

The definition of L in 2.2.5 gives the primitive types and operations of the language. The types are the nodes and the operations are the arrows of a graph. This graph generates a free categoryF(L), and the equations im-posed in 2.2.5(ii) and (iv) (each of which says that two arrows ofC(L) must be equal) generate a congruence relation as just described. The resulting quotient category is preciselyC(L).

When one adds constructors such as record types to the language, the quotient construction is no longer enough. Then it must be done using sketches. The construction just given is in fact a special case of a model of a sketch (see Section 4.6).

3.5 Quotient categories 91 3.5.9 Functorial semantics Functors provide a way to give a meaning to the constructs of the languageL just mentioned. This is done by giving a functor fromC(L) to some category suitable for programming language semantics, such as those discussed in 2.4.3.

We illustrate this idea here using a functor toSetas the semantics for the language described in 2.2.5.Setis for many reasons unsuitable for program-ming language semantics, but it is the natural category for expressing our intuitive understanding of what programming language constructs mean.

Following the discussion in 2.2.5, we define a semantics functor Σ :C(L)

−→Set. To do this, first we define a functionF on the primitive types and operations of the language.

(i) F(NAT) is the set of natural numbers. The constant 0 is the number 0 andF(succ) is the function which adds 1.

(ii) F(BOOLEAN) is the set{true,false}. The constantstrue and false are the elements of the same name, and F(¬) is the function which switches true and false.

(iii) F(CHAR) is the set of 128 ASCII symbols, and each symbol is a constant.

(iv) F(ord) takes a character to its ASCII value, andF(chr) takes a num-bernto the character with ASCII codenmodulo 128.

LetF(L) be the free category generated by the graph of types and opera-tions, as in 2.6.16. By Proposition 3.1.15, there is a functorFb:F(L)−→Set which has the effect ofF on the primitive types and operations.

This functorFb has the property required by Proposition 3.5.4 that if∼ is the congruence relation on F(L) generated by the equations of 2.2.5(ii) and (iv), thenf ∼gimplies thatFb(f) =Fb(g) (Exercise 5). This means that there is a functor Σ :C(L)−→Set(calledF0 in Proposition 3.5.4) with the property that ifxis any primitive type or operation, then Σ(x) =F(x).

The fact that Σ is a functor means that it preserves the meaning of programs; for example the program (path of arrows)chrsuccordought to produce the next character in order, and in fact


does just that, as you can check. Thus it is reasonable to refer to Σ as a possible semantics of the languageL.

We will return to this example in Section 4.3.12. The construction of C(L) and Σ are instances of the construction of the theory of a sketch in Section 7.5.

3.5.10 Exercises

1. Show that an equivalence relation ∼ satisfying CR–1 is a congruence relation if and only if, for all arrowsf1,f2,g1,g2as in this diagram,

A f1



B g1

−−→−−→g2 C

iff1∼f2 andg1∼g2, theng1f1∼g2f2.

2. Show that the intersection of congruence relations is a congruence rela-tion.

3. Show that the quotient functor in 3.5.3 is full. (Warning: This exercise would be incorrect if we allowed the more general definition of quotient, which allows merging objects as well as arrows.)

4. LetF :C −→D be a functor.

a.Show that the relation∼induced byF(defined in 3.5.5) is a congruence relation.

b. Show that the induced functorF0:C/∼ −→D is faithful.

c.Conclude from this and the preceding exercise that every functorF:C

−→Dfactors as a full functor followed by a faithful functor.

5. LetFband∼be defined as in 3.5.9. Prove thatf ∼gimplies thatFb(f) = F(g).b

6. LetM be a monoid. AcongruenceonM is an equivalence relation∼ with the property that it is a congruence relation for the category C(M) determined byM.

a. Show that an equivalence relation∼onM is a congruence relation if and only if for all elementsm, n, n0 of M, if n∼n0 then mn∼mn0 and nm∼n0m.

b. Let K be the subset {(m, n)|m∼n} of the monoid M ×M. Show thatK is a submonoid ofM×M if and only if ∼is a congruence relation.

(M ×M is the monoid whose elements are all ordered pairs of elements of M with multiplication (m, n)(m0, n0) = (mm0, nn0).)


Diagrams, naturality and sketches

Commutative diagrams are the categorist’s way of expressing equations. Nat-ural transformations are maps between functors; one way to think of them is as a deformation of one construction (construed as a functor) into another.

A sketch is a graph with imposed commutativity and other conditions; it is a way of expressing structure. Models of the structure are given by functors, and homomorphisms between them by natural transformations.

All this will become clearer as the chapter is read. It turns out that the concepts just mentioned are all very closely related to each other. Indeed, there is a sense in which diagrams, functors and models of sketches are all different aspects of the same idea: they are all types of graph homomorphisms in which some or all of the graphs are categories.

The first three sections introduce diagrams, commutative diagrams and natural transformations, three basic ideas in category theory. These concepts are used heavily in the rest of the book. Section 4.4 gives the Godement rules.

These form the basis of the algebra of functors and natural transformations, which is studied in more abstract form in Section 4.8.

Section 4.5 introduces the concepts of representable functor, the Yoneda embedding and universal elements. Working through the details of this pre-sentation is an excellent way of learning to work with natural transforma-tions.

We also recommend studying the introduction to linear sketches and lin-ear sketches with constants in Sections 4.6 and 4.7 as an excellent way to familiarize yourself with both commutative diagrams and natural transfor-mations. However, these two sections may be skipped unless you are going to read Chapters 7, 8, 10 or 11.

Section 4.8 introduces 2-categories, a notion of category that allows map-pings between arrows (called 2-cells) that has been found useful to model program refinement, among other things. This section is not used in the rest of the book.


4.1 Diagrams

We begin with diagrams in a graph and discuss commutativity later.

4.1.1 Definition LetI andG be graphs. A diagramin G ofshapeI is a homomorphismD:I −→G of graphs.I is called theshape graphof the diagramD.

We have thus given a new name to a concept which was already defined (not uncommon in mathematics). A diagram is a graph homomorphism from a different point of view.

4.1.2 Example At first glance, Definition 4.1.1 may seem to have little to do with what are informally called diagrams, for example

A f -B


h@@R ¡ª¡g (4.1)

The connection is this: a diagram in the sense of Definition 4.1.1 is pic-tured on the page with a drawing of nodes and arrows as for example in Diagram (4.1), which could be the picture of a diagramDwith shape graph

i u -j


w@@R ¡ª¡v (4.2)

defined byD(i) =A,D(j) =B,D(k) =C,D(u) =f,D(v) =gandD(w) = h.

4.1.3 Example Here is an example illustrating some subtleties involving the concept of diagram. Let G be a graph with objects A, B and C (and maybe others) and arrowsf :A−→B,g:B −→Candh:B−→B. Consider these two diagrams, where here we use the word ‘diagram’ informally:

A f -B


g A f -RB h

(a) (b)


These are clearly of different shapes (again using the word ‘shape’ infor-mally). But the diagram

A f -B


h (4.4)

4.1 Diagrams 95 is the same shape as (4.3)(a) even though as a graph it is the same as (4.3)(b).

To capture the difference thus illustrated between a graph and a diagram, we introduce two shape graphs

1 u -2 v -3 1 u -R2 w



(where, as will be customary, we use numbers for the nodes of shape graphs).

Now diagram (4.3)(a) is seen to be the diagramD:I −→G withD(1) =A, D(2) =B, D(3) =C, D(u) =f andD(v) =g; whereas diagram (4.3)(b) is E:J −→G withE(1) =A,E(2) =B,E(u) =f andE(w) =h. Moreover, Diagram (4.4) is just likeD (has the same shape), except thatv goes toh and 3 goes toB.

4.1.4 Our definition in 4.1.1 of a diagram as a graph homomorphism, with the domain graph being the shape, captures both the following ideas:

(i) A diagram can have repeated labels on its nodes and (although the examples did not show it) on its arrows, and

(ii) Two diagrams can have the same labels on their nodes and arrows but be of different shapes: Diagrams (4.3)(b) and (4.4) are different diagrams because they have different shapes.

4.1.5 Commutative diagrams When the target graph of a diagram is the underlying graph of a category some new possibilities arise, in partic-ular the concept of commutative diagram, which is the categorist’s way of expressing equations.

In this situation, we will not distinguish in notation between the category and its underlying graph: ifI is a graph andC is a category we will refer to a diagramD:I −→C.

We say thatDiscommutative(orcommutes) provided for any nodes iandj ofI and any two paths

fromitoj inI, the two paths

compose to the same arrow inC. This means that

DsnDsn1. . .Ds1=DtmDtm1. . .Dt1

4.1.6 Much ado about nothing There is one subtlety to the definition of commutative diagram: what happens if one of the numbers m or n in Diagram (4.7) should happen to be 0? If, say,m= 0, then we interpret the above equation to be meaningful only if the nodesiandj are the same (you go nowhere on an empty path) and the meaning in this case is that

DsnDsn−1. . .Ds1= idDi

(you do nothing on an empty path). In particular, a diagramD based on the graph

Ri e

commutes if and only ifD(e) is the identity arrow fromD(i) toD(i).

Note, and note well, that both shape graphs R e

i i d -j

(a) (b)

have models that one might think to represent by the diagram R f


but the diagram based on (a) commutes if and only iff = idA, while the diagram based on (b) commutes automatically (no two nodes have more than one path between them so the commutativity condition is vacuous).

We will always picture diagrams so that distinct nodes of the shape graph are represented by distinct (but possibly identically labeled) nodes in the

4.1 Diagrams 97 picture. Thus a diagram based on (b) in whichdgoes tof andiandj both go toAwill be pictured as

A f


In consequence, one can always deduce the shape graph of a diagram from the way it is pictured, except of course for the actual names of the nodes and arrows of the shape graph.

4.1.7 Examples of commutative diagrams – and others The proto-typical commutative diagram is the triangle

A f -B


h@@R ¡ª¡g (4.8)

that commutes if and only if h is the composite gf. The reason this is prototypical is that any commutative diagram – unless it involves an empty path – can be replaced by a set of commutative triangles. This fact is easy to show and not particularly enlightening, so we are content to give an example.

The diagram

commutes if and only if the two diagrams

C -D

commute (in fact if and only if either one does).

4.1.8 Example An arrowf :A−→B is an isomorphism with inverseg: B−→Aif and only if


-A¾ B

g (4.11)

commutes. The reason for this is that for this diagram to commute, the two paths () and (g, f) from A to A must compose to the same value in the diagram, which means that g f = idA. A similar observation shows that f g must be idB.

4.1.9 Graph homomorphisms by commutative diagrams The defi-nition of graph homomorphism in 1.4.1 can be expressed by a commutative diagram. Let φ= (φ0, φ1) be a graph homomorphism from G to H. For any arrow u:m−→n in G, 1.4.1 requires that φ1(u) :φ0(m)−→φ0(n) in H. This says that φ0(source(u)) = source(φ1(u)), and a similar statement about targets. In other words, these diagrams must commute:

G0 -H0

In these two diagrams the two arrows labeled ‘source’ are of course different functions; one is the source function forG and the other for H. A similar remark is true of ‘target’.

4.1.10 This point of view provides a pictorial proof that the composite of two graph homomorphisms is a graph homomorphism (see 2.4.1). If φ:G

−→H andψ:H −→K are graph homomorphisms, then to see thatψφ is a graph homomorphism requires checking that the outside rectangle below commutes, and similarly with target in place of source:

G0 -H0

The outside rectangle commutes because the two squares commute. This can be checked by tracing (mentally or with a finger or pointer) the paths from G1 toK0to verify that

sourceψ1φ10sourceφ1 (4.14) because the right square commutes, and that

ψ0sourceφ10φ0source (4.15)

4.1 Diagrams 99 because the left square commutes. The verification process just described is called ‘chasing the diagram’. Of course, one can verify the required fact by writing the equations (4.14) and (4.15) down, but those equations hide the source and target information given in Diagram (4.13) and thus provide a possibility of writing an impossible composite down. For many people, Diagram (4.13) is much easier to remember than equations (4.14) and (4.15).

However, diagrams are more than informal aids; they are formally-defined mathematical objects just like automata and categories.

The proof in 2.6.10 that the composition of arrows in a slice gives another arrow in the category can be represented by a similar diagram:



@@R C h-C0

C00 -h0 f?0 ¡f00

¡¡ ª

These examples are instances ofpastingcommutative diagrams together to get bigger ones. (See 4.8.16.)

4.1.11 Associativity by commutative diagrams The fact that the mul-tiplication in a monoid or semigroup is associative can be expressed as the assertion that a certain diagram inSetcommutes.

LetSbe a semigroup. Define the following functions, using the cartesian product notation for functions of 1.2.9:

(i) mult :S×S−→S satisfies mult(x, y) =xy.

(ii) S×mult :S×S×S−→S×S satisfies

(S×mult)(x, y, z) = (x, yz) (iii) mult×S:S×S×S−→S×S satisfies

(mult×S)(x, y, z) = (xy, z)

That the following diagram commutes is exactly the associative law.

S×S -S


S×S×S S×mult-S×S

? mult×S


mult (4.16)

4.1.12 Normally, associativity is expressed by the equationx(yz) = (xy)z for allx, y, zin the semigroup. The commutative diagram expresses this same factwithout the use of variables. Of course, we did use variables in defining the functions involved, but we remedy that deficiency in Chapter 5 when we give a categorical definition of products.

Another advantage of using diagrams to express equations is that dia-grams show the source and target of the functions involved. This is not par-ticularly compelling here but in other situations the two-dimensional picture of the compositions involved makes it much easier to follow the discussion.

4.1.13 In 3.5.7, we described how to force two arrows in a category C to be the same by going to a quotient category. More generally, you can make any setD of diagrams inC commute, by imposing all the relations of the form

are two paths in any diagramD∈D. As before, if one of these paths is the empty path the other must be an identity arrow in order for the diagram to commute.

4.1.14 Diagrams as functors In much of the categorical literature, a diagram in a categoryC is a functorD:E −→C whereE is a category. Be-cause of Proposition 3.1.15, a graph homomorphism into a category extends uniquely to a functor based on the free category generated by the graph, so that diagrams in our sense generate diagrams in the functorial sense. On the other hand, any functor is a graph homomorphism on the underlying graph of its domain (although not conversely!), so that every diagram in the sense of functor is a diagram in the sense of graph homomorphism.