#monad

Horizontal Composition

In the last blog post, we looked at the monoidal category of endofunctors ([𝒞,𝒞],⊗,1). Objects are endofunctors on the category 𝒞, morphisms are natural transformations and the composition of α: F -> G and β: G -> H is given by the vertical composition (β ∘ α)_A = β_A ∘ α_A. The functor 1: 𝒞 -> 𝒞 is the identity functor and the tensor product F ⊗ G is given by composition of functors F ∘ G. The laws α,λ,ρ are all simply identity. However, the tensor product of natural transformations (i.e. the action of the bifunctor ⊗ on arrows) I gave in my last blog-post doesn't make sense. The definition of a monad only depends on the action of the tensor product on functors, so it doesn't really matter to my last post, but I want to give the correct definition here for the sake of completeness and because this product is later used in defining morphisms between monads.

Suppose we have categories 𝒞, 𝒟 and ℰ, functors F,H: 𝒞 ⇉ 𝒟 and G,J: 𝒟 ⇉ ℰ and natural transformations α: F -> H and β: G -> J as in the diagram on the right below:

A pair of vertically composable natural transformations (left) and a pair of horizontally composable natural transformations (right).

We want to define the horizontal composition of α and β, denoted β * α, as a natural transformation from G ∘ F to J ∘ H. There seem to be two different ways to do this. We can set β * α = Jα ∘ βF or β * α = βH ∘ Gα, as illustrated in the diagram on the left below:

A diagram of transformations (left) and that same diagram indexed by an object A (right). Composition of functors is denoted using juxtaposition instead of the ring operator to avoid clutter.

However, these two ways of defining β * α give the same result, i.e. the diagram on the left is commutative. To see this, note that the diagram on the left commuting is equivalent to the diagram on the right commuting for every object A of 𝒞. This follows immediately from the naturality of β. And so, we have

Definition. For categories 𝒞, 𝒟 and ℰ, functors F,H: 𝒞 ⇉ 𝒟 and G,J: 𝒟 ⇉ ℰ and natural transformations α: F -> H and β: G -> J, call the pair (α,β) a horizontally composable pair of natural transformations. Define the horizontal composition by β * α := Jα ∘ βF = βH ∘ Gα. ❀

Now, we can complete the definition of the monoidal category of endofunctors by setting the tensor product β ⊗ α of natural transformations to be the horizontal composition β * α.

T-algebras

Recall the definition of a T-algebra:

Definition. Let 𝒞 be a category and let (T,μ,η) be a monad over 𝒞. A T-algebra is a pair (X,α) with an object X in 𝒞 and an arrow α: T(A) -> A in 𝒞 satisfying the following two conditions:

α ∘ η_X = id_X;

α ∘ T(α) = α ∘ μ_X.

X is called the carrier and α is called the action of the T-algebra. ❀

Example. If T = list is the list monad over Set, then a list-algebra consists of a set X and a function α: list(X) -> X that maps a list of elements of X to a single element of X, so that α maps the list (x) to x and

α(α(x_11,...,x_1n₁),...,α(x_m1,...,x_mnₘ)) = α(x_11,…,x_1n₁,…,x_m1,…,x_mnₘ)

I.e. applying α to each element of a nested list and then applying α again is equivalent to first flattening the list and then applying the action α once. We can see a list-algebra is equivalent to a monoid. The neutral element of the monoid is given by α() and the monoid operation is given by x ∘ y := α(x,y). The operation ∘ is associative as α(α(x,y),z) = α(x,y,z) = α(x,α(y,z)) (note: α(x) = x and α(z) = z). Further, by the second condition of a T-algebra, any expression of the form α(x₁,...,xₙ) can be reduced to x₁ ∘ ... ∘ xₙ. ◆

As we'll see later in this blog-post, this correspondence between algebras of the monad list and algebras of a certain kind (namely, monoids) isn't a coincidence.

I'll now define the category of T-algebras.

Definition. Let 𝒞 be a category and let (T,μ,η) be a monad over 𝒞. We define the category Alg(T) of T-algebras:

Objects are T-algebras (X,α);

A morphism from (X,α) to (Y,β) is a morphism f: X -> Y in 𝒞 for which f ∘ α = β ∘ T(f). ❀

Equivalent Categories

For elements x and y of a set, we treat them as identical when they are equal. For objects of a category, such as sets, topologies or groups, strict equality is often too strict of a condition for identity, so we often view objects A and B as "identical" when they are isomorphic (i.e. have an isomorphism between them): we care about the overall structure of these objects, not the specific names we give the data of such an object (such as the exact elements of a set or group). For categories themselves, however, isomorphism is still too strict of a condition. There is a weaker condition, called "equivalence", which is in some sense the "correct" way to identify categories.

Definition. Categories 𝒞 and 𝒟 are equivalent, denoted 𝒞 ≃ 𝒟, iff there are functors F: 𝒞 -> 𝒟 and G: 𝒟 -> 𝒞 and natural isomorphisms α: G ∘ F -> id_𝒞 and β: F ∘ G -> id_𝒟. Such a quadruple (F,G,α,β) is called an equivalence of 𝒞 and 𝒟. ❀

I'll introduce some basic category-theoretic notions before giving an example.

Definition. A functor F: 𝒞 -> 𝒟 is full iff, for all objects A,B in 𝒞 and every arrow g: F(A) -> F(B) in 𝒟, there is an arrow f: A -> B in 𝒞 for which F(f) = g. It is faithful iff, for all objects A,B in 𝒞 and arrows f,g: A ⇉ B in 𝒞, if F(f) = F(g), then f = g. It is fully faithful iff it is both full and faithful. ❀

So, a functor is full if it is surjective on arrows (between objects in its image), and faithful if it is injective on arrows.

Definition. A subcategory of a category 𝒞 is a category ℬ for which:

Ob(ℬ) ⊂ Ob(𝒞) (every object of ℬ is an object of 𝒞);

For objects A,B in ℬ, ℬ(A,B) ⊂ 𝒞(A,B) (every arrow in ℬ is an arrow in 𝒞).

We call a subcategory ℬ ⊂ 𝒞 a full subcategory iff its inclusion functor m: ℬ -> 𝒞, defined by m(A) = A and m(f) = f, is full. ❀

I.e. in a full subcategory, we have ℬ(A,B) = 𝒞(A,B). The inclusion functor m is automatically faithful.

Definition. Let 𝒞 be a category. An object I in 𝒞 is called initial iff, for every object A in 𝒞, there is a unique arrow I -> A. An object T in 𝒞 is called terminal iff, for every object A in 𝒞, there is a unique arrow A -> T. ❀

For example, in Set, the initial object is the empty set ∅ and the terminal object is a singleton {*}.

I will now give an example of an equivalence.

Example. Let 𝒞 be the full subcategory of Set consisting of finite subsets of ℕ (i.e. finite sets of natural numbers) and let 𝒟 be the full subcategory of Set consisting of sets of the form [n] = {0,...,n-1} for n in ℕ. Then, 𝒞 and 𝒟 are not isomorphic: 𝒞 has infinitely many (ℵ₀ to be exact) terminal objects, one {n} for every n in ℕ, but 𝒟 only has [1] = {0}. However, they are equivalent. We can define the functor F: 𝒞 -> 𝒟 by mapping the set A to the set [#A], where #A denotes the number of elements of A, and F maps the function f: {a₀,...,aₘ₋₁} -> {b₀,...,bₙ₋₁} to the function F(f): [m] -> [n] defined by F(f)(k) = l, where f(aₖ) = bₗ, and a₀ < ... < aₘ₋₁ and b₀ < ... < bₙ₋₁. The reader may verify F is indeed functorial, i.e. preserves identities and composition. The functor G: 𝒟 -> 𝒞 is defined by G([n]) = [n] and G(f) = f. For A = {a₀,...,aₙ₋₁} in 𝒞, with a₀ < ... < aₙ₋₁, we set α_A (aₖ) = k. For [n] in 𝒟, we set β_[n] (k) = k. Then, (F,G,α,β) is an equivalence of categories. ◆

Algebraic Theories

Definition. An algebraic signature σ has the following data:

A collection F of function symbols;

A function |·|: F -> Card that maps a function symbol f to its arity |f|. ❀

Here, the arity |f| of a function symbol f in F is a cardinal number, i.e. the size of some set. We may also define |f| as simply a set itself. We usually write the arity of a function symbol in its superscript, so that, e.g., f² is a symbol with arity 2. We call symbols with arity 0, 1, 2, 3, etc, nullary, unary, binary, ternary, etc, respectively. Nullary function symbols are also called constants symbols.

Example. Let F = {∘,e}, |∘| = 2 and |e| = 0. Then, σ, consisting of F and |·|, is an algebraic signature. We then write σ = (∘²,e⁰). ∘ is a binary function symbol and e is a constant symbol. ◆

Definition. Given an algebraic signature σ, we define a functor Term(σ,-): Set -> Set. For a set V, Term(σ,V) is the set of terms of σ over V, and is defined recursively as follows:

For each v in V, (0,v) is in Term(σ,V);

For each function symbol f and function t⃗: |f| -> Term(σ,V), (1,f,t⃗) is in Term(σ,V).

Or, formally, as:

Term(σ,V)_α = ({0} × V) ∪ ⋃{β<α} {(1,f,t⃗) | f in F; t⃗: |f| -> Term(σ,V)_β};

Term(σ,V) = ⋃{α in Ord} Term(σ,V)_α.

For a function g: V -> W, we define a function Term(σ,g): Term(σ,V) -> Term(σ,W), called substitution, recursively as follows:

Term(σ,g)(0,v) = (0,g(v));

Term(σ,g)(1,f,t⃗) = (1,f,g ∘ t⃗).

I'll abbreviate Term(σ,g) to g*. ❀

Informally, we write v for (0,v) and f(t⃗) for (1,f,t⃗). Depending on the function symbol and arity, one of the following notations may also be used for (1,f,t⃗):

f if |f| = 0;

a f b if |f| = 2, t⃗(0) = a and t⃗(1) = b.

Terms of σ over V are also called formal expression of σ in V. Here, V acts as a set of formal variables or basic terms, which can be combined together using the function symbols to make more complicated terms.

Definition. A formal equation over an algebraic signature σ is a triple (V,s,t) with a set V and formal expressions s and t in Term(σ,V). ❀

Informally, we write (V,s,t) as s = t. For example, (a ∘ b) ∘ c = a ∘ (b ∘ c) is a formal equation expressing associativity of ∘. Formally, this is written as:

({a,b,c},(1,∘,(1,∘,(0,a),(0,b)),(0,c)),(1,∘,(0,a),(1,∘,(0,b),(0,c))))

Definition. An algebraic theory T is a pair (σ,E) with an algebraic signature σ and a collection E of formal equations over σ. ❀

We often write an algebraic theory as (F | E), where F is a list of function symbols with their arity in the superscript, and E is a list of formal equations.

Example. The algebraic theory of monoids is:

(∘², e⁰ | (a ∘ b) ∘ c = a ∘ (b ∘ c), a ∘ e = a, e ∘ a = a). ◆

We want to be able to model these theories, so that e.g. a model of the theory of monoids is a monoid.

Definition. Let σ be an algebraic theory. A model 𝔐 of σ has the following data:

A set M;

For each function symbol f of σ, a function f^M: M^|f| -> M.

We define an evaluation (-)^M: Term(σ,M) -> M of terms in M by recursion as follows:

(0,v)^M = v;

(1,f,t⃗)^M = f^M((-)^M ∘ t⃗).

Let T = (σ,E) be an algebraic theory. A model of T is a model 𝔐 of the signature σ satisfying the following:

For every formal equation (V,s,t) in E and every function g: V -> M, we have (g* (s))^M = (g* (t))^M. ❀

Example. A model of the theory of monoids is a monoid. ◆

Morphisms of models are morphisms of the underlying sets that preserve the functions of that model. This makes the collection of models of a signature or theory into a category.

Definition. Let σ be an algebraic signature and let 𝔐 and 𝔑 be models of σ. A morphism from 𝔐 to 𝔑 is a function g: M -> N for which, for all function symbols f of σ and all functions t⃗: |f| -> M, we have g(f^M(t⃗)) = f^N(g(t⃗)). We write Model(σ) for the category of models of σ. For an algebraic theory T = (σ,E), we write Model(T) for the full subcategory of models of T. ❀

Example. A morphism from a monoid (M,∘) to a monoid (N,∘) is a function f: M -> N for which f(a ∘ b) = f(a) ∘ f(b) and f(e) = e. ◆

Example. The algebraic theory ( | a = b) has, up to isomorphism, two models. One where M is empty, and one where M has a single element. The category Model( | a = b) is equivalent to the category → or 2, which has two objects A and B and one non-identity arrow from A to B. ◆

Example. The algebraic theory (!⁰ | a = !) only has one model {!}. The category Model(!⁰ | a = !) is equivalent to the terminal category, which has one object and only the identity arrow on that object. ◆

Example. For every algebraic theory T = (σ,E), there is a model 𝔐 with M = {*} a singleton and, for every function name f of σ, f(t⃗) = *. This model is always the terminal object of Model(T). ◆

Later in the blog-post, I will give a sketch of the following theorem:

Theorem. For every algebraic theory T, there is a monad (T,μ,η) over Set for which Model(T) ≃ Alg(T). Conversely, for every monad (T,μ,η) over Set, there is an algebraic theory T for which Alg(T) ≃ Model(T). □

Technically, the theorem as stated above is not entirely true due to some details regarding proper classes. I won't explain these details now as they are a bit too technical. I will give a more precise version of this theorem in the chapter Algebras and Models which clarifies the details regarding proper classes.

Adjoint Functors

Definition. Let 𝒞 be a category. We define the hom-functor Hom: 𝒞^op × 𝒞 -> Set for 𝒞. For objects A,B in 𝒞, let Hom(A,B) = 𝒞(A,B) be the set of arrows from A to B. For objects A,B,C,D in 𝒞 and arrows f: A -> B and h: C -> D in 𝒞, define the function Hom(f,h): Hom(B,C) -> Hom(A,D) as follows: for g: B -> C, set Hom(f,h)(g) = h ∘ g ∘ f. ❀

Note that Hom is contravariant in its left argument and covariant in its right. We sometimes use Hom_𝒞 to denote the hom-functor for the category 𝒞.

Definition. Let 𝒞 and 𝒟 be categories and let F: 𝒞 -> 𝒟 and G: 𝒟 -> 𝒞 be functors. We say (F,G) is an adjoint pair (F is left-adjoint to G, or G is right-adjoint to F), denoted F ⊣ G, iff there is a natural bijection α: Hom_𝒟(F(-),-) -> Hom_𝒞(-,G(-)). I.e. iff, for all objects X of 𝒞 and Y of 𝒟, there is a bijection α_(X,Y): 𝒟(F(X),Y) -> 𝒞(X,G(Y)) so that, for an arrow f: X' -> X in 𝒞, an arrow h: Y -> Y' in 𝒟 and an arrow g: F(X) -> Y in 𝒟, we have that α_(X,Y) (G(h) ∘ g ∘ f) = h ∘ α_(X',Y') (g) ∘ f. ❀

This definition looks very complicated. The picture I like to have in mind is the following:

Arrows from F(X) to Y correspond to arrows from X to G(Y) in a natural way.

What "in a natural way" means exactly is the complicated part.

Example. Let U: Grp -> Set be the forgetful functor of the category of groups. I.e. U sends a group (G,∘) to its set G and sends a group homomorphism f: (G,∘) -> (H,*) to the function f: G -> H. Then, U has a left-adjoint F: Set -> Grp that maps a set X to the free group F(X) generated by X. We see that a function f: X -> G corresponds to a group homomorphism F(X) -> (G,∘) (that maps a generator x in X to the group element f(x)) and that, conversely, a group homomorphism g: F(X) -> (G,∘) has a corresponding function g|X: X -> G. ◆

Example. Let U: Top -> Set be the forgetful functor of topologies. I.e. U sends a topology (X,τ) to the set X and sends a continuous map f: (X,τ₁) -> (Y,τ₂) to the function f: X -> Y. Then, U has a left- and a right-adjoint. The left adjoint, L: Set -> Top endows a set X with the discrete topology L(X) = (X,P(X)), and the right adjoint R: Set -> Top endows a set X with the indiscrete topology R(X) = (X,{∅,X}). For a topology (Y,τ) and sets X and Z, we see that a function f: X -> Y is a continuous map from (X,P(X)) to (Y,τ), and a function g: Y -> Z is a continuous map from (Y,τ) to (Z,{∅,Z}). ◆

Adjoints of a functor are always unique up to natural isomorphism, which I won't prove in this blog-post. The reason I bring adjoint functors up is because a monad (T,μ,η) induces an adjoint pair F ⊣ U, with F: 𝒞 -> Alg(T) and U: Alg(T) -> 𝒞. This adjunction is defined as follows:

Definition. Let (T,μ,η) be a monad over 𝒞. We define functors U: Alg(T) -> 𝒞 and F: 𝒞 -> Alg(T) (the forgetful functor and the free functor). For a T-algebra (X,α) in Alg(T), let U(X,α) = X. For a morphism f: (X,α) -> (Y,β) in Alg(T), define U(f): U(X,α) -> U(Y,β) by U(f) = f. For an object X in 𝒞, let F(X) = (T(X),μ_X). For a morphism f: X -> Y in 𝒞, define F(f): F(X) -> F(Y) by F(f) = T(f). ❀

That F(f) is a homomorphism in Alg(T) follows immediately from the naturality of μ.

Theorem. F ⊣ U.

It's a long diagram chase, but the proof is not too difficult. I encourage the reader to first try to prove this theorem for themselves (or, at least, define the bijections α_(X,(Y,β)): Hom(F(X),(Y,β)) -> Hom(X,U(Y,β)) and prove that they are bijections) to familiarize themselves with this style of proof.

Proof. For a morphism f: F(X) -> (Y,β) in Alg(T), I define the corresponding morphism g: X -> U(Y,β) in 𝒞 by setting g = f ∘ η_X.

Conversely, for a morphism g: X -> U(Y,β) in 𝒞, I define the corresponding morphism f: F(X) -> (Y,β) in Alg(T) by setting f = β ∘ T(g).

We want to verify f is a morphism in Alg(T), i.e. that f ∘ μ_X = β ∘ T(f). By definition of f, we want to show that β ∘ T(g) ∘ μ_X = β ∘ T(β ∘ T(g)). As T is a functor, and thus preserves composition, we want to show that β ∘ T(g) ∘ μ_X = β ∘ T(β) ∘ T²(g). So, we want to show that the outer rectangle in the following diagram commutes:

This is implied by the two inner squares commuting. The square on the left commutes by naturality of μ. The square on the right commutes by the definition of (Y,β) being a T-algebra. So, we have that f is a morphism in Alg(T).

We now want to show these two correspondences are inverses of eachother. I.e. that, for f: F(X) -> (Y,β) in Alg(T), we have f = β ∘ T(f ∘ η_X) and that, for g: X -> U(Y,β) in 𝒞, we have g = β ∘ T(g) ∘ η_X.

First, let f: F(X) -> (Y,β) in Alg(T). As T is a functor, we want to show that f = β ∘ T(f) ∘ T(η_X). As f is a morphism in Alg(T), we have that β ∘ T(f) = f ∘ μ_X, so we can reduce the problem to f = f ∘ μ_X ∘ T(η_X). As (T,μ,η) is a monad, we have that μ_X ∘ T(η_X) = 1_T(X), so we want f = f ∘ 1_T(X), which is immediate.

Second, let g: X -> U(Y,β) in 𝒞. We want to show that g = β ∘ T(g) ∘ η_X. by naturality of η, we have that T(g) ∘ η_X = η_Y ∘ g. So, we want to show that g = β ∘ η_Y ∘ g. As (Y,β) is a T-algebra, we have that β ∘ η_Y = 1_Y, so we want to show g = 1_Y ∘ g, which is immediate.

This proof is getting too long, so I'll skip showing the naturality of this correspondence. ∎

The reader may verify naturality themselves if they so wish.

Kind of surprisingly, an adjunction F ⊣ G, with F: 𝒞 -> 𝒟 and G: 𝒟 -> 𝒞 also induced a monad (T,μ,η) on 𝒞 and a comonad (C,δ,ε) on 𝒟, which is nothing but a monad over the opposite category 𝒟^op.

Definition. Let 𝒞 and 𝒟 be categories and let F: 𝒞 -> 𝒟 and G: 𝒟 -> 𝒞 be adjoint functors (so that F ⊣ G), witnessed by α: Hom_𝒟(F(-),-) -> Hom_𝒞(-,G(-)). We define a monad (T,μ,η) over 𝒞 and a comonad (C,δ,ε) over 𝒟. We set T = G ∘ F and C = F ∘ G. The unit η: 1 -> T is defined by η_A = α_(A,FA) (1_FA) for A in 𝒞 and the counit ε: C -> 1 is defined by ε_A = α⁻¹_(GA,A) for A in 𝒟. For A in 𝒞, define μ_A: T²A -> TA by μ_A = G(ε_FA) and, for A in 𝒟, define δ_A: CA -> C²A by δ_A = F(η_GA). ❀

Example. Let U: Grp -> Set be the forgetful functor of groups and let F: Set -> Grp be the free group functor. The induced monad maps a set X to the underlying set of the free group generated by X, the unit η_X maps an element x of X to its corresponding element in the free group and μ_X maps an element of the free group generated by elements of the free group of X to its "evaluation" in the free group generated by X, e.g. μ_X([x] * [y * z]) = x * y * z, where x, y and z are in X, [x] is the element of the free group generated by elements of the free group of X corresponding to x and [y * z] is the generator of the free group generated by elements of the free group of X corresponding to the element x * y in the free group generated by X. The comonad C maps a group G to the free group C(G) generated by elements of G and maps a group homomorphism f: G -> H to a group homomorphism C(f): C(G) -> C(H) which is the unique homomorphism extending the function G -> C(H) defined by sending an element g of G to the generator f(g) of C(H). The counit ε_A: C(G) -> G is the unique group homomorphism extending the identity function on G. The comultiplication δ_G: C(G) -> C(C(G)) sends a generator g of C(G) to g. ◆

Example. Let U: Top -> Set be the forgetful functor of topologies and let F: Set -> Top be the discrete functor. Then, T is the identity on Set, and μ and η are the identity on T. Note that, now, the category Alg(T) is not equivalent to the category Top we started with. So, a monad induced by an adjunction can forget some of the structure. ◆

Category of Monads

Definition. Let (𝒞,⊗,I) be a monoidal category. Define the category of monoids Mon(𝒞) as follows:

Objects are monoids (M,m,e) in 𝒞;

A morphism from (M,m,e) to (M',m',e') is a morphism f: M -> M' in 𝒞 for which the following diagrams commute:

I.e. f ∘ m = m' ∘ (f ⊗ f) and f ∘ e = e'. ❀

The category of monads over 𝒞, denoted Mnd(𝒞), is then simply the category of monoids over ([𝒞,𝒞],∘,1). Explicitly, a morphism from a monad (T,μ,η) to a monad (T',μ',η') is a natural transformation φ: T -> T' for which φ ∘ η = η' and φ ∘ μ = μ' ∘ (φ * φ). Here, * denotes the horizontal composition from the first chapter.

For a monad (T,μ,η) over 𝒞, we have defined a category of T-algebras Alg(T). One might wonder if we can extend Alg(-) to a functor from Mnd(𝒞) to Cat. My guess is that the following works:

Let (T,μ,η) and (T',μ',η') be monads over 𝒞 and let φ: (T',μ',η') -> (Τ,μ,η) be a morphism of monads. We define a functor Alg(φ): Alg(T) -> Alg(T'). For a T-algebra (X,α), we set Alg(φ)(X,α) = (X, α ∘ φ_X). For a morphism f: (X,α) -> (Y,β) in Alg(T), we set Alg(φ)(f) = f.

Though I have not verified this is well-defined.

Logic of Equations

Given an algebraic theory T, we can define the forgetful functor U: Model(T) -> Set. For a model 𝔐, U(𝔐) is the underlying set M, and for a morphism f: 𝔐 -> 𝔑, we can set U(f) = f: M -> N. If we can find a left-adjoint F: Set -> Model(T), we have a monad T = U ∘ F. The free functor F will be something like a "free functor" for models, mapping a set X to a model of T freely generated by X (every function X -> N extends uniquely to a morphism F(X) -> 𝔑, "free" refers to the existence of an extension, "generated" refers to the uniqueness).

For an algebraic signature σ, we can define a left-adjoint F: Set -> Model(σ) to U by mapping a set X to a model 𝔐 with domain M = Term(σ,X) and functions f^M (t⃗) = (1,f,t⃗), and mapping a function g: X -> Y to the function Term(σ,g). I.e. F(X) is the set of formal expressions in X and F(g) is the substitution function.

However, for an algebraic theory T = (σ,E), we have a set of formal equations E that needs to be satisfied by the model. So, the free model for a signature as described above isn't necessarily a model of T. So, we want to take a kind of quotient of the model, identifying two elements of the model if they can be proven to be equal within the theory. Knowing which expressions can be proven equal requires a logic. Since the only thing we want to do in this logic is prove when two expressions are equal, I call this logic the logic of equations.

For a function g: V -> W and a formal equation (V,s,t), I write g*(V,s,t) for (W,g*(s),g*(t)). We can generalize the case for a function g: V -> W to a function g: V -> Term(σ,W):

Definition. Let σ be an algebraic signature, let V and W be sets and let g: V -> Term(σ,W) be a function. I define a function g*: Term(σ,V) -> Term(σ,W) by recursion as follows:

g*(0,v) = g(v);

g*(1,f,t⃗) = (1,f,g* ∘ t⃗). ❀

If g: V ∪ {x} -> Term(σ,V) satisfies g(v) = v for v in V and g(x) = t, then we write e[x <- t] for g*(e), where e is a formal expression or a formal equation.

Definition. Let T = (σ,E) be an algebraic theory and let X be a set. A proof is a sequence (φ₀,...,φₙ) of formal equations φₖ = (X,sₖ,tₖ) over σ, where n is an ordinal, so that, for each k < n, at least one of the following holds:

Axiom. There is a formal equation (V,s,t) in E and a function g: V -> Term(σ,X) for which φₖ = g*(V,s,t);

Reflexivity. sₖ = tₖ;

Substitution. There is some set Y disjoint from X, a function i: Y -> k, some j < k and terms s,t in Term(σ,X ∪ Y) for which φⱼ = g*(X,s,t) and φₖ = h*(X,s,t), where g: X ∪ Y -> X and h: X ∪ Y -> X are defined by g(x) = h(x) = x for x in X, g(y) = s_i(y) and h(y) = t_i(y).

The proof (φ₀,...,φₙ) is said to prove the formal equation φₙ. If there is a proof of φ, then we write T ⊦ φ. ❀

There's probably a better way to do this.

Example. Let T = (a⁰,b⁰,c⁰ | a = b, b = c) and X = ∅. Then, (a = b, b = c, a = c) is a proof of a = c. The first two equations satisfy the rule axiom and the last satisfies substitution with Y = {y}, i(y) = 1 and j = 0: (a = b) = (a = y)[y <- b] and (a = c) = (a = y)[y <- c]. ◆

Example. Let T = (a⁰,b⁰ | a = b) and X = ∅. Then, (a = a, a = b, b = a) is a proof of b = a. The first equation satisfies reflexivity, the second satisfies axiom and the third satisfies substitution with Y = {y}, i(y) = 1 and j = 0: (a = a) = (y = a)[y <- a] and (b = a) = (y = a)[y <- b]. ◆

Example. Let T be the theory of monoids and X = {a,b,c,d}. Then, the following is a proof of ((a ∘ b) ∘ c) ∘ d = a ∘ (b ∘ (c ∘ d)):

Axiom. (a ∘ b) ∘ c = a ∘ (b ∘ c);

Substitution. ((a ∘ b) ∘ c) ∘ d = (a ∘ (b ∘ c)) ∘ d;

Axiom. (a ∘ (b ∘ c)) ∘ d = a ∘ ((b ∘ c) ∘ d);

Substitution. ((a ∘ b) ∘ c) ∘ d = a ∘ ((b ∘ c) ∘ d);

Axiom. (b ∘ c) ∘ d = b ∘ (c ∘ d);

Substitution. a ∘ ((b ∘ c) ∘ d) = a ∘ (b ∘ (c ∘ d));

Substitution. ((a ∘ b) ∘ c) ∘ d = a ∘ (b ∘ (c ∘ d)). ◆

Example. Let T = (f^ℵ₀, a₀⁰, a₁⁰, a₂⁰, ..., b₀⁰, b₁⁰, b₂⁰, ... | a₀ = b₀, a₁ = b₁, a₂ = b₂, ...). Then, (a₀ = b₀, a₁ = b₁, a₂ = b₂, ..., f(a₀, a₁, a₂, ...) = f(b₀, b₁, b₂, ...)) is an (infinitely long) proof of f(a₀, a₁, a₂, ...) = f(b₀, b₁, b₂, ...). ◆

Note that, for proofs (φ₀,...,φₘ) and (ψ₀,...,ψₙ) and for k < m, (φ₀,...,φₘ,ψ₀,...,ψₙ) and (φ₀,...,φₖ) are again proofs.

Theorem. Let T = (σ,E) be an algebraic theory and let X be a set. Define a binary relation ~ on Term(σ,X) as follows: s ~ t iff T ⊦ (X,s,t). Then, ~ is an equivalence relation. I.e.:

t ~ t for all t in Term(σ,X);

If s ~ t and t ~ u, then s ~ u;

If s ~ t, then t ~ s.

Proof. For a term t, ((X,t,t)) is a proof of (X,t,t). For terms s, t and u, suppose s ~ t and t ~ u witnessed by (φ₀,...,φₘ) and (ψ₀,...,ψₙ). Then, (φ₀,...,φₘ,ψ₀,...,ψₙ,(X,s,u)) is a proof of (X,s,u), where the last formal equation satisfies the substitution rule. Suppose s ~ t witnessed by (φ₀,...,φₙ). Then, (φ₀,...,φₙ,(X,s,s),(X,t,s)) is a proof of (X,t,s), where the second-to-last formal equation satisfies the reflexivity rule and the last satisfies the substitution rule. ∎

Theorem. Let T = (σ,E) be an algebraic theory, let X and Y be sets and let g: X -> Y be a function. For s,t in Term(σ,X), if T ⊦ (X,s,t), then T ⊦ g*(X,s,t).

Proof. Let (φ₀,...,φₙ) be a proof of (X,s,t). Then, (g*(φ₀),...,g*(φₙ)) is a proof of g*(X,s,t). ∎

Definition. Let T = (σ,E) be an algebraic theory. We define a functor F: Set -> Model(T). Let X be a set and let ~ be as in the theorem above. We set F(X) = 𝔐 with domain M = Term(σ,X)/~ = {[s] | s in Term(σ,X)}, where [s] = {t | s ~ t}. For a function symbol f in σ and a function t⃗: |f| -> M, where t⃗(a) = [t_a], set f^M (t⃗) = [(1,f,(t_a))]. For a function g: X -> Y, we define F(g): F(X) -> F(Y) by F(g)([t]) = [g(t)]. ❀

Theorem. Let T = (σ,E) be an algebraic theory. If T ⊦ (X,s,t), then, for all models 𝔐 of T and all functions g: X -> M, we have g*(s)^M = g*(t)^M (soundness). Conversely, if, for all models 𝔐 of T and all functions g: X -> M, we have g*(s)^M = g*(t)^M, then T ⊦ (X,s,t) (completeness).

I'm getting eepy, so I won't proof this theorem now.

Algebras and Models

Theorem. Let T be an algebraic theory and let U: Model(T) -> Set and F: Set -> Model(T) be as described in the previous chapter. Then, F ⊣ U.

Proof sketch. For a function f: X -> U(𝔑), we define a corresponding morphism g: F(X) -> 𝔑. We set g([t]) = f*(t)^N, this function is well-defined by soundness. For a morphism g: F(X) -> 𝔑, we define a corresponding function f: X -> U(𝔑) by f(x) = g([(0,x)]). By completeness, for a morphism g: F(X) -> 𝔑, we have that f*(t)^N = g(t), where f is defined by f(x) = g([(0,x)]). ∎

Theorem. Let T be an algebraic theory and let (T,μ,η) be the monad induced by F ⊣ U. Then, Model(T) ≃ Alg(T).

Proof sketch. We define an equivalence (H,J,γ,δ). Define H: Model(T) -> Alg(T) by H(𝔐) = (M,α) where α: TM -> M is defined by α([t]) = t^M, and H(f) = f. Define J: Alg(T) -> Model(T) by J(X,α) = 𝔐, with domain M = X and functions f^M (t⃗) = α([(1,f,t⃗)]). We set γ and δ to both be the identity. ∎

Theorem. Let (T,μ,η) be a monad over Set. Then, there is an algebraic theory T for which Alg(T) ≃ Model(T).

Proof sketch. For every set X and every t in T(X), we add a function symbol (X,t) to the language T with arity |(X,t)| = #X equal to the cardinality of X. Further, for sets X, Y and Z, functions g: X -> Z and h: Y -> Z and elements s of T(X) and t of T(Y), if T(g)(s) = T(h)(t), then we have a formal equation (Z,(1,(X,s),g),(1,(Y,t),h)) in T. ∎

One might notice the theory T in the sketch above is a large theory: is has a proper class of function symbols and formal equations. I had previously said F (the collection of function symbols) and E (the collection of formal equations) of an algebraic theory T are "collections" to keep it vague whether they are sets or proper classes. The theorem from the chapter Algebraic Theories applies if T is a small theory (i.e. has a set of function symbols and equations), but more generally if free models of T are small. So, the precise theorem of the chapter Algebraic Theories is:

Theorem. For every algebraic theory T, if the free functor F: Set -> Model(T) exists (i.e. if free models of T are small), then there is a monad (T,μ,η) over Set for which Model(T) ≃ Alg(T). Conversely, for every monad (T,μ,η) over Set, there is an algebraic theory T for which Alg(T) ≃ Model(T). ∎

Transitivity of Alg(-)

For a monad (T,μ,η) over 𝒞, call Alg(T) a category of algebras over 𝒞. Then, given a monad (T,μ,η) over 𝒞, we have a category of algebras Alg(T) over 𝒞, over which we can define another monad (T',μ',η'), which then gives us a category Alg(T') of algebras over Alg(T). Is there a way to define a monad T * T' over 𝒞 for which Alg(T') is equivalent to Alg(T * T')?

For example, we can set T to be the group monad over Set. I.e. T = U ∘ F where F: Set -> Grp is the free group functor and U: Grp -> Set is the forgetful functor. Then, Alg(T) ≃ Grp. We can then define a monad (T',μ',η') over Grp. For a group G, T'(G) = Gₐᵦ = G/G' is the group G made Abelian (there is no subscript b so I'm using β instead) (G' is the derivative of G, which is the subgroup generated by the commutators [a,b] = aba⁻¹b⁻¹ of G). For groups G and H and a group homomorphism f: G -> H, T'(G): Gₐᵦ -> Hₐᵦ sends the coset aG' to f(a)H'. For a group G, μ'_G: (Gₐᵦ)ₐᵦ -> Gₐᵦ is the identity (the derivative of an Abelian group is trivial) and η'_G: G -> Gₐᵦ sends g to its coset gG'. A T'-algebra is a pair (G,α) with a group G (the carrier) and a group homomorphism α: Gₐᵦ -> G (the action) for which α ∘ η'_G = id_G, meaning that α(gG') = g, and α ∘ μ'_G = α ∘ T'(α). As functions send equal elements to equal elements, if gG' = hG', then α(gG') = α(hG') = g = h. So, G' is trivial and the carrier G must already be Abelian. The second condition of a T'-algebra is then automatic: α(μ'(g)) = α(T'(α)(g)) = g. So, the category of T'-algebras is equivalent to the category Ab of Abelian groups which is equivalent to a category of algebras over Set.

Theorem. Let 𝒞, 𝒟 and ℰ be categories, let F: 𝒞 -> 𝒟 and G: 𝒟 -> 𝒞 be a pair of adjoint functors F ⊣ G and let H: 𝒟 -> ℰ and J: ℰ -> 𝒟 be a pair of adjoint functors H ⊣ J. Then, H ∘ F ⊣ G ∘ J.

Proof. Let α: Hom_𝒟(F(-),-) -> Hom_𝒞(-,G(-)) and β: Hom_ℰ(H(-),-) -> Hom_𝒟(-,J(-)) be natural isomorphisms. Then, α(1_𝒞 × J) ∘ β(F × 1_ℰ) is a natural isomorphism from Hom_ℰ(H(F(-)),-) to Hom_𝒞(-,G(J(-))). ∎

In the proof above, for functors F: 𝒜 -> 𝒞 and G: ℬ -> 𝒟, the functor F × G: 𝒜 × ℬ -> 𝒞 × 𝒟 is defined by (F × G)(A,B) = (F(A),G(B)) and (F × G)(f,g) = (F(f),G(g)). 1_𝒜 is the identity functor on 𝒜 and α(1_𝒞 × J) and β(F × 1_ℰ) denote whiskering.

Definition. Let (T,μ,η) be a monad over some category 𝒞 and let (T',μ',η') be a monad over Alg(T). Let F ⊣ U be the adjunction induced by T and let F' ⊣ U' be the adjunction induced by T'. Define T * T' as the monad over 𝒞 induced by the adjunction F' ∘ F ⊣ U ∘ U'. ❀

More explicitely, T * T' maps an object X of 𝒞 to the carrier of the T-algebra T'(T(X),μ_X) and maps a morphism f to T'(T(f)).

Conjecture. Alg(T * T') ≃ Alg(T').