How to prove equations using diagrams, part 1

Motifs among initial functors

Let’s begin with a few minimal examples of initial functors, acting as motifs or patterns. Each such example will give rise to a rule of inference for diagrammatic reasoning.

The target category \(\mathsf{C}\) for the diagrams is fixed throughout. That is, any initial functor should also be a morphism in the category of diagrams in \(\mathsf{C}\), the slice category \(\mathsf{Cat}/\mathsf{C}\).

• Operation introduction: for any morphism \(f: X \to Y\) in \(\mathsf{C}\), the map of diagrams

  

  is initial.

• More generally, for any path \(X_0 \xrightarrow{f_1} X_1 \xrightarrow{f_2} \cdots \xrightarrow{f_n} X_n\) in \(\mathsf{C}\), the map of diagrams

  

  is initial.

• Congruence reduction: for any morphism \(f: X \to Y\) in \(\mathsf{C}\), the map of diagrams,⁴

  

  sending both \(y\) and \(y'\) in the domain shape to \(y\) in the codomain shape, is initial.

• Subsuming both operation introduction and congruence reduction, for any morphism \(f: X \to Y\) in \(\mathsf{C}\) and number \(n \geq 0\), the map of diagrams,

  

  sending all of \(y_1,\dots,y_n\) to \(y\), is initial.

• Equation introduction: suppose that the equation \(g \circ f = k \circ h\) holds in \(\mathsf{C}\), as depicted earlier. Then both maps in the span of free diagrams

  

  are initial. More generally, this works for any path equation in \(\mathsf{C}\). As another example, we can introduce a nullary path equation, say \(\operatorname{id}_X = g \circ f\), as:

  

Later, we will formalize not just the rules but how to apply them, using ideas from category-theoretic rewriting. For the moment, we take for granted that when applying the rules in a larger context, the resulting functors are still initial. Or, you can check initiality by inspection in each application.

Pasting commutative squares

We’re ready to do our first calculation, proving the pasting law for commutative squares: that two commutative squares with a common edge can be juxtaposed to produce a commutative rectangle. The notation makes this seem obviously true—that’s what makes it good notation!—but it still needs a proof. We’ll present the proof in a highly mechanical style, where each diagram in the sequence is related to the previous one by an initial functor or, when introducing an equation, by a span of initial functors.

Assume: We are given the two commutative squares

By this we mean that the target category \(\mathsf{C}\) is generated by six objects, called \(X,X',Y,Y',Z,Z'\), and seven morphisms, called \(f,f',g,g',h,k,\ell\), subject to those two equations.

Construct: Start with the singleton diagram on \(X\), whose limit is trivially \(X\). Introduce the left- and right-hand sides of the path equation we want to prove:

Recognize the path \(X \xrightarrow{h} X' \xrightarrow{f'} Y'\) as the left-hand side of the first square, then introduce that equation:

Apply congruence reduction to the occurrences of \(f\):

Now recognize the path \(Y \xrightarrow{k} Y' \xrightarrow{g'} Z'\) as the left-hand side of the second square, then introduce that equation:

We’re already done, but we might as well tidy up by congruence reducing the occurrences of \(g\) and then \(\ell\):

Conclude: The outer rectangle commutes, since the limit of the diagram is still \(X\).

A monoid presentation

Consider a monoid with an element \(f\) satisfying the equations

\[ f^3 = \operatorname{id}= f^5. \]

That is, the target category \(\mathsf{C}\) is generated by a single object, say \(\bullet\), and an endomorphism, \(f: \bullet \to \bullet\), satisfying those two equations.

Start with the singleton diagram \(\{\bullet\}\) and introduce both defining equations, noting that since each equation has an identity on one side, they appear as cycles:

We leave the arrows unlabeled since every arrow lies over the generating morphism \(f\). We’ll now compute the congruence closure, iteratively applying congruence reduction until that is no longer possible. Arrows affected by a congruence reduction are colored the same on either side of the reduction, starting with the two blue arrows above. The first reduction is:

Next:

Congruence reducing three more times gives the sequence:

We could stop here, but we might as well reduce twice more, yielding the diagram that is the self-loop over \(f\). We have proved the equation

\[ f = \operatorname{id}, \]

since the limit of the diagram is the one we started with, namely the unique object \(\bullet\). In other words, the monoid presented is actually the trivial monoid. You might remember this as a special case of the fact in group theory that if a group element \(g\) satisfies \(g^m = \operatorname{id}= g^n\) for relatively prime numbers \(m\) and \(n\), then \(g = \operatorname{id}\).