PS

Category of monads

圏論定義 Category Monad

Monoidal category

Monoidal category:

$(\mathcal{C}, \otimes, e, \alpha, \lambda, \rho)$

とは、

category: $\mathcal{C}$
bifunctor: $\otimes : \mathcal{C} \times \mathcal{C} \rightarrow \mathcal{C}$ (monoidal product)
$\mathcal{C}$ -object: $e$ (unit object)
natural isomorphism: $\big( \alpha _ {a, b, c} : (a \otimes b) \otimes c \cong a \otimes (b \otimes c) \big) _ {a, b, c}$ (associator)
natural isomorphism: $( \lambda _ a : e \otimes a \cong a ) _ a$ (left unitor)
natural isomorphism: $( \rho _ a : a \otimes e \cong a ) _ a$ (right unitor)

で、pentagon equalityとtriangle equalityを満たすもの。

Monoid object

上記のmonoidal categoryにおいて、monoid object:

$(m, \eta, \mu)$

とは、

$\mathcal{C}$ -object: $m$
$\mathcal{C}$ -morphism: $\eta : e \rightarrow m$ (unit)
$\mathcal{C}$ -morphism: $\mu : m \otimes m \rightarrow m$ (multiplication)

で、associative lawとunit lawを満たすもの。

Monoid morphism

二つのmonoid object:

$(m, \eta, \mu)$
$(m', \eta', \mu')$

について、

$f \circ \eta = \eta'$
$f \circ \mu = \mu' \circ (f \otimes f)$

を満たす $\mathcal{C}$ -morphism:

$f : m \rightarrow m'$

を、monoid morphismという。

Category of monoid objects

Objectをmonoid object、morphismをmonoid morphismとするcategory:

$\mathcal{Mon} _ \mathcal{C}$

を定義することが出来る。

Category of monads

Endofunctor category $\mathcal{B} ^ \mathcal{B}$ 上にmonoidal category:

$\big( \mathcal{B} ^ \mathcal{B}, \circ, 1 _ \mathcal{B}, (1 _ {F,G,H}) _ {F,G, H}, (1 _ F) _ F, (1 _ F) _F \big)$

を定義することが出来る。*1

このmonoidal category上のmonoid objectは、monadそのものである*2ので、

$\mathcal{Mnd}(\mathcal{B}) := \mathcal{Mon} _ { \mathcal{B} ^ \mathcal{B} }$

と定義する。特にこのとき、monoid morphismをmonad morphism*3という。

Free monad (official)

Monadのcategoryが出来たのでfree monadを定義できる。

Fogetful functor:

$U : \mathcal{Mnd}(\mathcal{B}) \rightarrow \mathcal{B} ^ \mathcal{B}$

について、 $U$ -initial morphism:

$\eta : F \rightarrow U(L)$

が存在するとき、 $L$ を、free monad for $F$ という。特に、その族:

$\big( \eta _ F : F \rightarrow U(L_ F) \big) _ F$

が存在すれば、Pointwise construction of adjoints - PS (のdual)により、

$L \dashv U$

Monad transformer

@deprecated

Endofunctor:

$t : \mathcal{Mnd}(\mathcal{B}) \rightarrow \mathcal{Mnd}(\mathcal{B})$

と、natural transformation:

$\big( \text{lift} _ m : m \rightarrow t(m) \big) _ {m \in \mathcal{Mnd}(\mathcal{B})}$

を合わせた代数的構造 $(t, \text{lift})$ を、monad transformerという(と思う)。*4

参考文献

*1:natural transformation間の $\circ$ はGodement product

*2:A monad is just a monoid in the category of endofunctors, what's the problem?

*3:natural transformation

*4:このようなendofunctorをpointed endofunctorというらしい