[0065] 自然変換

自然変換は関手の間の射の概念である。実際、関手を対象、自然変換を射とする前圏を構成できる([0069])。さらに、終域が圏であるような関手のなす前圏は圏であることを示す([006C])。

$$i$$ を階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $F,G:\mathord {\textnormal {\textsf {Fun}}}(C,D)$ を関手とする。型 $\mathord {\textnormal {\textsf {NatTrans}}}(F,G):\mathcal {U}(i)$ を

\lbrace t:\prod _{x:C}\mathord {\textnormal {\textsf {Map}}}(F(x),G(x))\mid \forall _{x_{1},x_{2}:C}\forall _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}G(f)\circ t(x_{1})=t(x_{2})\circ F(f)\rbrace

と定義する。

\mathord {\textnormal {\textsf {NatTrans}}}(F,G)

の要素を

\(F\)

から

\(G\)

への自然変換(natural transformation)と呼ぶ。自然変換

t:\mathord {\textnormal {\textsf {NatTrans}}}(F,G)

が満たすべき性質(

\forall _{x_{1},x_{2}:C}\forall _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}G(f)\circ t(x_{1})=t(x_{2})\circ F(f)

)を

\(t\)

の自然性(naturality)と言う。

[0067] 演習

$$i$$ を階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏とする。

1関手 $F:\mathord {\textnormal {\textsf {Fun}}}(C,D)$ に対して、恒等自然変換 $\mathord {\textnormal {\textsf {id}}}\lbrace F\rbrace :\mathord {\textnormal {\textsf {NatTrans}}}(F,F)$ を $\lambda x.\mathord {\textnormal {\textsf {id}}}\lbrace F(x)\rbrace$ と定義する。 $\mathord {\textnormal {\textsf {id}}}\lbrace F\rbrace$ の自然性を確認せよ。
2関手 $F_{1},F_{2},F_{3}:\mathord {\textnormal {\textsf {Fun}}}(C,D)$ と自然変換 $t_{1}:\mathord {\textnormal {\textsf {NatTrans}}}(F_{1},F_{2})$ と $t_{2}:\mathord {\textnormal {\textsf {NatTrans}}}(F_{2},F_{3})$ に対して、合成 $t_{2}\circ t_{1}:\mathord {\textnormal {\textsf {NatTrans}}}(F_{1},F_{3})$ を $\lambda x.t_{2}(x)\circ t_{1}(x)$ と定義する。 $t_{2}\circ t_{1}$ の自然性を確認せよ。

[0068] 命題

関数外延性を仮定する。 $$i$$ を階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $F,G:\mathord {\textnormal {\textsf {Fun}}}(C,D)$ を関手、 $s,t:\mathord {\textnormal {\textsf {NatTrans}}}(F,G)$ を自然変換とすると、同値

(s=t)\simeq (\forall _{x:C}s(x)=t(x))

を構成できる。

[0069] 定義

関数外延性を仮定する。 $$i$$ を階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏とする。前圏 $\mathord {\textnormal {\textsf {Fun}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C,D):\mathord {\textnormal {\textsf {PreCat}}}(i)$ を次のように定義する。

- $\mathord {\textnormal {\textsf {Obj}}}\equiv \mathord {\textnormal {\textsf {Fun}}}(C,D)$
- $\mathord {\textnormal {\textsf {Map}}}\equiv \lambda (F,G).\mathord {\textnormal {\textsf {NatTrans}}}(F,G)$
-恒等射と合成は[0067]の通り。
-残りは[0068]から容易に示せる。

[006A] 命題

関数外延性を仮定する。 $$i$$ を階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $F,G:\mathord {\textnormal {\textsf {Fun}}}(C,D)$ を関手、 $t:\mathord {\textnormal {\textsf {NatTrans}}}(F,G)$ を自然変換とする。次は論理的に同値である。

1任意の $$x:C$$ に対して、 $t(x):\mathord {\textnormal {\textsf {Map}}}(F(x),G(x))$ は同型である。
2 $$t$$ は前圏 $\mathord {\textnormal {\textsf {Fun}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C,D)$ の射として同型である。

証明

2から1は自明である。

1から2を示す。各 $$x:C$$ に対して、射 $s(x),u(x):\mathord {\textnormal {\textsf {Map}}}(G(x),F(x))$ と同一視 $p(x):s(x)\circ t(x)=\mathord {\textnormal {\textsf {id}}}$ と $q(x):t(x)\circ u(x)=\mathord {\textnormal {\textsf {id}}}$ を得る。[0068]より、 $$s$$ と $$u$$ の自然性を確認すれば十分である。 $x_{1},x_{2}:C$ を対象、 $f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$ を射とする。 $F(f)\circ s(x_{1})=s(x_{2})\circ G(f)$ を言うには、[005G]より $F(f)\circ s(x_{1})\circ t(x_{1})=s(x_{2})\circ G(f)\circ t(x_{1})$ を示せば十分で、これは次のように分かる。

F(f)\circ s(x_{1})\circ t(x_{1})

\(=\)

{

p(x_{1})

}

\(F(f)\)

\(=\)

{

{(p(x_{2}))}^{-1}

}

s(x_{2})\circ t(x_{2})\circ F(f)

\(=\)

{

\(t\)

の自然性}

s(x_{2})\circ G(f)\circ t(x_{1})

\(u\)

の自然性も同様である。

[006C] 命題

関数外延性を仮定する。 $$i$$ を階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏とする。 $$D$$ が圏ならば、 $\mathord {\textnormal {\textsf {Fun}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C,D)$ は圏である。

証明

$F:\mathord {\textnormal {\textsf {Fun}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C,D)$ を対象とする。[006A]よりレトラクト $(\sum _{G:\mathord {\textnormal {\textsf {Fun}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C,D)}F\cong G)\triangleleft (\sum _{G:\mathord {\textnormal {\textsf {Fun}}}(C,D)}\lbrace t:\mathord {\textnormal {\textsf {NatTrans}}}(F,G)\mid \forall _{x:C}\mathord {\textnormal {\textsf {IsIso}}}(t(x))\rbrace )$ を得る。後者が可縮であることを示すには、[006B]より

\sum _{G_{0}:C.\mathord {\textnormal {\textsf {Obj}}}\to D.\mathord {\textnormal {\textsf {Obj}}}}\sum _{G_{1}:\prod _{\lbrace x_{1},x_{2}:C\rbrace }\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\to \mathord {\textnormal {\textsf {Map}}}(G_{0}(x_{1}),G_{0}(x_{2}))}\lbrace t:\prod _{x:C}F(x)\cong G_{0}(x)\mid \forall _{x_{1},x_{2}:C}\forall _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}G_{1}(f)\circ t(x_{1})=t(x_{2})\circ F(f)\rbrace

が可縮であることを示せばよい。

\sum _{G_{0}:C.\mathord {\textnormal {\textsf {Obj}}}\to D.\mathord {\textnormal {\textsf {Obj}}}}\prod _{x:C}F(x)\cong G_{0}(x)

の部分は

\prod _{x:C}\sum _{y:D}F(x)\cong y

のレトラクトなので、[0029]と

\(D\)

が圏であるという仮定から可縮である。よって、件の型は

\lbrace G_{1}:\prod _{\lbrace x_{1},x_{2}:C\rbrace }\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\to \mathord {\textnormal {\textsf {Map}}}(F(x_{1}),F(x_{2}))\mid \forall _{x_{1},x_{2}:C}\forall _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}G_{1}(f)\circ \mathord {\textnormal {\textsf {id}}}=\mathord {\textnormal {\textsf {id}}}\circ F(f)\rbrace

のレトラクトである。この型はさらに

\prod _{x_{1},x_{2}:C}\prod _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\lbrace g:\mathord {\textnormal {\textsf {Map}}}(F(x_{1}),F(x_{2}))\mid g=F(f)\rbrace

のレトラクトであるが、これは[0029]と[0026]より可縮である。

$\mathord {\textnormal {\textsf {Fun}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C,D)$ は普遍性でも特徴づけられる([006R])。

[006Q] 定義

$$i$$ を階数、 $C_{1},C_{2},D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏とする。型 $\mathord {\textnormal {\textsf {BiFun}}}(C_{1},C_{2};D):\mathcal {U}(i)$ を次のレコード型と定義する。

- $\mathord {\textnormal {\textsf {obj}}}:C_{1}.\mathord {\textnormal {\textsf {Obj}}}\to C_{2}.\mathord {\textnormal {\textsf {Obj}}}\to D.\mathord {\textnormal {\textsf {Obj}}}$
- $\mathord {\textnormal {\textsf {map}}}_{1}:\prod _{\lbrace x_{11},x_{12}:C_{1}\rbrace }\mathord {\textnormal {\textsf {Map}}}(x_{11},x_{12})\to (\prod _{x_{2}:C_{2}}\mathord {\textnormal {\textsf {Map}}}(\mathord {\textnormal {\textsf {obj}}}(x_{11},x_{2}),\mathord {\textnormal {\textsf {obj}}}(x_{12},x_{2})))$
- $\mathord {\textnormal {\textsf {map}}}_{2}:\prod _{x_{1}:C_{1}}\prod _{\lbrace x_{21},x_{22}:C_{2}\rbrace }\mathord {\textnormal {\textsf {Map}}}(x_{21},x_{22})\to \mathord {\textnormal {\textsf {Map}}}(\mathord {\textnormal {\textsf {obj}}}(x_{1},x_{21}),\mathord {\textnormal {\textsf {obj}}}(x_{1},x_{22}))$
- $\_:\forall _{x_{1}:C_{1}}\forall _{x_{2}:C_{2}}\mathord {\textnormal {\textsf {map}}}_{1}(\mathord {\textnormal {\textsf {id}}}\lbrace x_{1}\rbrace ,x_{2})=\mathord {\textnormal {\textsf {id}}}\lbrace \mathord {\textnormal {\textsf {obj}}}(x_{1},x_{2})\rbrace$
- $\_:\forall _{x_{11},x_{12},x_{13}:C_{1}}\forall _{x_{2}:C_{2}}\forall _{f_{1}:\mathord {\textnormal {\textsf {Map}}}(x_{11},x_{12})}\forall _{f_{2}:\mathord {\textnormal {\textsf {Map}}}(x_{12},x_{13})}\mathord {\textnormal {\textsf {map}}}_{1}(f_{2}\circ f_{1},x_{2})=\mathord {\textnormal {\textsf {map}}}_{1}(f_{2},x_{2})\circ \mathord {\textnormal {\textsf {map}}}_{1}(f_{1},x_{2})$
- $\_:\forall _{x_{1}:C_{1}}\forall _{x_{2}:C_{2}}\mathord {\textnormal {\textsf {map}}}_{2}(x_{1},\mathord {\textnormal {\textsf {id}}}\lbrace x_{2}\rbrace )=\mathord {\textnormal {\textsf {id}}}\lbrace \mathord {\textnormal {\textsf {obj}}}(x_{1},x_{2})\rbrace$
- $\_:\forall _{x_{1}:C_{1}}\forall _{x_{21},x_{22},x_{23}:C_{2}}\forall _{f_{1}:\mathord {\textnormal {\textsf {Map}}}(x_{21},x_{22})}\forall _{f_{2}:\mathord {\textnormal {\textsf {Map}}}(x_{22},x_{23})}\mathord {\textnormal {\textsf {map}}}_{2}(x_{1},f_{2}\circ f_{1})=\mathord {\textnormal {\textsf {map}}}_{2}(x_{1},f_{2})\circ \mathord {\textnormal {\textsf {map}}}_{2}(x_{1},f_{1})$
- $\_:\forall _{x_{11},x_{12}:C_{1}}\forall _{x_{21},x_{22}:C_{2}}\forall _{f_{1}:\mathord {\textnormal {\textsf {Map}}}(x_{11},x_{12})}\forall _{f_{2}:\mathord {\textnormal {\textsf {Map}}}(x_{21},x_{22})}\mathord {\textnormal {\textsf {map}}}_{1}(f_{1},x_{22})\circ \mathord {\textnormal {\textsf {map}}}_{2}(x_{11},f_{2})=\mathord {\textnormal {\textsf {map}}}_{2}(x_{12},f_{2})\circ \mathord {\textnormal {\textsf {map}}}_{1}(f_{1},x_{21})$

\mathord {\textnormal {\textsf {BiFun}}}(C_{1},C_{2};D)

の要素を

C_{1},C_{2}

から

\(D\)

への双関手(bifunctor)と呼ぶ。

[006R] 演習

関数外延性を仮定する。 $$i$$ を階数、 $C,D,X:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏とする。同値

\mathord {\textnormal {\textsf {Fun}}}(X,\mathord {\textnormal {\textsf {Fun}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C,D))\simeq \mathord {\textnormal {\textsf {BiFun}}}(C,X;D)

を構成せよ。