随伴系
Adjunction.sig2-signature <Adjunction: c, d; l, r; ε, η>
fixed-in CAT
Data
0-morph c
0-morph d
1-morph leftAdjoint @ l : c -> d
1-morph rightAdjoint @ r : d -> c
2-morph unit @ η
: c^ => l * r
: c -> c
2-morph counit @ ε
: r * l => d^
: d -> d
Axioms
3-eq snaky-1
: (η * l^); (l^ * ε) =3= l^
: l => l
: c -> d
3-eq snaky-2
: (r^ * η); (ε * r^) =3= r^
: r => r
: d -> c=\left\lang\mathrm{ Adjunction }\colon C, D;L,R;η,ε\right\rang
0-morph
C, D \colon \mathbf{CAT}
1-morph
L\colon C\to D,R\colon D\to C
左右はここで決めてしまう
2-morph
\eta \colon C^\wedge \Rightarrow L*R
\varepsilon\colon R*L \Rightarrow D^\wedge
公理系
ニョロニョロ公理 (snaky)
\eta * L ; L * \varepsilon = L^\wedge
R*\eta ; \varepsilon * R = R^\wedge
用語
命題としてL \dashv R⇔
{}^\exist \eta,{}^\exist \epsilon,\left\lang L\dashv R \colon C→D, \eta, \epsilon \right \rangが随伴系となる
Lが右随伴(函手)をもつ⇔
{}^\exist R,L\dashv R
Rが左随伴(函手)をもつ⇔
{}^\exist L,L\dashv R
性質
ホムセット自然同型、転置、反転置
随伴系の定義から以下を得る
ホムセット自然同型
\Phi \colon \hom_D(\_.L,\_) \Rightarrow \hom_C(\_,\_.R)
\colon C^\mathrm{op}× D \to \mathbf{Set}
その適用の添え字を省略したものが
転置オペレーター
\_^\cap \coloneqq (c,d).\Phi
\colon \hom_D(c.L,d) → \hom_C(c,d.R)
反転置オペレーター
\__{\cup} \coloneqq (c,d).\Phi^{-1} =(\_^{\cap})^{-1}
\colon \hom_C(c,d.R) → \hom_D(c.L,d)
具体的には
g\colon c.L→dについて
g^\cap= c.\eta;g.R
f\colon c→d.Rについて
f_\cup = f.L;d.\epsilon
この自然性がニョロニョロ方程式と同値になる
随伴系の構成
定義と同値な命題がいくつかある
\left\lang d.R, d.\varepsilon \right\rangが普遍射になる
L\dashv RかつL'\dashv R'のとき
L\cong L'\iffR\cong R'
とくに
L\dashv RかつL\dashv R'ならばR\cong R'
L\dashv RかつL'\dashv RならばL\cong L'