PS

Universal associated adjunctions

圏論 Monad Adjunction

(･･･という用語は無いかもしれない)

任意のmonad:

$(T : \mathcal{C} \to \mathcal{C}, \eta, \mu)$

について･･･

Associated adjunction

$T = U F$
$\mu = U \epsilon F$

を満たすadjunction:

$F \overset{\epsilon}{ \underset{\eta}{\dashv} } U$

を、associated adjunction with $T$ というのであった。

Category of associated adjunctions

上記をobjectとするcategory:

$\mathcal{Adj}(T)$

をAdjunction category - PSと同様にして*1定義できる。

f:id:mbps:20140730170601p:plain

Terminal associated adjunction

Eilenberg-Moore adjunction - PS:

${\sf F} ^ T \overset{\epsilon ^ T} { \underset{\eta}{\dashv} } {\sf U} ^ T$

は $\mathcal{Adj}(T)$ のterminal object。

実際、任意のassociated adjunction with $T$ :

$F \overset{\epsilon}{ \underset{\eta}{\dashv} } U : \mathcal{D} \to \mathcal{C}$

について、comparison functor:

$K ^ T : \mathcal{D} \to \mathcal{C} ^ T$
$K ^ T(f: A \to B) := Uf : (UA, U \epsilon _ A) \to (UB, U \epsilon _ B)$ *2

がmediatorになる。

Initial associated adjunction

Kleisli adjunction - PS:

${\sf F} _ T \overset{\epsilon _ T}{ \underset{\eta}{\dashv} } {\sf U} _ T$

は $\mathcal{Adj}(T)$ のinitial object。

実際、任意のassociated adjunction with $T$ :

$F \overset{\epsilon}{ \underset{\eta}{\dashv} } U : \mathcal{D} \to \mathcal{C}$

について、functor:

$K _ T : \mathcal{C} _ T \to \mathcal{D}$
$K _ T(f _ T : C _ T \to D _ T) := \epsilon _ {FD} \circ Ff : FC \to FD$

がmediatorになる。

参考文献

*1:要件3は自明になる

*2:naturality square