PS

Adjunction lifting

Precomposition functor

Category  \mathcal{A} と functor  K : \mathcal{M} \to \mathcal{C} について、precomposition functor:

を定義できる。

命題

  • counit-adjunction:  (F \dashv K : \mathcal{M} \to \mathcal{C}, \epsilon)
  • category:  \mathcal{A}

について

  •  \big( (\unicode{x2013}) K \dashv (\unicode{x2013}) F : \mathcal{A} ^ {\mathcal{M}} \to \mathcal{A} ^ {\mathcal{C}},  (\unicode{x2013})\epsilon \big)

は counit-adjunction となる。ここで

は、 K-ran *3 の族である。

逆に、二つの  K-ran:

  •  \epsilon :  FK \Rightarrow 1_{\mathcal{M}}
  •  K \epsilon :  KFK \Rightarrow K

が存在するならば *4

  •  (F \dashv K, \epsilon)

は counit-adjunction となる。

  •  (F \dashv K, \epsilon) が counit-adjunction
    •  \iff \epsilon, K \epsilon が共に  K-ran

参考文献

*1:whiskering

*2:明らかにnatural

*3: (\unicode{x2013})K-terminal natural transfomation

*4:族は必ずしも必要ない