PS

Free monads are free

圏論命題 Monad

いわゆるfree monadは、確かに圏論的にもfreeである。

Free object

あるforgetful functor:

$U : \mathcal{D} \rightarrow \mathcal{C}$

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

$i : X \rightarrow U(A)$

のことを(特に代表して $A$ のことを)、free $\mathcal{D}$ -object over $X$ というのであった。

命題

category: $\mathcal{S}$
endofunctor: $F : \mathcal{S} \rightarrow \mathcal{S}$
forgetful functor: $U : \mathcal{Mnd}(\mathcal{S}) \rightarrow \mathcal{S} ^ \mathcal{S}$

について、Free monad - PSによって作られたmonadを

$\big( \mathtt{Free} _ F, (\mathtt{pure} _ a : a \rightarrow \mathtt{Free} _ F a ) _ a, (\mathtt{join} _ a : (\mathtt{Free} _ F) ^ 2 a \rightarrow \mathtt{Free} _ F a ) _ a \big)$

とすると、

$\big( \mathtt{lift} _ {F, a} := \mathtt{free} _ a \circ F(\mathtt{pure} _ a) : Fa \rightarrow U(\mathtt{Free} _ F)a \big) _ a$

は、 $U$ -initial morphism、つまりfree monad over $F$ 。

証明

任意のmonad $(M, \eta, \mu)$ について、

$( h _ a : \mathtt{Free} _F a \rightarrow Ma ) _ a \mapsto ( h _ a \circ \mathtt{lift} _ {F, a} : Fa \rightarrow Ma ) _ a$
$( g _ a : Fa \rightarrow Ma ) _ a \mapsto ( \mathtt{cata} (\eta _ a, \mu _ a \circ g _ {Ma}) : \mathtt{Free} _F a \rightarrow Ma ) _ a$

は、互いにinverse(と思うのだが･･･)。*1

Free monad functor

$U$ -initial morphismの族:

$\big( \mathtt{lift} _ F : F \rightarrow U(\mathtt{Free} _ F) \big) _ { F : \mathcal{S} \rightarrow \mathcal{S} }$

を作れたので、Pointwise construction of adjoints - PS (のdual)により

$\mathtt{Free} \dashv U$

参考文献

*1:より一般には、Beck's monadicity theoremというのを使うらしい