by Charles Wells     Last revised 2015 1130     Charles (at) abstractmath.org

Introduction

A form is a kind of generalized sketch that I introduced in [GenSk].   The most detailed description of forms is in [GBLS].  Reading this introduction might help you work your way through that paper.

A sketch (invented fifty years ago by Charles Ehresmann) is a mathematical structure designed for specifying a type of mathematical structure.  Sketches are described briefly here and in detail in references [CTCS] and [TTT]. A form is an abstraction of the concept of sketch. Forms also specify kinds of mathematical structures, and they can specify more kinds of structures than sketches can [LimSk].  In a sense, a form is a kind of sketch of a sketch.

I will sneak up on the idea of sketch using the specification of directed graphs as an example.

Directed graphs

This picture shows a directed graph.   A graph theorist might call it a directed multigraph with loops.  

What makes it a directed graph is that it has some nodes (x, y, z and w in this case), some arrows (a, b, c, d, e, u), and each arrow has a source and a target; for example, the source of c is z and its target is x. That information completely determines the structure of a directed graph.

The picture has lots of extraneous information irrelevant to the structure, for example the placement of the nodes.  This extraneous data may make it easier to see the structure but is not part of the structure of the directed graph itself. 

You can denote the set of positive divisors of 7 by {1,7} or by {7,1}; in either case it is the set whose elements are exactly 1 and 7 and nothing else.  Whether the 1 or the 7 comes first inside the braces is not relevant.  It is interesting that most notation systems for mathematical object has properties that are irrelevant to the structure denoted -- even the notation for a two-element set.  This introduces noise in the required pattern recognition process.

The statement in blue above is an informal definition of  "directed graph" written in mathematical English.  This definition determines a type of mathematical structure.  You could go on and say that a morphism of directed graphs must take nodes to nodes, arrows to arrows, and preserve source and target. For example, a morphism  f from the directed graph in the picture to some other directed graph must satisfy the requirements that the source of f(c) must be f(z) and the target must be f(x).   Thus the two statements in blue define a category of directed graphs.

There are other ways to define morphism of directed graphs; for example, you can allow an arrow to go to a node.  That category of directed graphs can also be sketched.  So can undirected graphs.  [GMG]  gives a survey of these concepts.

About definitions

The definitions in blue require experience in reading mathematical prose and fairly sophisticated pattern-recognition to determine that they are definitions and to determine just what requirements they impose for an object to be a directed graph.   This is discussed in detail in abstractmath.org.

Both the definitions in blue could be made more formal.  They could be clearly marked as definitions and the example remarks could be segregated into another paragraph.  For example:

Definition. A directed graph consists of two sets A, whose elements are called arrows, and N, whose elements are called nodes, and two functions  and .

This formal definition is still a piece of mathematical English.  It still requires pattern recognition to extract the mathematical content.  But what is the mathematical content of a definition? Both mathematical logic and sketch theory provide (different) answers to this question:  Both provide a mathematical object that determines a type of structure.

First-order theories

A  first-order theory is a mathematical structure that specifies a type of mathematical structure.  It provides a mathematically defined system of symbols, expressions and formulas that determine a type of structure, along with a set of rules that determine which sets-with-structure are of the desired type, in other words are models.  The expressions and formulas are strings of symbols defined recursively and subject to axioms.

As an example, the theory for directed graphs could contain two types (node, arrow), a set of variables of each type, two unary function symbols s and t, and some production rules such as: "If a is of type arrow, then s(a) is a well formed term of type node."    (You could also use a single-sorted theory, with predicates that say whether an object is a node or an arrow.)  A model of this theory (in the category of sets) must consist of two sets and two functions between them.

This theory is a mathematical object. The fact that first-order theories and their models are math objects allows you to prove theorems such as the Löwenheim-Skolem Theorem (every finitary first order theory that has an infinitary model has non-isomorphic models, which is where you get non-standard integers).

The details about first order theories are spelled out in the Stanford encyclopedia entry.   Wikipedia has a list of first order theories of common structures such as groups and (undirected) graphs. 

A first order theory could be described as a mathematical object consisting of strings of symbols subject to certain axioms, along with rules describing what models must be.  Thus it takes a formal definition in Mathematical English, such as the definition of directed graph given above, and models it as strings, in the same way we might model the flight of a cannonball as a parabola.  (This is a different use of the word "model" from the meaning of model of a first order theory.  Abstractmath.org has a discussion about the various uses of the word "model".) 

Because of this, it makes sense to say that a first order theory is a string-based specification of a type of math structure.

Sketches

A sketch is a graph-based specification of a type of mathematical structure.  The sketch for directed graphs is shown at the right.  It is itself a graph, which is confusing.  Get used to it. 

A model M of this sketch in a category  consists of objects  and   of  and morphisms  and   of .

Thus a model in the category of sets is both of these things:

·     A particular directed graph.

·     A functor  from the sketch to the category of sets.

A functor from a directed graph into a category is defined in the same way as a functor from a category into a category, except that there are no composites or identities to preserve. 

A morphism of models of this sketch from  to  is a pair of functions   and    for which these diagrams commute:

If you chase these diagrams you will discover that they say both these things:

• 
  
   is a morphism of directed graphs.
• 
  
   is a natural transformation from
  
    to  
  
  .

That is a start on understanding sketches: Models are functors and morphisms between models are natural transformations.

Specifying more kinds of structure

Groups, small categories, fields and many other structures are models of sketches.  To show how that happens, I have to say how to sketch binary operations (to define groups), how to impose equations (to state the associative law), how to define equalizers (so I can say how to define composition when the domain of one morphism equals the codomain of another) , "not equals" (so I can say  ), and many other things.  Many examples of sketches may be found in [TTT] and [CTCS].

We can go further and sketch special kinds of categories (cartesian closed, toposes, and others) which we will need to do to create forms with more power than sketches. 

The sketch for an endofunction

Let  be the graph above. It has one node c and one arrow s, whose source and target are (necessarily) c. A model of this sketch is a set C and a function from C to itself. Any such function determines a cyclic semigroup of transformations of C. One particular model is the one in which in which C is the set of natural numbers and s is the successor function: this is the free semigroup on one letter.

You may want to experiment with other graphs as sketches. Any graph produces a category of models in sets. Each such category is a category of presheaves, hence is a topos ([TTT], p. 67, Theorem 2.4).

Imposing equations

We need to expand the idea of sketch to be able to define more kinds of structure. Let’s start with equations. Suppose we take the sketch for an endofunction and want to modify it so that  in every model in Set. This means we must require that the diagram (in the category of sets) below commute for every model M.

To say that this diagram is commutative (or commutes) requires that  .

·       This use of the word "commutative" is distinct from the meaning of the word in algebra. 

·       Saying exactly what “this diagram is commutative” means for any particular diagram requires fussiness. Chapter 2 of [GBLS] goes into excruciating detail about this.

The obvious way to do this is to say that we require a model to be a functor from the graph  to the category of sets that has the property that the image of the diagram

under M is a commutative diagram in the category of sets. We say that this diagram is formally commutative. In general, in sketch theory, something is formally P if in every model of the sketch its image is required to be P.

To say that the diagram itself is commutative is meaningless.  It is a diagram in a graph, which has no notion of composition of arrows. 

This gives us a more general notion of sketch which allows the specification of equations, although so far only between unary operations. Formally, a linear sketch  consists of a graph G together with a set  of zero or more formally commutative diagrams. It should be apparent that an linear sketch can specify anything that a universal algebra signature with only unary operations can specify.

Models in arbitrary categories

A model in Set of a linear sketch  is a graph morphism  with the property that M takes every diagram in D to a commutative diagram in Set.  

This definition would still be meaningful if we replaced  by any category whatever. So now we can talk about a model of  in any category C. For example, a model in the category of groups of the endofunction sketch above that requires the cube to be the identity function is simply a group with a specified automorphism of order 1 or 3. Indeed, in any category of structures of a certain type, a model is a structure of that type with a specified automorphism of order 1 or 3.

The more elaborate sketches we construct later will still allow models in any category. For example, a model of the sketch for groups (see [TTT] starting on page 126) in the category of Hausdorff spaces is precisely a Hausdorff topological group.

Ancient cute theorem: A model of the sketch for groups in the category of groups is an Abelian group. That’s because the group operations must be homomorphisms!

Clones and theories

Sketches as I have described them so far can now describe some kinds of universal algebras, namely those with unary operations and equations.  n-ary operations and more elaborate constructions will come later.

The first big construction in universal algebra is that of the clone of a type of algebra (commonly called a signature): a specific set of n-ary operations for various n and specific equations involving those operations.  The clone is essentially all the expressions you can create from the operations, requiring two expressions to be equivalent if you can prove they are equivalent given the equations of the algebra. 

For example, in the clone for groups, x(y(xy)) is equivalent to (xy)(xy).  On the other hand, xy is not equivalent to yx because there are noncommutative groups, so xy = yx can’t possibly follow from the equations.

The Lawvere theory of the algebra is a different construction which essentially expresses the clone as a special kind of category, with models of the theory being product-preserving functors.

In model theory a first-order theory is an extension of the concept of clone that allows relations other than equality, as well as the use of negation and quantifiers.  First order theories are constructed in a different way from clones and Lawvere theories but they capture the same general idea in the bigger context.

The cattheory of a sketch

For a sketch, the idea equivalent to the clones and theories just described is that of a cattheory. (This is a new coinage.  See Terminology below.)

Suppose we have a linear sketch  where G is a graph and D is a set of formally commutative diagrams.  The cattheory of the linear sketch, denoted by , is the free category generated by G with the condition imposed that the diagrams in D must become commutative.  The graph morphism  that takes the nodes and arrows in G to the corresponding objects and arrows of the free category is by definition a model of the sketch . G is called the generic model of the sketch.

A model of the cattheory  in a category  is simply a functor .  We don’t have to impose properties on the functor because functors automatically preserve commutative diagrams.  When we get into more complicated structures we will have to add preservation requirements on the model functor. 

The category of models of the linear sketch  in a category  is denoted by .  The category of models of the cattheory  in  is denoted by .  By definition of "free", any model  induces a unique model  for which . 

I defined a model of  in  as a graph morphism , but in the previous paragraph I referred to a model .  This is the standard abuse of notation used everywhere in math: Deliberately not distinguishing a structure from its underlying set.  (See "abuse of notation" in Wikipedia and in [Hbk].)

The cattheory has this universal property:

Theorem The map

is an equivalence of categories.

This theorem forces the cattheory to be determined up to natural equivalence of categories that commutes with the generic model.  For all practical purposes, a model of the sketch is thus the same thing as a model of its cattheory.  This will remain true as we go up the hierarchy of new constructions (n-ary operations, limits and colimits, and other things) and is the defining property of the cattheory.   Clones, Lawvere theories and first order theories are all cattheories up to equivalence.

How to think about cattheories

  may be thought of as the minimal category that contains a model of , the model being the generic model G. Every model M of  in any category  must induce a unique (up to natural isomorphism) model of  in , simply because everything in  must be there because any category containing a model of  must have everything in .

For example, consider the sketch for endofunctions above.   Because s is in the graph of the sketch, every power of M(s) must be in any category  containing a model M of the sketch.  This forces by induction a unique functor M' from the cattheory of the sketch to (Usually the induced functor is unique only up to natural isomorphism, but this time it is rilly rilly unique.)

Terminology

The remarks in this section apply in general to all kinds of sketches, not just the restricted version we are considering here.

The situation in the literature is confusing.

• In [TTT] and in the other books and articles by Michael Barr and/or me, we call the cattheory the theory.
• In [GBLS], Atish Bagchi and I refer to the cattheory of a finite limit sketch as a theory or as a categorial theory in an attempt to distinguish it from some version or other of logical theory.  We said “categorial theory” instead of “categorical theory” because the latter phrase means something different to logicians.  Unfortunately, “categorial” means something different to linguists!
• In [SkEl], Johnstone calls the cattheory of a sketch the syntactic category.
• In [GBLS], page 33, we refer to SynCat[ f ], where f is a form (generalized sketch).  Now f has a cattheory, but it is not SynCat[ f ], which is the cattheory correspond to the doctrine that f belongs to (the type of categories it can have models in.)

I am using “cattheory” so that I will have a neologism that doesn’t mean anything different to anybody.  Personally, I think we should keep using “theory”, because the theory (syntactic category in the sense of Johnstone) is ultimately the same thing (satisfies the same universal property) as the corresponding logical theory; the difference is only in the construction.

Products

A (binary) product diagram in a category is a cone to {a,b}, in other words a diagram that looks like this

(1)

with this specific universal property:  For any other cone to {a,b},

(2)

there is a unique fill-in arrow fi such that this diagram commutes:

(3)

This diagram has been called a sawhorse. But like most metaphors in math, this name is misleading. 

How to think about the sawhorse

1. The sawhorse is not symmetrical with respect to its two pairs of legs.  The black (right) legs form a product cone but the blue (left) legs need not be a product diagram. It could be called a directed sawhorse.
2. The construction of the fill-in arrow is like an algebraic operation whose domain is the set of diagrams of the form (2) for a fixed product diagram (1)  and whose output is the fill-in arrow.   Now ordinary algebraic operations have domain some cartesian product of sets with output in a set.  For example scalar multiplication of a real vector space is an operation .  The fill-in arrow is an operation on a set of tuples of arrows, but the domain is not the cartesian products of arrow sets; instead it is an equationally defined subset of a cartesian product of arrow sets (the equation says that the source of one must match the product of the other).
3. The colors in the sawhorse correspond to the quantifiers in the definition of the diagram:  Given a cone from x to {a, b}, then for any other cone from any object y to {a,b}, there is a unique fill-in arrow fi from a to b such that the sawhorse commutes.
4.  By making the blue cone also a product diagram you get an instant proof that the resulting fi is an isomorphism, in fact the only isomorphism making the sawhorse commute.  Thus "products in a category are determined up to a unique isomorphism".

Chapter 5 of [CTCS] gives a detailed explanation of products in categories at a rather elementary level.

Finite products

Finite products  products of a finite number of objects in a category -- can be define analogously.  However, if you assume you have all products of two objects then you automatically get all finite products of two or more elements.  It is an easy exercise to see that every category has all products of one object.  A product of no objects is a terminal object and that has to be assumed separately.  Not all categories have a terminal object, for example the category you get if the singleton groups and the arrows to and from them are untimely ripp’d from the category of groups  it has all products of finite nonempty sets of objects but no terminal object.

A category has finite products if there is a product diagram for any finite set of objects.

FP sketches

An FP sketch is a graph together with some  specified formally commutative diagrams and some specified formal product diagrams.  A model of an FP sketch in a category  is a functor from the graph to  that takes the specified formally commutative diagrams to commutative diagrams and the specified formal product diagrams to product diagrams.

The category of all algebras for any specified type of universal algebra (with finitary operations) is  equivalant to the category of models of an FP sketch.  Chapter 4 of [TTT] describes an FP sketch for the category of groups starting on page 126.

On the nose

The homomorphisms in the category of models of an FP sketch must preserve the designated product diagrams on the nose.  For example, the sketch for groups just mentioned has three designated formal product cones, for the terminal object, for  and for .  The formal binary operation is an arrow .  "On the nose" means that in a model the binary operation must have domain the exact copy of  that is the value of the model at  .  This is just a technicality,  although some mathematicians make a big deal out of it.  In fact when mathematicians talk about the “category of groups” they never say which product cone they mean by  and .

Finite Limits

Review: a cone to a set  of objects of a category consists of an object v of the category and one arrow from v to each object in .  A finite-product diagram is a cone to such a (finite) set with the unique fill-in property. 

Now suppose we have a finite diagram  in a category.  I am specifically not assuming it is commutative.  A commutative cone to  is an object v, an arrow(called a projection) from v to each node of , with the additional property that each triangle formed by two projections and an arrow of the diagram must commute.  The diagram  is called the base diagram of the cone.

Example

Here is an example of a base diagram:

(a)

A commutative cone over this base will look like the left diagram below.  The three arrows with source P are the projections.

Since the triangles involving two projections have to commute, the diagonal projection is determined by the other two.  For this reason, this particular example is almost always drawn as on the right.  It is called a pullback diagram.

Two other examples

In each case all the projections are shown on the left and only the necessary ones on the right.

(b)

(c)

Limit cones

A limit cone over a diagram is a commutative cone over the diagram with the same unique-fill-in property that product cones have.  For example if this is a limit cone over diagram (a) above

(d)

and the blue arrows on the left below also form a commutative cone over the same base, then there must be a unique fill-in arrow making everything commute in the diagram on the right.

This particular shape (d) of limit cone is called a pullback diagram. A limit cone in the shape of (b) is an equalizer diagram. It turns out that if you assume that if all pullbacks and equalizers exist, then you have limit cones over every finite diagram for free.  Limit cones of shape (c) don’t have a common name but they will be referred to later.

Since a finite set of objects is just a finite diagram with no arrows, product diagrams are a special case of limit diagrams.  The commutativity requirement is then vacuous.

A category has all finite limits is called an FL-category.  From the remark in the previous paragraph, an FP-category is automatically an FL-category; the diagrams in  have nodes but no arrows.

An older name, which is deprecated, is left exact category.

FL-Sketches

An FL sketch (finite-limit sketch) is a finite graph  with a finite set  of finite formally commutative diagrams and a finite set  of formal limit cones over finite diagrams (which are not usually among the formally commutative diagrams.)

A model of an FL sketch in an FL category  is a graph map into the (underlying graph of) the FL category that take the diagrams in  to commutative cones and the cones in   to limit cones.

The category of models of the FL sketch  in an FL category  is denoted by .

FL cattheories

The FL cattheory of a linear sketch  is a category   together with a  model  with the the property that for any model  of  in a category , there is a unique model M' of  in  such that

commutes.  G is the generic model of .

The category of models of the cattheory in  is denoted by .

The cattheory has this universal property:

Theorem The map

is an equivalence of categories.

(Compare the corresponding theorem for linear categories.)

This theorem forces the cattheory to be determined up to natural equivalence of categories that commutes with the generic model.  For all practical purposes, a model of the sketch is thus the same thing as a model of its cattheory.

FL-sketches and forms

The first key to understanding forms is that all sorts of interesting kinds of categories (cartesian closed, toposes, symmetric monoidal) are models of FL-sketches.  Indeed, I expect (but haven't proved) that every kind of n-category that anyone ever defined is a model of an FL-sketch  it doesn’t require anything that might be called “n-sketches”.  However, they will have the same problem as ordinary categories in that in the category of models the structure has to be preserved on the nose.  In the case of FL-sketches for different kinds of 1-categories, the sketch’s model category is equivalent (but not isomorphic because of the nose problem) to the usual way we define categories of that kind of category.  What “equivalence” means for “every kind of n-category” is referred to in [nLEquiv].

Constructing FL cattheories

The linear cattheory of a linear sketch is just the free category generated by the graph of the sketch, with the formally commutative diagrams forced to be commutative.  It is more complicated to prove the existence of the FL cattheory of an FL sketch.  Once you do show it exists, it follows easily from the definition that it is uniquely determined up to equivalence of categories.

There are two approaches to showing the existence of the FL cattheory.

As a fixed point

Introduce an operator on categories that adjoins diagrams that in effect add limit cones to finite diagrams that don’t already have limits.  This is done in lots of detail in sections 4.2 and 4.3 of [GLBS].  Starting with an FL-sketch  , the cattheory   is the minimum fixpoint of this operator.

This is the computer-sciencey way of doing it.  Each arrow and commutative diagram in the theory is constructed explicitly. When [GLBS] constructs proofs, this step-by-step construction corresponds to the inductive construction of formulas and rules of inference in classical string-based logic.

Embedded in a functor category

Given an FL sketch , the category   of models of  in the category of sets turns out to be a full reflective subcategory of the presheaf category  .

Let’s spell out what this means: the models are finite-limit-preserving functors and the presheaf category contains all functors.  The reflectivity means that the embedding has a left adjoint, which implies that a limit of a diagram in the model category is also the limit of the diagram in the presheaf category.  The fullness means that every natural transformation between models is a morphism of models. Using these facts you can get an embedding of    in  ;  is then the full FL subcategory generated by the image of the embedding.

This is worked out in detail for the FP case in [TTT], Chapter 4.3.  The construction is then carefully described for the FL case  in Chapter 4.4, but the proof is omitted.  It is quite analogous to the FP case.

I have been focusing here on the FL case because that is the foundation of the construction of forms in [GBLS].

FP Sketches

An FP sketch  and its FP cattheory are defined in the same way, except that the finite diagrams that the cones are over have to be discrete, and it has properties analogous to those for FL sketches given above.  Note that any FP sketch or  linear sketch will also have an FL cattheory.

The sketch for categories

FL sketches (finite-limit sketches) makes it possible to construct a sketch for categories. To do this you need some nodes:

, which in a model will become the set of objects --  so in our "formal" terminology  is the formal set of objects.  (This terminology, by the way, is due to John W. Gray.)

, the formal set of arrows.

, the formal set of composable pairs of arrows.

, the formal set of composable triples of arrows, needed to state the associative law.

It needs many arrows, some of which are:

 that formally picks the identity arrow of an object

 that formally pick the source and target of an arrow.

 that formally picks out the composite of a pair of arrows.

...as well as many structural arrows that, for example, pick out the first arrow in a composable chain, or that picks out the pair of arrows  given a composable triple.

Cones and diagrams

Of course, you can’t just say that    is the formal set of composable pairs of arrows.   What you must do is produce a cone that forces it to be that formal set, in other words forces it to be the set of composable arrows in a model.   And here it is:

(The blue arrows are the projections, the black objects and arrows form the base diagram.  Note that the middle blue arrow is superfluous.  If you drop it, you may recognize this as an ordinary pullback diagram.)

You need an analogous cone for  and diagrams for associativity and to make the identity arrows behave right.  The details are in [GLBS], chapter 7.

In a model M, the elements of  are diagrams that look like this:

This green diagram is in the model (semantics), and the cone above is a diagram in the syntax. You have to make the distinction constantly in this subject. This is remarkably annoying. To help, I am systematically putting objects of the category-that-is-the-model in green, and cone projections in blue.  Black and blue means syntax,  green means semantics.

Remarks

 is the domain of the composition arrow .  So defining categories requires more subtlety that defining an ordinary algebra, where the domains of the ops are always cartesian products:  this domain is an equalizer.  To sketch categories requires the full power of finite limits, not just finite products. Of course, that last sentence does not follow from anything I have said, since there might be a rascally way to use only finite products.  But there isn’t: the category of small categories is not regular (Exercise 6, page 278, of [TTT])  but any category of multisorted universal algebras (which are the same thing as models of FP theories) does have that property: see [TTT], section 8.4.

Nevertheless, the category of models of an FL sketch always has all sortwise limits and all sortwise filtered colimits. in particular initial algebras. 

Constructing a particular kind of limit or colimit sortwise means that it is constructed sort by sort.  For example, if always , then the category of models has sortwise products.  In most of the references the name “pointwise” is used.

Categories with structure

Many categories with particular properties can also be sketched with FL sketches.  These include

• Categories with finite limits
• Cartesian closed categories
• Toposes
• Symmetric monoidal categories
• Abelian categories

Sketch for categories with finite products

A category has finite products (is an FP category) if it has terminal objects and binary products.  GBLS describes the construction of the FL sketch for categories with finite products in section 7.3, which spells out how you sketch the set of terminal objects and the set of binary product cones.  I will give a more detailed discussion of how to do binary product cones here and introduce the annotation notation we use.

Syntax and semantics

We must distinguish between two things:

• The FL sketch for FP categories
• The models of the FL sketch for FP categories, which are FP categories. 

A diagram in the FL sketch will be in black (the color for syntax) and a diagram in a category with finite products will be green (the color for semantics).  In both syntax and semantics, projection arrows may be blue and arrows that exist uniquely (fill-in arrows) may be red.

Product diagrams

A product diagram in an FP category looks like this:

(Diagram )

But a diagram can look like that without being a product diagram. You have to say that it is a product diagram.   This means that for any cone to the same pair of objects

(Diagram )

there is a unique arrow h making this diagram commute:

(Diagram F)

FL sketch for FP categories

To get the FL sketch for FP categories, you start with the sketch for categories and add some objects and arrows.  The ones listed below are the objects and arrows needed for sketching the set of binary cones and finite-product cones.  Others are needed for the terminal object (much easier and not done here).

Objects

, the formal set of cones of the form .

, the formal set of fill-in diagrams (diagrams of the form of F above).

Arrows

, that picks out the product cone over a pair of objects.

, that picks out the source cone of a fill-in arrow.

, that picks out the target cone of a fill-in arrow.

, that takes a cone to the unique fill-in diagram that has the cone as source cone.

 that formally picks out the fill-in arrow in a fill-in diagram.

Specification for the formal set of cones

The FL sketch for FP categories contains this limit cone, which requires that the two arrows in a cone have the same source. Note that I have named the projections lproj and rproj.

(Diagram ConeSpec)

Annotations

This cone is annotated according to a system that is spelled out precisely in [GBLS].  The annotation of this diagram refers to cone  above.  Some perspectives on this situation:

1. The annotations allow you to chase the diagram.  For example, if  is a member of the set of cones of a model, then  and .  In the preceding sentence, I use abuse of notation:  The sentence should say that  and that .
2.  is being used as the shape graph (see [GBLS], 2.3) for ConeSpec.
3. The annotation is a section of the model thought of as a sheaf.

Specification for the formal set of fill-in diagrams

This much more complicated annotated limit cone defines :

I completed the annotation compared to the version in GBLS, whose partial annotation generates the rest.  The three projection arrows shown generate all the others, not shown to avoid clutter.

Some notes and examples:

1. It is worthwhile checking through the conditions to see that this limit cone really does specify fid.  If you do, you will see the sketch needs a couple of commutative diagrams, found in GBLS, 7.3.2.
2. The whole diagram is commutative because of the diagrams just mentioned and the commutative diagrams of the FL sketch for categories mentioned above (and described completely in GBLS 7.2).
3. This diagram is symmetrical in spirit, with one exception: The arrow prod breaks the symmetry because there is no corresponding arrow going upward.  This reflects the fact that a fill-in diagram is not symmetrical: The right hand cone is a limit cone but the left hand cone is not.
4. I suspect that the diagram could be drawn in a way that is really symmetrical (geometrically) in three dimensions (or four?), except for the break mentioned in (3).

Cartesian closed categories

A Cartesian closed category is a category with the following structure:

• has binary products.
• For each pair of objects A and B of , there is an object and an arrow .   is an exponential object.
• For each triple of objects A, B and C of , there is a map such that for every arrow , the diagram below commutes:

(lameval)

• For any arrow , .

It follows that  is a natural isomorphism of homsets.

Currying

Going from  to  is called currying or partial application. You can curry a multivariable function all the way down to a constant.  The inverse process is usually called uncurrying.   It constitutes getting rid of entries in the codomain of a function that are function spaces by adding variables to the function. I suggest using blanding instead of “uncurrying”.

The FL sketch for cartesian closed categories

The FL sketch for CCC’s (which I will call CCCSk) is spelled out in detail in [GBLS]. I will mention some of the constructions here.  I will use many of them in the next section to give an example of a form.

Objects and arrows

The complete list is spelled out in Sections 7.2 and  7.6 of [GBLS].  Here I mention

 that formally picks out the identity arrow of an object.

, the formal set of functions of two variables, in other words arrows of the form .

 that picks out the arrow  itself.

 that picks out the source  of a two-variable function .

, the formal set of curried functions from .

 and  that pick out the source and target of a curried function .

 that picks out the function space  of two objects  and . 

, the formal set of composable pairs of arrows in the FL sketch for categories, defined by this pullback diagram: 

(Ar2Def)

For the purposes of the example below, I need  as defined by this diagram:(Bsource)

In an object-oriented program built on this work, this would be a derived method..

One of the limit cones in CCCSk defines  and in particular gives  the properties it needs:

(Curry)

The formally commutative diagram below should have been included in the FL sketch for categories in Section 7.2 of [GLBS].   It gives the composite of a composable pair the right source and target.

(Compreq)

Representing reflexive function spaces

An object  of a cartesian closed category is reflexive if there are arrows  and  such that

(ret)

commutes.  That means   is a retract of .    is called  a reflexive function space.  Reflexive function spaces are the theoretical basis for programming languages which have functions as first class objects.

So a sketch for RFS’s would be defined by a limit cone over  the diagram below.  I have always shown the cones in blue before, but GBLS does not show cones at all, and it isn’t necessary to show them.

(ReflFSConeBase)

To specify a reflexive function space you would have to give  an object  and two arrows  that satisfies Diagram (lameval) above, so the mandatory projections would be to ,  and .  The projection to  is induced by Diagram (Curry) above, the projection to   by Diagram (Ar2Def), and the projection to  follows from the fact that it is the vertex of the product cone shown.  The other projections exist by composition.

Let's call the vertex of this cone rfs for "reflexive function space".  Note that all the objects and arrows in this diagram exist in the FL sketch for cartesian closed categories.

Now you can check (or forget all the constructions above and just Put Your Hands On The Monitor And Believe) that in a model  of the FL sketch for CCC’s,  would be the set of reflexive function spaces together with specified inclusion  and retraction .

Non-surprise: In any model of the FL sketch for CCC’s in the category of sets, will be the empty set. It is well known that for any set   the function space  has cardinality properly bigger that the cardinality of , so there can be no inclusion of  into .

Nevertheless,  is a perfectly well defined set.  It just turns out to be empty.

Forms

Forms are defined formally in [GBLS].  Here I will provide a form for reflexive function spaces as an example. In such a way that you get an informal definition of form.

Some terminology:

Constructor space

The sketch CCCSk for cartesian closed categories is a constructor space. A constructor space must be an FL-sketch that “contains” and is “generated” (see [GBLS], Chapter 6.1) by the FL sketch for categories, and indeed CCCSk is built from the FL sketch for categories by adjoining some objects and arrows, cones and commutative diagrams that all exist already in the FL Cattheory for categories.  So a constructor space  has models we can call  C-categories. In particular a model for CCCSk in sets is a cartesian closed category. 

We can identify the constructor space  as a doctrine.  For example, the doctrine of equational theories (FP sketches) is the constructor space for categories with finite products, and the doctrine of cartesian closed categories is CCCSk.  (I believe, without having thought about it enough, that this definition of doctrine is spiritually the same as Beck's definition of doctrine.)

Form

For any constructor space , take an object  in the FL Cattheory of    and adjoin a new arrow  where 1 is the terminal object.    is what we call a C-form and  with   as a freely adjoined arrow is called  .

A "model of a -form in a C-category “  means that contains a model of .  This means that in  ,  is nonempty.

The CCC-form for reflexive function spaces is then a global element of the node  of CCCSk as constructed above for some CCC.  There are no models in the category of sets, but there are many toposes (and many other CCC’s) that do have models, as in domain theory.

More about a model of a form

Sketches are forms, in this sense:  If you have a sketch   in some doctrine  (for example, a finite-limit sketch), the sketch consists of a graph with some diagrams, cones and cocones.  There is a node S in the FL-Cattheory of finite-limit categories each of whose elements in a model of S (in other words in an FL -category) will be such a sketch.

Example: The FP sketch for magmas

A magma is a set with a binary operation defined on it.  It does not have to be associative or commutative or anything. 

In the FP doctrine, the sketch for magmas consists of objects  and , arrows

and one cone

(Cone1)

and nothing else.  The FP-Cattheory for this sketch is (equivalent to) the Lawvere theory of magmas.

The FL-Cattheory FPSk for FP categories contains a node whose inhabitants in any model of FPSk  (in other words in any FP-category) are all such sketches (objects, arrows and the cone).   This means that the FP sketch for magmas corresponds to an FP-form.  In this way you can see that all sketches in Ehresmann’s sense are forms in my sense.

This node can be constructed as the limit  of a cone over a diagram in FPSk.  You have to make the diagram become a description of the objects, arrows and cone above, using the arrows in the constructor space FPSk. For example , ,  and others, and including formally commutative diagrams that say for example that Cone1's projections go to the same object (using  and }.   Adjoining a global element to this limit node will result in an FL-category  which contains FPSk along with that global element.

So a model of the form for magmas in an FP category  is a model of  for which the model of the underlying cattheory FPSk is ; in other words it is the category   with a distinguished element f of the node .  That distinguished element is a particular diagram and cone like the ones shown above for a particular object  (because the projections onto  include a particular projection to   That object  with the arrows corresponding to ,  and  is a particular magma, a model of the sketch for magmas given above.

The paper [LimSk] contains two other examples of forms, the form whose models are categories with subterminal objects, and the category of groups with morphisms restricted to those that preserve centers.  Neither of these categories can be sketched.  They both use a "Universal Quantifier Constructor", and so have models in toposes.

Acknowledgments

Thanks to Toby Bartels for corrections and suggestions.

References

[GBLS] Atish Bagchi and Charles Wells, Graph-Based Logic and Sketches, draft, September 2008, on ArXiv.

[MSk] Michael Barr, Models of sketches (1986). Cahiers de Topologie et Géométrie Différentielle Catégorique, 27:93-107.

[LimSk] Michael Barr and Charles Wells. On the limitations of sketches (1992). Canadian Mathematical Bulletin, 35:287-294.

[CTCS] Michael Barr and Charles Wells, Category Theory for Computing Science (1999). Les Publications CRM, Montreal (publication PM023).

[TTT] Michael Barr and Charles Wells, Toposes, Triples and Theories (2005). Reprints in Theory and Applications of Categories 1.

[GMG] R. Brown, I. Morris, J. Shrimpton and C. D. Wensley.  Graphs of morphisms of graphs, 2008.

[Mgm] M. Hazewinkel (2001), “Magma“, in Hazewinkel, Michiel, Encyclopaedia of Mathematics, Kluwer Academic Publishers, ISBN 978-1556080104

[SkEl] Peter T. Johnstone, Sketches of an Elephant: A Topos Theory Compendium, Volume 2 (2002). Oxford Logic Guides 44, Oxford University Press, ISBN 978-0198524960.

[KPT] Yoshiki Kinoshita, John Power, and Makoto Takeyama. Sketches (1997). In Mathematical Foundations of Programming Semantics, Thirteenth Annual Conference, Stephen Brookes and Michael W. Mislove, editors. Elsevier.

[nLEquiv] n-Labs, Equivalence of categories.

[PHLCC] Palmgren, E and Vickers, Steven (2006) Partial Horn logic and cartesian categories. Annals of Pure and Applied Logic, 143 (3). pp. 314-353. ISSN 0168-0072

[FEAS] A.J. Power and Charles Wells. A formalism for the specfication of essentially algebraic structures in 2-categories (1992) Mathematical Structures in Computer Science, 2:1-28.

[FDDT] Charles Wells and Michael Barr, The formal description of data types using sketches, in Mathematical Foundations of Programming Language Semantics, M Main, A Melton, M Mislove, and D Schmidt, editors. Lecture Notes in Computer Science 298 (1988).

[GenSk] Charles Wells. A generalization of the concept of sketch (1990). Theoretical Computer Science, 70:159-178.

[Hbk] Charles Wells, A Handbook of Mathematical Discourse (2003).

[SkOut]  Charles Wells, Sketches: Outline with references. (2009).

Charles (at) abstractmath.org