[005J] 関手

関手は前圏の間の構造を保つ関数である。

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

- $\mathord {\textnormal {\textsf {obj}}}:C.\mathord {\textnormal {\textsf {Obj}}}\to D.\mathord {\textnormal {\textsf {Obj}}}$
- $\mathord {\textnormal {\textsf {map}}}:\prod _{\lbrace x_{1},x_{2}:C.\mathord {\textnormal {\textsf {Obj}}}\rbrace }C.\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\to D.\mathord {\textnormal {\textsf {Map}}}(\mathord {\textnormal {\textsf {obj}}}(x_{1}),\mathord {\textnormal {\textsf {obj}}}(x_{2}))$
- $\_:\prod _{x:C.\mathord {\textnormal {\textsf {Obj}}}}\mathord {\textnormal {\textsf {map}}}(C.\mathord {\textnormal {\textsf {id}}}(x))=D.\mathord {\textnormal {\textsf {id}}}(\mathord {\textnormal {\textsf {obj}}}(x))$
- $\_:\prod _{x_{1},x_{2},x_{3}:C.\mathord {\textnormal {\textsf {Obj}}}}\prod _{f_{1}:C.\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\prod _{f_{2}:C.\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{3})}\mathord {\textnormal {\textsf {map}}}(C.\mathord {\textnormal {\textsf {comp}}}(f_{2},f_{1}))=D.\mathord {\textnormal {\textsf {comp}}}(\mathord {\textnormal {\textsf {map}}}(f_{2}),\mathord {\textnormal {\textsf {map}}}(f_{1}))$

\mathord {\textnormal {\textsf {Fun}}}(C,D)

の要素を

\(C\)

から

\(D\)

への関手(functor)と呼ぶ。

[005L] 記法

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

-対象 $$x:C$$ に対して、 $F.\mathord {\textnormal {\textsf {obj}}}(x):D$ の代わりに単に $$F(x)$$ と書く。
-対象 $x_{1},x_{2}:C$ と射 $f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$ に対して、 $F.\mathord {\textnormal {\textsf {map}}}(f):\mathord {\textnormal {\textsf {Map}}}(F(x_{1}),F(x_{2}))$ の代わりに単に $$F(f)$$ と書く。

[0060] 演習

$$i$$ 階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $F:\mathord {\textnormal {\textsf {Fun}}}(C,D)$ を関手、 $x_{1},x_{2}:C$ を対象、 $f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$ を射とする。 $$f$$ が同型ならば、 $$F(f)$$ は同型であることを示せ。

[0022]や[004V]と同様に、前圏の構造同一原理が得られる。

[005M] 定義

$$i$$ を階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $F:\mathord {\textnormal {\textsf {Fun}}}(C,D)$ を関手とする。型 $\mathord {\textnormal {\textsf {IsIso}}}(F):\mathcal {U}(i)$ を次のレコード型と定義する。

- $\_:\mathord {\textnormal {\textsf {IsEquiv}}}(F.\mathord {\textnormal {\textsf {obj}}})$
- $\_:\prod _{x_{1},x_{2}:C}\mathord {\textnormal {\textsf {IsEquiv}}}(F.\mathord {\textnormal {\textsf {map}}}\lbrace x_{1},x_{2}\rbrace )$

\mathord {\textnormal {\textsf {IsIso}}}(F)

の要素がある時、

\(F\)

は前圏の同型(isomorphism of precategories)であると言う。

[005N] 演習(前圏の構造同一原理)

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

(C=D)\simeq \lbrace F:\mathord {\textnormal {\textsf {Fun}}}(C,D)\mid \mathord {\textnormal {\textsf {IsIso}}}(F)\rbrace

を構成せよ。

従来の圏論においては、[005M]は圏の同一視の概念としては強過ぎて、次の弱圏同値こそが「正しい」圏の同一視の概念とされる。

[005O] 定義

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

-型 $\mathord {\textnormal {\textsf {IsFF}}}(F):\mathcal {U}(i)$ を $\forall _{x_{1},x_{2}:C}\mathord {\textnormal {\textsf {IsEquiv}}}(F.\mathord {\textnormal {\textsf {map}}}\lbrace x_{1},x_{2}\rbrace )$ と定義する。 $\mathord {\textnormal {\textsf {IsFF}}}(F)$ の要素がある時、 $$F$$ は充満忠実(fully faithful)であると言う。
-型 $\mathord {\textnormal {\textsf {IsEssSurj}}}(F):\mathcal {U}(i)$ を $\forall _{y:D}\exists _{x:C}F(x)\cong y$ と定義する。 $\mathord {\textnormal {\textsf {IsEssSurj}}}(F)$ の要素がある時、 $$F$$ は本質的全射(essentially surjective)であると言う。
-型 $\mathord {\textnormal {\textsf {IsWCatEquiv}}}(F):\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {IsFF}}}(F)\land \mathord {\textnormal {\textsf {IsEssSurj}}}(F)$ と定義する。 $\mathord {\textnormal {\textsf {IsWCatEquiv}}}(F)$ の要素がある時、 $$F$$ は弱圏同値(weak categorical equivalence)であると言う。

ホモトピー型理論での圏論では、圏の間の関手が前圏の同型であることと弱圏同値であることは同値であることに差はなくなる([005P])。[005N]と合わせると、圏の間に弱圏同値があればそれらの圏は同一視される([0064])。よって、弱圏同値が正しい同一視の概念であることが厳密な定理として得られる。

[0061] 演習

$$i$$ を階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $F:\mathord {\textnormal {\textsf {Fun}}}(C,D)$ を関手、 $x_{1},x_{2}:C$ を対象、 $f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$ を射とする。 $$F$$ は充満忠実であると仮定する。 $$F(f)$$ が同型ならば $$f$$ は同型であることを示せ。

[006Y] 定義

$$i$$ を階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $F:\mathord {\textnormal {\textsf {Fun}}}(C,D)$ を関手、 $$y:D$$ を対象とする。型 $\mathord {\textnormal {\textsf {Fiber}}}^{\cong }(F,y):\mathcal {U}(i)$ を次のレコード型と定義する。

- $\mathord {\textnormal {\textsf {obj}}}:C$
- $\mathord {\textnormal {\textsf {iso}}}:F(\mathord {\textnormal {\textsf {obj}}})\cong y$

[006Z] 補題

$$i$$ を階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $F:\mathord {\textnormal {\textsf {Fun}}}(C,D)$ を関手、 $$y:D$$ を対象とする。 $$C$$ が圏で、 $$F$$ が充満忠実ならば、 $\mathord {\textnormal {\textsf {Fiber}}}^{\cong }(F,y)$ は命題である。

証明

[0041]を適用し、 $a:\mathord {\textnormal {\textsf {Fiber}}}^{\cong }(F,y)$ を仮定して $\mathord {\textnormal {\textsf {Fiber}}}^{\cong }(F,y)$ が可縮であることを示す。レトラクト

\mathord {\textnormal {\textsf {Fiber}}}^{\cong }(F,y)

\triangleleft

{定義}

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

\triangleleft

{

a.\mathord {\textnormal {\textsf {iso}}}

と合成}

\sum _{x:C}F(a.\mathord {\textnormal {\textsf {obj}}})\cong F(x)

\triangleleft

{[0060]と[0061]}

\sum _{x:C}a.\mathord {\textnormal {\textsf {obj}}}\cong x

を得て、最後の型は

\(C\)

が圏なので可縮である。

[0063] 補題

$$i$$ を階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $F:\mathord {\textnormal {\textsf {Fun}}}(C,D)$ を関手とする。 $$C$$ と $$D$$ が圏で、 $$F$$ が充満忠実ならば、 $F.\mathord {\textnormal {\textsf {obj}}}:C.\mathord {\textnormal {\textsf {Obj}}}\to D.\mathord {\textnormal {\textsf {Obj}}}$ は埋め込みである。

証明

$$y:D$$ を対象とする。 $$D$$ が圏であることから、 $\mathord {\textnormal {\textsf {Fiber}}}(F.\mathord {\textnormal {\textsf {obj}}},y)$ は $\mathord {\textnormal {\textsf {Fiber}}}^{\cong }(F,y)$ のレトラクトであることが分かる。後者は[006Z]より命題である。

[0075] 補題

$$i$$ を階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $F:\mathord {\textnormal {\textsf {Fun}}}(C,D)$ を関手とする。 $$D$$ が圏で、 $$F$$ が本質的全射ならば、 $F.\mathord {\textnormal {\textsf {obj}}}:C.\mathord {\textnormal {\textsf {Obj}}}\to D.\mathord {\textnormal {\textsf {Obj}}}$ は全射である。

証明

定義からすぐである。

[005P] 定理

$$i$$ を階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $F:\mathord {\textnormal {\textsf {Fun}}}(C,D)$ を関手とする。 $$C$$ と $$D$$ が圏ならば、次は論理的に同値である。

1 $$F$$ は前圏の同型である。
2 $$F$$ は弱圏同値である。

証明

1から2は自明である。

2から1を示す。 $F.\mathord {\textnormal {\textsf {obj}}}:C.\mathord {\textnormal {\textsf {Obj}}}\to D.\mathord {\textnormal {\textsf {Obj}}}$ が同値であることを示せばよいが、これは[005X]と[0063]と[0074]と[0075]から従う。

[0064] 系(圏の構造同一原理)

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

(C=D)\simeq \lbrace F:\mathord {\textnormal {\textsf {Fun}}}(C,D)\mid \mathord {\textnormal {\textsf {IsWCatEquiv}}}(F)\rbrace

を得る。