Introduction

This post gives a proof of an easy theorem in category theory using the graph-based logic approach of Graph based logic and sketches, (GBLS) by Atish Bagchi and me.

Formal logic is typically defined in terms of formulas and terms, defined recursively as strings of characters, together with rules of inference. GBLS proposes a new approach to logic where diagrams are used instead of strings of characters. The exposition here spells out the proof in more detail than GBLS does and uses various experimental ways of drawing diagrams using Mathematica.

To follow this proof, you need to be familiar with basic category theory. Most special definitions that are needed are defined in this post where they are first used. Section 1 of GBLS also gives the definitions you need with more context.

The theorem

The Theorem to be proved (it is Theorem 8.3.1 of GBLS) says that, in any category, if the triangles in the diagram below commute, then the outside square commutes. This is easy using the associative law: If $xf=h$ and $kx=g$, then $kh=k(xf)=(kx)f=gf$.

Subject Diagram

So what?

This theorem is not interesting. The point of this post is to present a new approach to proving such theorems, using diagrams instead of strings. The reason that exhibiting the dig
rammatic proof is interesting is that many different kinds of categories have a FL cattheory, including these:

• Categories with all finite limits, also called FL categories, left exact categories, cartesian categories, or
  essentially algebraic theories. Note that what I am saying here is that the category of all categories with finite limits is the category of models of a particular category (a cattheory) with finite limits. It is easy to get syntax and semantics (theory and models) confused!
• Finitely complete and cocomplete categories.
• Cartesian closed categories.
• Locally cartesian closed categories.
• Toposes.

Essentially algebraic string-based logic is described in detail in Partial Horn logic and cartesian categories, by E. Palmgren and Steven Vickers.

Commercial

My concept of form in A generalization of the concept of sketch generalizes sketches to all the categories that can be defined as models of FL cattheories. So the method of proof using diagrams can be applied to theorems about the objects defined by forms.

Concepts needed for the graph-based proof

To prove the theorem, I will make use of $\mathbf{ThCat}$, the FL cattheory for categories.

• An FL category is a category with all finite limits.
• GLBS uses the word cattheory for what Category theory for computing science and Toposes, triples and theories call the theory of a sketch.
• In many books and articles, and in nLab, a “sketch” is what we call the cattheory (or the theory) of a sketch. For us, the sketch is a generating collection of objects, arrows, diagrams, cones and cocones for the cattheory. The category of models of the sketch and the cattheory are equivalent.
• $\mathbf{ThCat}$ is a category with finite limits freely generated by certain designated objects, arrows, commutative diagrams and limit cones, listed below.
• A model of $\mathbf{ThCat}$ in $\mathbf{Set}$ (the category of sets, whichever one you like) is an FL functor $\mathfrak{C}:\mathbf{ThCat}\to\mathbf{Set}.$
• Such a model $\mathfrak{C}$ is a small category, and every small category is such a model. If this statement worries you, read Section 3.4 of GBLS.
• Natural transformations between models are FL-preserving functors that preserve the structure on the nose.
• The category of models of $\mathbf{ThCat}$ in $\mathbf{Set}$ is equivalent to the category of small categories and morphisms, which, unlike the category of models, includes functors that don’t preserve things on the nose.
• $\mathbf{ThCat}$ is an example of the theory of an FL sketch. Chapter 4 of GBLS describes this idea in detail. The theory has the same models as the sketch.
• The sketch generating $\mathbf{ThCat}$ is defined in detail in section 7.2 of GBLS.

Some objects and arrows of $\mathbf{ThCat}$

I will make use of the following objects and arrows that occur in $\mathbf{ThCat}.$ A formal thing is a construction in $\mathbf{ThCat}$ that becomes an actual thing in a model. So for example a model $\mathfrak{C}$ of $\mathbf{ThCat}$ in $\mathbf{Set}$ is an actual (small) category, and $\mathfrak{C}(\mathsf{ar_2})$ is the set of all composable pairs of arrows in the category $\mathfrak{C}$.

• $\mathsf{ob}$, the formal set of objects.
• $\mathsf{ar}$, the formal set of arrows.
• $\mathsf{ar}_2$, the formal set of composable pairs of arrows.
• $\mathsf{ar}_3$, the formal set of composable triples of arrows.
• $\mathsf{unit} : \mathsf{ob}\to \mathsf{ar}$ that formally picks out the identity arrow of an object.
• $\mathsf{dom},\mathsf{cod} : \mathsf{ar}\to \mathsf{ob}$ that formally pick out the domain and codomain of an arrow.
• $\mathsf{comp} : \mathsf{ar}_2\to \mathsf{ar}$ that picks out the composite of a composable pair.
• $\mathsf{lfac}, \mathsf{rfac} :\mathsf{ar}_2\to \mathsf{ar}$ that pick out the left and right factors in a composable pair.
• $\mathsf{lfac}, \mathsf{mfac},\mathsf{rfac} :\mathsf{ar}_3 \to\mathsf{ar}$ that pick out the left, middle and right factors in a composable triple of arrows.
• $\mathsf{lass}, \mathsf{rass} : \mathsf{ar}_3 \to \mathsf{ar}_2$: $\mathsf{lass}$ formally takes $\langle{h,g,f}\rangle$ to $\langle{hg,f}\rangle$ and $\mathsf{rass}$ takes it to $\langle{h,gf}\rangle$.

$\mathsf{ob}$, $\mathsf{ar}$, $\mathsf{unit}$, $\mathsf{dom}$, $\mathsf{cod}$ and $\mathsf{comp}$ are given primitives and the others are defined as limits of finite diagrams composed of those objects. This is spelled out in Chapter 7.2 of GBLS. The definition of $\mathbf{ThCat}$ also requires certain diagrams to be commutative. They are all provided in GBLS; the one enforcing associativity is shown later in this post.

Color coding

I will use color coding to separate syntax from semantics.

• Syntax consists of constructions in $\mathbf{ThCat}.$ The description will always be a commutative diagram in black, with annotations as explained later.
• The limit of the description will be an object in $\mathbf{ThCat}$ (the form) whose value in a model $\mathfrak{C}$ will be shown in green, because being an element of the value of a model makes it semantics.
• When a limit cone is defined, the projections (which are arrows in $\mathbf{ThCat}$) will be shown in blue.

Descriptions

In graph-based logic, a type of construction that can be made in a category has a description, which (in the case of our Theorem) is a finite diagram in $\mathbf{ThCat}$. The value of the limit of the description in a model $\mathfrak{C}$ is the set of all instances of that type of construction in $\mathfrak{C}$.

The Subject Diagram

• This diagram is the subject matter of the Theorem. It is not assumed to be commutative.
• As in most diagrams in category theory texts, the labels in this diagram are variables, so the diagram is implicitly universally quantified. The Subject Diagram is a generic diagram of its shape.
• “Any diagram of its shape” includes diagrams in which some of the nodes may represent the same object. An extreme example is the graph in which every node is an object $\mathsf{E}$ and every arrow is its identity arrow. The diagram below is nevertheless an example of the Subject Diagram:



• Shapes of diagrams are defined properly in Section 2.3 of
  GBLS and in Section 4.1 of Category Theory for Computing Science.

The description of the Subject Diagram

Diagram SDD below shows the Subject Diagram as the limit of its description. The description is the black diagram.

Diagram SDD

• Following the practice in GBLS, the nodes of the description are annotated by the variable names used in the Subject Diagram. The annotations are purely for the reader’s convenience, to see for example which copy of $\mathsf{ar}$ formally contains the arrow named $f$.
• The description is a commutative diagram in $\mathbf{ThCat}$, and a model functor $\mathfrak{C}$ must take the description to a commutative diagram in the model. Every node in this commutative diagrams is either the set of all nodes or the set of all arrows in the category $\mathfrak{C}$. Every arrow is either the map that takes an arrow to its domain or the map that takes an arrow to its codomain.
• You can see that the description spells out precisely what the domain and comain of each arrow is. So the value of the limit node must be the set of all diagrams of the form of the Subject Diagram. I have named the limit by exhibiting the Subject Diagram rather than by giving it another random name that you have to remember.

Definition of $\mathsf{ar}_2$

The object $\mathsf{ar}_2$ of composable pairs of arrows is defined as a pullback:

In the usual categorical notation this would be shown as

This makes use of the fact that the unnamed blue arrow is induced by the other two projection arrows. In the rest of the post, projection arrows that are induced are normally omitted.

An enrichment of the description

Because $\mathsf{ar}_2$ is defined as a pullback, we can enrich the description of Diagram SDD by adjoining two pullbacks as shown below. This is Diagram 8.10 in GBLS. The enriched diagram has the same limit as the description of Diagram SDD.

Enriched Diagram SDD

Note that the projections from the limit to the two occurrences of $\mathsf{ar}_2$ induce all the other projections. This follows by diagram chasing; remember that the description must be a commutative diagram.

Make the triangles commute

To make the triangles commute, we add two comp arrows to the enriched diagram as shown below. These two arrows are not induced by the description; they are therefore additions to the description — they describe a more restrictive (green) diagram with commutative triangles and so are shown in black.

Diagram TC: The triangles commute

The left comp makes $xf=h$ and the right comp makes $kx=g$.

The outside square commutes

Now we enrich Diagram TC with four objects, <comp,id>, <id,comp> and three comp arrows as shown in bolder black. These objects and arrows already exist in $\mathbf{ThCat}$ and therefore do not change the limit, which must be the same as the limit of Diagram TC.

The outside square commutes

The diagram in bold black is exactly the commutative diagram that requires associativity for these particular objects and arrows, which immediately implies that $gf=kh$, as the Theorem requires.

By the definitions of $\mathsf{ar_2}$ and $\mathsf{ar_3}$, the part of the description in bold black induces the rest of the diagram. Omitting the rest of the diagram would make $\mathsf{ar_2}$ and $\mathsf{ar_3}$ modules in the sense of GBLS, Chapter 7.4. Modules would be vital to deal with proofs more complicated than the one given here.

References

• Graph based logic and sketches, by Atish Bagchi and Charles Wells.
• Category theory for computing science, by Michael Barr and Charles Wells.
• Toposes, triples and theories, by Michael Barr and Charles Wells.
• On the limitations of sketches, by Michael Barr and Charles Wells. Examples of what forms can describe that sketches can’t.
• Left exact logic, Colin McLarty. Journal of pure and applied algebra 41 (1986), pp. 63-66.
• Partial Horn logic and cartesian categories, E. Palmgren and Steven Vickers. Annals of Pure and Applied Logic, 143 (2007), pp. 314-353. ISSN 0168-0072.
• A formalism for the specification of essentially algebraic structures in $2$-categories, (1992), by John Power and Charles Wells.
• A generalization of the concept of sketch, (1990), by Charles Wells. This is the founding paper for forms.
• Forms, by Charles Wells. This is an introduction to forms aimed a people with only a little knowledge of category theory.
• Forms diagrams, link to Mathematica notebooks and diagrams concerning Forms.

This work is licensed under a Creative Commons Attribution-ShareAlike 2.5 License.