ñòð. 13 |

Â¡ @

Â¡

Âª ? R

@

- c0 Â¾

c1 c1

s t

to go to the cone

sÂ£s

Â¡ @

p1 Â¡ @ p2

Â¡ @

Âª

Â¡ ? R

@

- 1Â¾

s s

which unfortunately is not a cone in the sketch for monoids. However, it is a cone

in the FL theory for the sketch for monoids, so it would appear that, although

we cannot realize the functor in question as induced by a sketch homomorphism

from the sketch for categories to the sketch for monoids, it is nevertheless induced

by a homomorphism to a sketch { the underlying sketch of the theory of monoids.

It is clear that, as the preceding example illustrates, one would normally

want to consider homomorphisms of theories (functors that preserve Â¯nite limits

in this case) rather than homomorphisms of sketches. In practice, one would

construct a homomorphism from a sketch to the theory of a sketch since

36 The category of sketches

such a homomorphism would extend essentially uniquely to a mapping between

theories. An alternative would be to adjoin just what you need to to make the

homomorphism work (the cone of Diagram (ES 3.3.7) { and others { in this case),

but that seems excessively clumsy when the whole theory exists in any case.

3.3.8 It is almost immediate that Propositions ES 3.3.2, ES 3.3.3 and ES 3.3.4

remain true if the category Sketch is replaced by the category of sketches with

diagrams based on a speciÂ¯c class of shape graphs, cones to speciÂ¯c class of

shape graphs not necessarily the same as that of the diagrams, and cocones from

a speciÂ¯c class of shape graphs not necessarily the same as either of the other

two. For example, taking any shapes for the diagrams, Â¯nite discrete shapes for

the cones, and no shapes for the cocones gives the category of FP sketches and

homomorphisms between them, so all these propositions are true of FP sketches.

3.3.9 Sentences For this subsection only, we will say a sentence in a sketch

is a diagram, cone or cocone in the graph of , not necessarily one in the

speciÂ¯ed set of diagrams, cones or cocones. The sentence is satisÂ¯ed in a model

M of if it commutes when M is applied (if it is a diagram) or if it is a limit

(co)cone when M is applied (if it is a (co)cone).

Â¡!

If F : is a sketch homomorphism, and Â¾ is a sentence of , then

F (Â¾) is a sentence of where F (Â¾) is deÂ¯ned by composition: this follows from

the deÂ¯nition of sketch homomorphism.

Â¡!

3.3.10 Proposition If F : is a sketch homomorphism and Â¾ is a

sentence of , then F (Â¾) is satisÂ¯ed in a model M of in a category if and

only if Â¾ is satisÂ¯ed in Mod (F )(M ).

This follows directly from the deÂ¯nitions and is left as an exercise.

Propositions ES 3.3.4 and ES 3.3.10 imply that the category of sketches with

designated shape graphs for each of the diagrams, cones and cocones, together

with sentences, form a `simple institution' in the sense of [Goguen and Burstall,

1986].

3.3.11 The results of this section show the way in which sketches are a very

diÂ®erent method for describing mathematical structures from the theories of tra-

ditional mathematical logic. Of course, sketches use graphs, diagrams, cones and

cocones instead of variables, symbols, expressions and formulas, but that diÂ®er-

ence, although signiÂ¯cant, is not the biggest diÂ®erence. When you use sketches,

you factor the entire descriptive process diÂ®erently. We have already discussed

the diÂ®erences to some extent for FP sketches in 7.2.8.

An example of the subtlety of the diÂ®erence is exempliÂ¯ed by our word `sen-

tence' above. Diagrams correspond to universally quantiÂ¯ed sentences, and the

correspondence, which is not entirely trivial (see Section 7.7), is nevertheless ex-

act. But to use a cone as a sentence corresponds to a statement about a type in

3.3 The model category functor 37

multisorted logic, rather than statements about terms. (McLarty [1986] makes

this explicit.) Such statements have not played a big role in classical logic. In

classical logic, you do not say (with an axiom) that a type is (for example) a

product type; the product type is implicit in the existence of some given term

which has a sequence of variables of speciÂ¯c types.

On the other hand, our sentences do not provide a way of giving universal

Horn clauses in (for example) an FL sketch. When using sketches, universal Horn

clauses are usually implicit. Such a clause which must be satisÂ¯ed in all models

is given by an arrow built into the graph of the sketch which causes an operation

to factor through some limit type. Thus if you wanted to require

a = b ) g(f(a; b)) = h(f (a; b))

where a and b are of type A, f is an operation of type C and g and h are operations

of type D, you build the graph of your sketch with arrows f : A Â£ A Â¡ C, g; h : C

!

Â¡ D, e : E Â¡ C, u : A Â¡ E and d : A Â¡ A Â£ A, with cones requiring A Â£ A

! ! ! !

to be the required product, e to be the equalizer of g and h, d to be the diagonal

map, and this diagram

d- A Â£ A

A

u f

? ?

-C

E e

which requires f Â± d to factor through the equalizer of g and h. It is built into

the graph in a way analogous to the way in classical logic you build the product

types implicitly by incorporating speciÂ¯c terms.

There is presumably a theory of sentences built in this way which makes FL

sketches an institution, but it will require work to produce it: it does not Â¯t well

with the ingredients of a sketch. In the same way, building an institution out

of classical logic using a deÂ¯nition of sentence which allows you to state that a

type is a certain equalizer or pullback requires work because it does not Â¯t the

traditional way of doing things. (It is not impossible, it merely does not Â¯t well.)

The classical approach and the sketch approach make diÂ®erent things easy.

3.3.12 Exercises

1. In Example 4.3.6 we deÂ¯ned a functor U Â£ U : Mon Â¡ Set. Show that it is

!

induced by a homomorphism of sketches.

2. Prove that MF{2 makes F Â¤ a natural transformation.

3. Prove Proposition ES 3.3.4.

4. Prove Proposition ES 3.3.10.

4

Fibrations

A category is both a generalized poset and a generalized monoid. Many construc-

tions in category theory can be understood in terms of the constructions in posets

that they generalize, so that it is generally good advice when learning about a

new categorical idea to see what it says about posets. Seeing what a construction

says about monoids has not usually been so instructive.

However, certain concepts used to study the algebraic structure of monoids

generalize to categories in a natural way, and often the theorems about them

remain true. In addition, applications of monoids to the theory of automata have

natural generalizations to categories, and some work has been done on these

generalized ideas.

In this chapter we describe some aspects of categories as generalized monoids.

We begin in Section ES 4.1 with the concept of Â¯bration, which has been used

in recent research on polymorphism. One way of constructing Â¯brations is by

the Grothendieck construction, described in Section ES 4.2, which is a general-

ization of the semidirect product construction for monoids. Section ES 4.3 gives

an equivalence between certain types of Â¯brations and category-valued functors.

Section ES 4.4 describes the wreath product of categories, a generalization of the

concept of the same name for monoids; some applications of the construction are

mentioned.

The Grothendieck construction is used in Section ES 5.7. The rest of the ma-

terial is not used elsewhere in the book.

4.1 Fibrations

In this section, we describe Â¯brations, which are special types of functors impor-

tant in category theory and which have been proposed as useful in certain aspects

of computer science.

The next section gives a way of constructing Â¯brations from set or category-

valued functors.

ñòð. 13 |