随伴系 - 雑多な感じ

随伴系

adjunction

adjoint system

signature.icon

code:Adjunction.sig

2-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

definition.icon随伴系 $ \Sigma = \left\lang L\dashv R \colon C→D, \eta, \epsilon \right\rang

$ =\left\lang\mathrm{ Adjunction }\colon C, D;L,R;η,ε\right\rang

0-morph

$ C, D \colon \mathbf{CAT}

1-morph

随伴対 adjoint pair

$ L\colon C\to D ,$ R\colon D\to C

それぞれ左随伴函手、右随伴函手と呼ぶ

左右はここで決めてしまう

2-morph

単位 unit

$ \eta \colon C^\wedge \Rightarrow L*R

余単位 counit

$ \varepsilon\colon R*L \Rightarrow D^\wedge

https://gyazo.com/35e0d9dc19a2b3c65de3ae1a0614015ehttps://gyazo.com/99018dee6e3f9c2ec0a91b8f61ea4216

1-2図式

https://gyazo.com/c0e62b224b8e489bc062e4273903204ahttps://gyazo.com/a0ef2d287f60483d3d67035aff85d76a

公理系

ニョロニョロ公理 (snaky)

$ \eta * L ; L * \varepsilon = L^\wedge

$ R*\eta ; \varepsilon * R = R^\wedge

https://gyazo.com/0d1581481fa2eaa0554c347a4fe074a7https://gyazo.com/f9763ac5fb517b3152578b4897b25fa0

https://gyazo.com/c22911e6f2609c697893c8fd26cac48bhttps://gyazo.com/41bf8501a9e08874f98ae063d117dfbd

用語

命題として$ 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 を「$ L の右随伴函手」と呼ぶ

$ R が左随伴(函手)をもつ⇔

$ {}^\exist L ,$ L\dashv R

$ L を「$ R の左随伴函手」と呼ぶ

性質

ホムセット自然同型、転置、反転置

随伴系の定義から以下を得る

ホムセット自然同型

hom自然同型

$ \Phi \colon \hom_D(\_.L,\_) \Rightarrow \hom_C(\_,\_.R)

$ \colon C^\mathrm{op}× D \to \mathbf{Set}

dragoon8192.iconCATを2-圏, 豊穣圏とした方が……

その適用の添え字を省略したものが

転置オペレーター

$ \_^\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

https://gyazo.com/e2f7ec430df3ac05b53a9e15ebe7fdf2

この自然性がニョロニョロ方程式と同値になる

随伴系のhom自然同型の構成

随伴系の構成

定義と同値な命題がいくつかある

$ \left\lang d.R, d.\varepsilon \right\rang が普遍射になる

随伴系の同型を除いた一意性

$ L\dashv R かつ$ L'\dashv R' のとき

$ L\cong L' $ \iff $ R\cong R'

とくに

$ L\dashv R かつ$ L\dashv R' ならば$ R\cong R'

$ L\dashv R かつ$ L'\dashv R ならば$ L\cong L'

ref.iconscrap:圏論の随伴をちゃんと抑えよう

ref.iconscrap:随伴関手 - 壱大整域