Although in the examples from geometry and physics the operations are untyped and always reversible, they illustrate that groups, monoids and categories not only are syntactic abstract algebraic structures, but also have a semantic influence. In the latter, the identity is ``do nothing'' and the composition is ``do this, then do that,'' which is clearly associative.
DEFINITION 4.2.1 A covariant action of a group or monoid (M,id,o) on a set A is a binary operation \blank*( = ):MxA® A such that
omitted eqnarray* environment
for all a Î A. Similarly a contravariant action is a binary operation (-)*( = ):MxA® A such that id*a = a and
omitted eqnarray* environment
Usually we treat the star as a unary operation on its first argument, so the abstract arrow f is represented by a concrete function \f*:A® A or f*:A® A such that \id* and id* are the identity on A and
|
A contravariant action of M is the same as a covariant action of Mop, the opposite monoid, cf Definitions 1.3.9 , 3.1.5 and 4.1.1.
A faithful action is one for which things are semantically equal only when they are syntactically the same:
|
EXAMPLE 4.2.2 Let M = (R,1,x) and A be a vector space. Then multiplication of a vector a Î A by a scalar f Î R is an action. Notice that it preserves the (additive) structure of A as well as the multiplicative (and additive) structure of R.
Actions may be used to give the effective definition of a monoid or group.
EXAMPLE 4.2.3 Rubik's cube consists of 27 pieces jointed in such a way that any of the six faces (each with nine pieces) can be rotated through a quarter turn. From the home position, in which each face is uniformly coloured, 212·12!·38·8!/12 » 4.3·1019 positions can be reached. The quarter turns generate a group of this order which acts on the set of components of the cube.
To solve this puzzle, ie to restore a jumbled cube to its home position, you need to know the complicated laws which the generators satisfy. However, if I presented a group with six generators by just giving these laws, without telling you that it acts on this structure, the problem would be more difficult: there is no general algorithm to decide whether the group defined by an arbitrary presentation is finite, or on the other hand whether it is non-trivial. Syntax - the expression of elements of the group as strings of generators subject to laws (``relations'') - gives us very little help in understanding the group. Indeed the structure on which it acts is the only thing we can use to give an explicit description. The semantics gives a kind of tally of the syntax, and then this group may be characterised quite straightforwardly in the language of group theory. The imperative interpretation (Remark 4.3.3) develops the ``tally'' idea.
It was originally thought that the following result, Cayley's Theorem, would eliminate the need for the abstract study of groups.
THEOREM 4.2.4 Every group has a faithful action of each variance.
PROOF: Let (M,id,o) be a group or monoid, and put A = M, ie the underlying set. Then \f*a = fo a and f*a = f;a = ao f define the covariant and contravariant regular actions, respectively. They may be seen to be faithful by considering the effect on id Î A. []
The importance of the result is undisputed, as is shown by the fact that it will shortly turn into a Lemma named after someone else, but the reductionist motive was mistaken. Both the abstract and concrete approaches are needed to complement one another. Indeed, the same group, eg A5 º PSL(2,5) (page 2.2.9), may have two intuitively unrelated concrete representations. Likewise, the beautifully simple but powerful theory of matrix representations of finite groups relies precisely upon considering all such representations. Again this supports the thesis that what mathematical objects do is more important than what they are.
The Rubik cube group was specified by means of its six generators and their action on the cube, from which we could see the laws or relations. The converse process - deriving the concrete form from the laws - is, as we have said, notoriously difficult. As for expressions in Lemma 1.2.4ff, we just have to accept that the equivalence classes can be constructed somehow. In Sections 5.6 and 7.4 we shall examine such quotienting (for arbitrary laws) categorically.
Sketches Let us transfer these ideas from groups to categories, starting with generators and laws.
DEFINITION 4.2.5 A unary theory, L, consists of
We write S for the set of sorts. A free unary theory has no laws.
EXAMPLES 4.2.6 This basic tool has many different names, and it would be instructive to read through the remainder of this section several times, substituting each of the following points of view in turn.
quote omitted diagram environment
A law is a (so-called commutative) (n+m)-sided polygon which has exactly one source and exactly one target (or sink): at every other node there must be just one incoming and one outgoing edge. The target is the type of the term and the source is (the type of) the free variable. Variables are redundant, as is the notion of application: only associative graphical composition of arrows remains. Indeed commutative diagrams are the best way to illustrate unary first order equational reasoning.
When we draw sketches, as for instance in Example 4.6.3(f), we may name several nodes with the same type X. This is to avoid appearing to state unintended laws, where it is understood informally that the polygons which we draw are meant to commute. (This convention is made formal in [FS90], using the puncture symbol \puncture to indicate that an apparent law is not required, though this does not mean that the equation is forbidden in any interpretation.) All occurrences of the same named type X must nevertheless be interpreted by the same set \typeAX.
DEFINITION 4.2.7 A model (also called an algebra, interpretation , representation or covariant action) of an elementary sketch is
PROPOSITION 4.2.9 Every elementary sketch has a faithful covariant action on its clones HX = ÈG \CloneL(G,X). Substitution for the variable defines a contravariant action on HY = ÈQ \CloneL(Y,Q), also faithful.
PROOF: Recall from Notation 2.4.12 that the clone, \CloneL(G,X), is the set of terms of type X in the context G, subject to the laws. In our case G consists of a single typed variable, so we abuse notation by writing G for the type too. A term of type X is a composable string of unary operation-symbols applied to a variable s:G (s for ``state'').
The actions of r:X® Y on Cn(G,X) Ì \HX and Cn(Y,Q) Ì HY are
\r* \an(···\a2(\a1(s))···) = r(\an(···\a2(\a1(s))··· )) Î \CloneL(G,Y) r* \zm(···\z2(\z1(ys))···) = \zm(···\z2(\z1(r(x)))·· ·) Î \CloneL(X,Q)
with s:G, x:X and y:Y; they are faithful by considering the empty strings (n = m = 0). []
Analogously, Definitions 3.1.7 and 3.9.6ff represented each element x of a poset X covariantly as the lower subset X¯ x and contravariantly as the upper set x¯ X. Lists were used to form the transitive closure of a binary relation in Exercise 3.60. We shall postpone the analogue of Proposition 3.1.8 (called the Yoneda Lemma) to Theorem 4.8.12.
EXAMPLE 4.2.10 The Lindenbaum algebra (Example 3.1.9) gives the regular representation of propositions. For types this is the term model.
Convention 4.1.2, that juxtaposition means application on the left, is clearly not very appropriate for unary theories. Many algebraists, in group theory in particular, apply functions on the right, and abstract this to composition without any sign; this is unambiguous in that subject because the language is first order and strongly typed. As we shall soon be passing on to many-argument and higher order languages, we shall put up with the earlier convention.
This interpretation is sound: the semantics obeys the rules specified by the syntax. It is also complete: any two terms which are semantically equal may be proved to be so using the given rules, because we only made them equal when the rules said so; this is what faithful means.
Generating a category A faithful action can be used to represent a category concretely: the object X is the set \typeAX and maps f:X® Y are those functions (``homomorphisms'') \typeAX® \typeAY which arise as actions. In the case of the Cayley-Yoneda action, we shall characterise them intrinsically in terms of naturality in Example 4.8.2(f).
The category obtained from an elementary sketch via its action has the same objects as the sketch. The maps of the category are composites of those of the sketch. In the case of a free unary theory, the maps are lists (Definition 2.7.2) of generators, though we postpone the proof to Theorem 6.2.8(a). With laws, they are equivalence classes of lists.
Since the action is faithful, the only equations amongst maps are those provable from those given in the sketch plus the axioms for a category. Lemma 1.2.4 gave the preorder version of this construction; recall that it made objects interchangeable (isomorphic), but didn't pretend to make them equal.
LEMMA 4.2.11 The hom-set \CloneL(X,Y) in the category is the clone of the same name. The identity \idX is the variable x:X qua term, and composition is substitution, which is associative. []
The category saturates the sketch by adding into \CloneL(X,Y) all derived operations of type Y (these are just composites in the unary case, cf the reflexive-transitive closure of a relation), and making all provable identifications amongst them. To sum up the precise relationship,
THEOREM 4.2.12 Every elementary sketch presents a category, and conversely, any small category C is presented by some sketch L in the sense that C º \CloneL. We write \qqdash for this isomorphism and call the sketch L = L(C) the canonical elementary language of C ( cf Proposition 3.9.3). It is defined as follows:
using \qq X and \qq f to distinguish the linguistic sorts and operation- symbols from the objects and morphisms of the original category. []
We are accustomed to writing languages in alphabets of 26 or maybe 128 enumerated symbols, but for this construction we need a ``letter'' for each object and morphism of C. Questions such as whether we can distinguish between letters or form a dictionary of the words now arise, to which one answer might be a severe restriction on the applicability of this result. This is not the line which we follow, but the issues deserve separate consideration , which we defer to Section 6.2.
The notion of sketch interpolates between those of oriented graph and category: it mentions some composites, where the extremes require none or all of them. For a category, the representations of an object X given by Proposition 4.2.9 reduce simply to ÈG C(G,X) and ÈQ C(X,Q), where we no longer have to form explicit composites.
The geometrical interpretation shows that unary theories have an input-output symmetry. This is broken by the term calculi of the richer type theories, but the closer analogy is retained if we consider programs or substitutions instead. By examining the covariant and contravariant actions of the latter, we shall next give a construction of the category of contexts and substitutions which is directly applicable to a very wide class of formal languages. The use of sketches to do this is new.
This section has shown how categories can present combinatorial data in algebra, topology and logic. The proofs are not complicated, but nor are the ideas trivial or immediately grasped: you should go back and use them to express any familiar examples as a category. This is important because our account of substitutions and hence the semantics of type theory depend on it.