It is folklore knowledge that a pair of adjoint functors induces a monad and a comonad. Due to my recent work, I had to load relevant information into my brain cache. However, it turned out to be hard for me to find all the pieces of information I need in one place. Therefore, I am going to summarise here what I know and need, hoping it will be helpful for someone like me.
Adjoint Functors
Given categories C and D , we call two functors L : C → D and R : D → C a pair of adjoint functors if, for all object A in C and object B in D, we have the following natural isomorphism:
Hom (L A, B) ≅ Hom (A, R B)
This is denoted by L ⊣ R. Functors L and R are respectively called the left and the right adjoint.
Concepts such as Hom (A, B) and natural isomorphism will be explained in more detail later. For now, it suffices to say that Hom (A, B) is the collection of all morphisms from A to B. For an example, in Set (the category of sets and total functions), Hom (A, B) are all the functions having type A → B, and that Hom (L A, B) ≅ Hom (A, R B) can be understood as
L A → B ≅ A → R B
That is, given a function L A → B there is a unique corresponding function A → R B, and vice versa. A typical example is when L A = A × S and R B = S → B for some S. Indeed we have
(A × S) → B ≅ A → (S → B)
with the mapping from left-to-right being curry, and the reverse mapping being uncurry.
Note that Set is but an instance of a category (that is easier for me to understand). The notion of adjoint functors is much more general. For example, when the categories are such that the objects are elements of a partially ordered set, and there is a morphism a → b if a ≼ b (thus there is either zero or one morphism between any two objects), then L and R being adjoint functors means that they form a Galois connection.
That Hom (L A, B) and Hom (A, R B) being isomorphic means that there exists a pair of mappings ϕ : Hom (L A, B) → Hom (A, R B) and θ : Hom (A , R B) → Hom (L A, B), such that ϕ ∘ θ = id and θ ∘ ϕ = id. Being natural isomorphic refers to an additional constraint: that ϕ and θ must be natural with respect to A and B. This is an important property that will be explained and used later.
Monad and Comonad
If L : C → D and R : D → C form a pair of adjoint functors, R ∘ L is a monad, while L ∘ R is a comonad.
Recall the example L A = A × S and R B = S → B. Indeed, we have (R ∘ L) A = S → (A × S) — the type of state monad!
Merely having the type does not constitute a monad — we have got to construct the monad operators. In a more programming-oriented definition, a monad M : * → * comes with two operators return : A → M A and (>>=) : M A → (A → M B) → M B. In traditional, mathematics-oriented definition, a monad M comes with three operators: return, map : (A → B) → M A → M B, and join : M (M A) → M A — as a convention, return and join are often respectively written as η and μ. Dually, a comonad N comes with three operators: ε : N B → B, map : (A → B) → N A → N B, and δ : N B → N (N B).
As mentioned before, adjoint functors L and R induce a monad M = R ∘ L and a comonad N = L ∘ R. The operators η and ε are given by:
η : A → R (L A) η = ϕ id -- id : L A → L A ε : L (R B) → B ε = θ id -- id : R B → R B
The types of id are given in the comments. Operators μ and δ can then be defined by:
μ : R (L (R (L A))) → R (L A) μ = R ε δ : L (R B) → L (R (L (R B))) δ = L η
where η : R B → R (L (R B)) and ε : L (R (L A)) → L A.
The operators do have correct types. Do they satisfy the monad laws? There are six monad laws for for (M, η, μ):
M id = idM f ∘ M g = M (f ∘ g)η ∘ f = M f ∘ ηM f ∘ μ = μ ∘ M (M f)μ ∘ η = id = μ ∘ M ημ ∘ μ = μ ∘ M μ
The first two laws demand that M be a functor. Since L and R are functors, the two laws are immediately true. Laws 3 and 4 demands that η and μ be natural transformations, while Laws 5 and 6 are important computational rules for monads. We have got to check they do hold for the definitions of μ and η.
For comonads there is a collections of dual laws. Since the proofs are dual, we talk only about the laws for monads in this post.
Hom-Set and Hom-Functors
To prove the four remaining monad rules we need more properties about ϕ and θ. For that we give the concepts of hom-set and natural isomorphism, which we quickly skimmed through, a closer look.
The collection of all morphisms from A to B (both of them objects in category C) is denoted by Hom(A,B). (In general Hom(A,B) is not necessarily a set. When it happens to be a set, C is called a locally small category. See hom-set on ncatlab for details.)
Given category C, Hom is also a functor Cᵒᵖ × C → Set (where Cᵒᵖ denotes the dual category of C). It maps an object (c,d) (in Cᵒᵖ × C) to Hom(A,B), which is now an object in Set, and maps a pair of morphisms f : A₂ → A₁與g : B₁ → B₂ to a morphism Hom(A₁,B₁) → Hom(A₂, B₂) in Set, defined by
Hom : (A₂ → A₁ × B₁ → B₂) → Hom(A₁,B₁) → Hom(A₂, B₂) Hom (f,g) h = g ∘ h ∘ f
(The “type” given to Hom is not a rigorous notation, but to aid understanding. For more details, see hom-functor on ncatlab.)
Recall that, given functors F and G, when we say h : F → G is a natural transformation (from F to G), we mean that h is a series of morphisms — for each object A there is a morphism h : F A → G A, and for all f : A → B we have the following
h ∘ F f = G f ∘ h
The types of h on the left and right hand sides are respectively F B → G B and F A → G A.
Recall also that the definition of adjoint functors demands ϕ and θ be natural with respect to A and B. What we mean by being natural here is essentially the same, but slightly complicated by the fact that Hom is a more complex functor: for all f : A₂ → A₁ and g : B₁ → B₂, we want
ϕ ∘ Hom (L f, g) = Hom (f, R g) ∘ ϕ θ ∘ Hom (f, R g) = Hom (L f, g) ∘ θ
If we expanding the definition of Hom, apply both sides of the equation regarding ϕ to an argument h : L A₁ → B₁, and apply both sides of the equation regarding θ to an argument k : A₁ → R B₁, we get
ϕ (g ∘ h ∘ L f) = R g ∘ ϕ h ∘ f θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f
These naturality condition will be of crucial importance in the proofs later.
Proving the Monad Laws
Now we are ready to prove the monad laws 3-6:
3. η ∘ f = M f ∘ η:
R (L f) ∘ ϕ id
= { ϕ (g ∘ h ∘ L f) = R g ∘ ϕ h ∘ f, [g, h, f := L f, id, id] }
ϕ (L f ∘ id ∘ L id)
= ϕ (L f)
= ϕ (id ∘ id ∘ L f)
= { ϕ (g ∘ h ∘ L f) = R g ∘ ϕ h ∘ f, [g, h := id, id]}
ϕ id ∘ f
4. M f ∘ μ = μ ∘ M (M f)
R (θ id) ∘ (R (L (R (L f)))
= R (θ id ∘ L (R (L f)))
= { θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f, [g, k, f := id, id, R (L f)] }
R (θ (R id ∘ id, R (L f)))
= R (θ (R (L f)))
{ θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f, [g, k, f := L f, id, id] }
= R (L f ∘ θ id ∘ id)
= R (L f) ∘ R (θ id)
5.1 μ ∘ η = id
R (θ id) ∘ ϕ id
= { ϕ (g ∘ h ∘ L f) = R g ∘ ϕ h ∘ f, [g, h, f := θ id, id, id] }
ϕ (θ id ∘ id ∘ id)
= ϕ (θ id)
= { ϕ ∘ θ = id }
id
5.2 μ ∘ M η = id
R (θ id) ∘ R (L (ϕ id))
= R (θ id ∘ L (ϕ id))
= { θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f, [g, k, f := id, id, ϕ id] }
R (θ (R id ∘ id ∘ ϕ id))
= R (θ (ϕ id))
= { θ ∘ ϕ = id }
R id
= id .
6. μ ∘ μ = μ ∘ M μ
R (θ id) ∘ R (L (R (θ id)))
= R (θ id ∘ L (R (θ id)))
= { θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f, [g, k, f := id, id, R (θ id)] }
R (θ (R id ∘ id ∘ R (θ id)))
= R (θ (R (θ id)))
= { θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f, [g, k, f := θ id, id, id]}
R (θ id ∘ θ id)
= R (θ id) ∘ R (θ id)
The proofs above use only functor laws, the fact that ϕ and θ are inverses, and the naturality laws of ϕ and θ. Traditionally, the proofs would proceed by diagram chasing, which would probably be easier for those who familiar with them. I am personally happy about being able to construct these equational proofs, guided mostly by the syntax.
References
- adjoint functor on ncatlab.
- Anton Hilado, Adjoint Functors and Monads, June 20, 2017.
- Thorsten Wißmann, Adjunctions and monads. Seminar “Categories in Programming”, June 3, 2015.
- Steve Awodey, Monads and algebras. Course Notes of Category Theory, LMU Munich, Sommer Semester 2011.