Monad
Collection
context | C … category |
definiendum | ⟨T,η,μ⟩ in it |
inclusion | T in CC |
inclusion | η:1C∙→T |
inclusion | μ:TT∙→T |
postulate | μ∘Tμ=μ∘μT |
postulate | μ∘Tη=μ∘ηT=1T |
Discussion
A monad is functor together with two natural transformations that fulfill some algebraic relations.
Elaboration
Written out in component form, the postulates read
- μX∘T(μX)=μX∘μTX
- μX∘T(ηX)=μX∘ηTX=1TX.
Picture the following chain of objects and notice that the axioms merely say the following: All ways ending up at TX must be the same.
XηX→TXT(ηTX) or ηTX→ μX←TTXT(μX) or μTX←TTTX
Alternative definition
From adjunctions
All monads arise by transferring some co-unit into the other category: Set T:=GF and μY:=G(εFY) and you got yourself a monad ⟨T,η,μ⟩.
Terminology/Notation
The forward arrows ηX are called „unit“ or, in programmer circles, „return“. The backwards arrows μX are called „join“ and from the counit-unit adjunction perspective, they are the arrow images of the functor applied to the „co-unit“ components.
Algebraic characterization
Recall that Set can be equipped with a monoidal structure where units are singletons (= final objects in Set, e.g. 1:={0}) and the product ⊗ can be taken to be the Cartesian product M⊗N:=M×N (= categorical product for Set). Here, a monoid object is a triple given by
M,
e:1→M,
∗:M×M→M.
Now a monad is given by
T,
η:1C∙→T,
μ:TT∙→T
and is also a monoid object, namely in the category of endofunctors CC, with the monoidal product ⊗ (not the categorical product) given by concatenation of functors S⊗T:=ST.
Reference
Wikipedia: Monad (category theory), Monade (Informatik)