Working up to the syntax-semantics Duality

Today we reach the sacred heights of the syntax-semantics duality by repeatedly defining the monoids.

Level 1

Definition (first course in algebra): a monoid is a set $M$ equipped with a special element $e$ and a multiplication $m$, such that $e$ is the multiplicative identity, and the multiplication is associative.

The natural numbers, with $+$ and $0$, makes a monoid.

Another example is the string monoid: $M$ is all possible English strings made from the 26 letters, $e$ is the empty string, and $m$ is just putting two strings together.

Level 2

The definition rephrases to

Definition (second course in algebra): a monoid is an object $M$ in the category Set, equipped with two arrows, the unit $e: M^0 \to M^1$, and the multiplication $m: M^2 \to M^1$, such that $e$ is a unit of multiplication:
$$m\circ (e, id) = id, m\circ (id, e) = id$$
and $m$ is associative:
$$m\circ (m \times id) = m\circ (id \times m)$$.

by replacing "Set" with a general category, we get:

Definition (category-theoretical): a monoid, in a category $C$ with finite cartesian products, is an object $M$ equipped with two arrows, the unit $e: M^0 \to M^1$, and the multiplication $m: M^2 \to M^1$, such that $e$ is a unit of multiplication:
$$m\circ (e, id) = id, m\circ (id, e) = id: M^1 \to M^1$$
and $m$ is associative:
$$m\circ (m \times id) = m\circ (id \times m): M^3 \to M^1$$.

The requirement for $C$ to have finite cartesian products is so that we can talk about $M^0, M^2, M^3$, etc, without worrying that they won't accidentally not exist. It would be pretty useless to talk about nonexistent objects. For the same reason, I don't talk about my happiness.

This definition works in any category. In the category of topological spaces, it defines "topological monoids", which are just monoids where multiplication is also continuous.

Similarly, if we formalize the definition of groups in the same category-theoretical style, then interpret it in the category of smooth manifolds, we get the Lie groups, where multiplication and inversion are not only continuous, but also smooth. The best-known example of Lie groups is the 3-sphere in 4-d space, with multiplication defined by quaternion multiplication.

Level 3

Consider a monoid in a category $C$ with finite cartesian products, defined by an object $M$, the unit $e$, and the multiplication $m$. Suppose we don't care about anything else in the category $C$, and only care about the monoid, what can we talk about?

Well, we can talk about the objects $M^0, M^1, M^2...$. We can talk about the arrows 

$$e: M^0 \to M^1, m: M^2 \to M^1, m \circ (m, id): M^3 \to M^1, p^2_1: M^2 \to M^1, p^2_2: M^2 \to M^1...$$.

For concreteness, let's work in the category Set. Then we have these arrows:

$$* \mapsto e: M^0 \to M^1, (a, b) \mapsto ab: M^2 \to M^1, (a, b, c) \mapsto a(bc): M^3 \to M^1,$$

$$(a, b) \mapsto a: M^2 \to M^1, (a, b) \mapsto b: M^2 \to M^1...$$

Basically, we have the objects generated by $M$ and the cartesian product, and the morphisms generated by $e, m,$ and the "coordinate maps" between $M^n \to M^k$.

Playing around with these maps and their compositions should convince you that there is exactly one arrow $f: M^n \to M^1$ for every string on the letters $a_1, a_2, ... a_n$. For example: 

$$(a, b, c, d) \mapsto abcd, (a, b, c, d) \mapsto adba, (a, b, c, d) \mapsto a$$

Once you see that, you should also see that there is exactly one arrow $f: M^n \to M^k$ for every $k$ strings on the letters $a_1, a_2, ... a_n$.

Things get confusing, though, if two arrows happen to be equal, even if they "should not be". For example, if $M$ is the set with just one element, then all arrows $M^3 \to M^1$ happen to be equal, even if there are infinitely many of them.

It would be good if we have one category as a "reference manual" that contains exactly the objects and arrows that we would want to use when talking about monoids. What should this category contain? It should contain the objects $A^0, A^1, A^2, ...$, with cartesian product defined on them in the obvious way: $A^n \times A^k = A^{n+k}$. It should contain exactly one arrow $f: A^n \to A^k$ for every $k$ strings on the letters $a_1, a_2, ... a_n$.

Since William Lawvere was the one that made this idea popular, we call this exemplar category $L_{Mon}$, meaning "the Lawvere category of monoids". 

Once we have this reference-category $L_{Mon}$, we can "refer to the reference manual" by a functor out of it. It should preserve finite cartesian products, since we used cartesian products a lot while composing arrows. But otherwise, this is it!

Definition (Lawvere theory): a monoid in a category $C$ with finite cartesian products is a functor $F: L_{Mon} \to C$ that preserves finite cartesian products up to isomorphism, that is, $F(A^n \times A^k) \simeq F(A^n) \times F(A^k)$.

This definition is just a rephrase the previous definition, so the examples are the same.

But what is $L_{Mon}$?

Well, what are the arrows $A^2 \to A^1$? There are $(a, b) \mapsto \emptyset, (a, b) \mapsto a, (a, b) \mapsto b, (a, b) \mapsto ab, (a, b) \mapsto ba, (a, b) \mapsto aab...$. One arrow for each string on $a, b$.

Now, consider an alphabet with letters $a_1, a_2, ...$, and define $S_n$ to be the monoid of strings made by letters $a_1, a_2, ... a_n$. It's easy to see that there is exactly one monoidal map $S_1 \to S_2$ for each string on $a_1, a_2$.

Yes! The category with $S_0, S_1, S_2, ...$ as objects, and monoidal maps between them as arrows, works exactly as $L_{Mon}$!

... except that the arrows are pointing in the wrong direction.

But that's okay, it means we've just constructed $L_{Mon}^{op}$, the opposite category! Simply reverse the arrows, and we've got $L_{Mon}$.

Level 4

The explicit construction of the category $L_{Mon}$ means we have got a concrete thing to handle. It is a semantic definition of monoids: a monoid is any functor out of this explicitly-constructed category. It is a "real" thing that we can use as a reference.

Now we go down the syntactic road.

What does it mean to talk about monoids? It means manipulation of symbols in a mathematical language. The best way to talk about manipulation of symbols is "type theory". Type theory is all about formalizing abstract mathematical reasoning by rewriting terms. We will use type theory here without defining it properly, but it should be readable:

• 1 generating type $A$.
• 2 generating terms $(x:A),(y:A)⊢(m(x,y):A)$ and $⊢(e:A)$.
• 3 generating equalities $(x:A),(y:A),(z:A)⊢(m(m(x,y),z)=m(x,m(y,z)):A)$ and $(x:A)⊢(m(x,e)=x:A)$ and $(x:A)⊢(m(e,x)=x:A)$.

(taken from What Is an n-Theory?)

These generating rules are used in a simply typed lambda calculus with cartesian product. Call the resulting type theory $T_{Mon}$.

Then, there is an exact equivalence with $L_{Mon}$ and $T_{Mon}$. Every generated statement of the form

$$⊢(\lambda (a_1:A),(a_2:A)... (a_n:A). (s_1(a_1, ... a_n), ... s_k(a_1, ... a_n))): A^n \to A^k$$

corresponds precisely to the arrow in $L_{Mon}$, 

$$(a_1, a_2... a_n) \mapsto (s_1(a_1, ... a_n), ... s_k(a_1, ... a_n)): A^n \to A^k$$

where $s_1, ... s_k$ are string functions.

And every generated statement of the form

$$⊢(\lambda (a_1:A),(a_2:A)... (a_n:A). (s_1(a_1, ... a_n), ... s_k(a_1, ... a_n)) = (s'_1(a_1, ... a_n), ... s'_k(a_1, ... a_n))): A^n \to A^k$$

corresponds precisely to an equation in $L_{Mon}$, 

$$(a_1, a_2... a_n) \mapsto (s_1(a_1, ... a_n), ... s_k(a_1, ... a_n)) = (a_1, a_2... a_n) \mapsto (s'_1(a_1, ... a_n), ... s'_k(a_1, ... a_n))$$

This is the syntax-semantics duality!