[006D] 前層

圏にとっての前層は、群にとっての作用、環にとっての加群に相当するものである。

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

- $\mathord {\textnormal {\textsf {Carrier}}}:C.\mathord {\textnormal {\textsf {Obj}}}\to \mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {act}}}:\prod _{\lbrace x_{1},x_{2}:C\rbrace }\mathord {\textnormal {\textsf {Carrier}}}(x_{2})\to \mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\to \mathord {\textnormal {\textsf {Carrier}}}(x_{1})$
- $\_:\forall _{x:C}\mathord {\textnormal {\textsf {IsSet}}}(\mathord {\textnormal {\textsf {Carrier}}}(x))$
- $\_:\forall _{x:C}\forall _{a:\mathord {\textnormal {\textsf {Carrier}}}(x)}\mathord {\textnormal {\textsf {act}}}(a,\mathord {\textnormal {\textsf {id}}})=a$
- $\_:\forall _{x_{1},x_{2},x_{3}:C}\forall _{f_{1}:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\forall _{f_{2}:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{3})}\forall _{a:\mathord {\textnormal {\textsf {Carrier}}}(x_{3})}\mathord {\textnormal {\textsf {act}}}(a,f_{2}\circ f_{1})=\mathord {\textnormal {\textsf {act}}}(\mathord {\textnormal {\textsf {act}}}(a,f_{2}),f_{1})$

\mathord {\textnormal {\textsf {Psh}}}(C)

の要素を

\(C\)

上の前層(presheaf)と呼ぶ。

[006F] 記法

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

-対象 $$x:C$$ に対して、 $A.\mathord {\textnormal {\textsf {Carrier}}}(x)$ の代わりに単に $$A(x)$$ と書く。
-対象 $x_{1},x_{2}:C$ と射 $f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$ と要素 $a:A(x_{2})$ に対して、要素 $a\cdot f:A(x_{1})$ を $A.\mathord {\textnormal {\textsf {act}}}(a,f)$ と定義する。

つまり、 $$C$$ 上の前層は $$C$$ の対象で添え字付けられた集合の族で、 $$C$$ の射が右から作用しているものである。

[006G] 定義

$$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $A,B:\mathord {\textnormal {\textsf {Psh}}}(C)$ を前層とする。型 $\mathord {\textnormal {\textsf {Hom}}}(A,B):\mathcal {U}(i)$ を

\lbrace h:\prod _{\lbrace x:C\rbrace }A(x)\to B(x)\mid \forall _{x_{1},x_{2}:C}\forall _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\forall _{a:A(x_{2})}h(a\cdot f)=h(a)\cdot f\rbrace

と定義する。

\mathord {\textnormal {\textsf {Hom}}}(A,B)

の要素を前層の射(morphism of presheaves)と呼ぶ。

[006L] 演習

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

1前層 $A:\mathord {\textnormal {\textsf {Psh}}}(C)$ に対して、前層の射 $\mathord {\textnormal {\textsf {id}}}\lbrace A\rbrace :\mathord {\textnormal {\textsf {Hom}}}(A,A)$ を $\lambda x.\mathord {\textnormal {\textsf {id}}}\lbrace A(x)\rbrace$ と定義する。これが前層の射の公理を満たすことを確かめよ。
2前層 $A_{1},A_{2},A_{3}:\mathord {\textnormal {\textsf {Psh}}}(C)$ と前層の射 $f_{1}:\mathord {\textnormal {\textsf {Hom}}}(A_{1},A_{2})$ と $f_{2}:\mathord {\textnormal {\textsf {Hom}}}(A_{2},A_{3})$ に対して、前層の射 $f_{2}\circ f_{1}:\mathord {\textnormal {\textsf {Hom}}}(A_{1},A_{3})$ を $\lambda x.f_{2}\lbrace x\rbrace \circ f_{1}\lbrace x\rbrace$ と定義する。これが前層の射の公理を満たすことを確かめよ。

前層と前層の射は前圏をなし、関手のなす前圏としても定義できる([006M])。

[006K] 定義

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

- $\mathord {\textnormal {\textsf {Obj}}}\equiv \mathord {\textnormal {\textsf {Psh}}}(C)$
- $\mathord {\textnormal {\textsf {Map}}}\equiv \lambda (A,B).\mathord {\textnormal {\textsf {Hom}}}(A,B)$
-恒等射と合成は[006L]の通りである。
-前圏の公理は関数外延性から分かる。

[006M] 演習

関数外延性を仮定する。 $$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏とする。 $\mathord {\textnormal {\textsf {Psh}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C)$ と $\mathord {\textnormal {\textsf {Fun}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(\mathord {\textnormal {\textsf {Op}}}(C),\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i))$ の間の前圏の同型を構成せよ。

[006O] 系

関数外延性と一価性を仮定する。 $$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏とすると、 $\mathord {\textnormal {\textsf {Psh}}}(C)$ は圏である。

[0072] 系

関数外延性を仮定する。 $$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $A,B:\mathord {\textnormal {\textsf {Psh}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C)$ を前層、 $f:\mathord {\textnormal {\textsf {Map}}}(A,B)$ を射とする。次は論理的に同値である。

1 $$f$$ は $\mathord {\textnormal {\textsf {Psh}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C)$ の射として同型である。
2任意の対象 $$x:C$$ に対して、関数 $\lambda a.f(a):A(x)\to B(x)$ は同値である。

さて、圏論において最も重要な米田の補題([006T])を導入する。

[006S] 定義

$$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏とする。 $\mathord {\textnormal {\textsf {Map}}}^{(\mathord {\textnormal {\textsf {Fun}}})}(C):\mathord {\textnormal {\textsf {BiFun}}}(\mathord {\textnormal {\textsf {Op}}}(C),C;\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i))$ を次のように定義する。

- $\mathord {\textnormal {\textsf {obj}}}\equiv \lambda (x_{1},x_{2}).\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$
- $\mathord {\textnormal {\textsf {map}}}_{1}\equiv \lambda (x_{11},x_{12},f,x_{2}).\lambda h.h\circ f$
- $\mathord {\textnormal {\textsf {map}}}_{2}\equiv \lambda (x_{1},x_{21},x_{22},f).\lambda h.f\circ h$

[006P] 定義

関数外延性を仮定する。 $$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏とする。米田埋め込み(Yoneda embedding) $\mathord {\textnormal {\textsf {よ}}}(C):\mathord {\textnormal {\textsf {Fun}}}(C,\mathord {\textnormal {\textsf {Psh}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C))$ を[006R]と[006M]で $\mathord {\textnormal {\textsf {Map}}}^{(\mathord {\textnormal {\textsf {Fun}}})}(C)$ に対応するものと定義する。

$\mathord {\textnormal {\textsf {よ}}}(C)$ が埋め込みと呼ばれるのは[006V]による。定義から、任意の対象 $$x,y:C$$ に対して $\mathord {\textnormal {\textsf {よ}}}(C)(x)(y)\equiv \mathord {\textnormal {\textsf {Map}}}(y,x)$ である。特に、 $\mathord {\textnormal {\textsf {id}}}:\mathord {\textnormal {\textsf {Map}}}(x,x)$ は $\mathord {\textnormal {\textsf {よ}}}(C)(x)(x)$ の要素とも思える。 $\mathord {\textnormal {\textsf {id}}}$ をどのように見ているかを区別するために別の表記を導入する。

[006U] 記法

関数外延性を仮定する。 $$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $$x:C$$ を対象とする。要素 $\mathord {\textnormal {\textsf {gen}}}(x):\mathord {\textnormal {\textsf {よ}}}(C)(x)(x)$ を $\mathord {\textnormal {\textsf {id}}}\lbrace x\rbrace$ と定義する。

米田の補題が主張するのは、 $\mathord {\textnormal {\textsf {よ}}}(C)(x)$ は $\mathord {\textnormal {\textsf {gen}}}(x):\mathord {\textnormal {\textsf {よ}}}(C)(x)(x)$ で自由に生成された $$C$$ 上の前層であることである。

[006T] 定理

関数外延性を仮定する。 $$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $$x:C$$ を対象、 $A:\mathord {\textnormal {\textsf {Psh}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C)$ を前層とする。関数

\lambda h.h(\mathord {\textnormal {\textsf {gen}}}(x)):\mathord {\textnormal {\textsf {Map}}}(\mathord {\textnormal {\textsf {よ}}}(C)(x),A)\to A(x)

は同値である。

証明

射 $h:\mathord {\textnormal {\textsf {Map}}}(\mathord {\textnormal {\textsf {よ}}}(C)(x),A)$ と対象 $$y:C$$ と要素 $f:\mathord {\textnormal {\textsf {よ}}}(C)(x)(y)$ に対して、同一視

\(h(f)\)

\(=\)

{前圏の公理}

h(\mathord {\textnormal {\textsf {gen}}}(x)\cdot f)

\(=\)

{前層の公理}

h(\mathord {\textnormal {\textsf {gen}}}(x))\cdot f

を得るので、

\(h\)

は

\mathord {\textnormal {\textsf {gen}}}(x)

における値のみで決まる。つまり、任意の要素

\(a:A(x)\)

に対して、

\mathord {\textnormal {\textsf {Fiber}}}(\lambda h.h(\mathord {\textnormal {\textsf {gen}}}(x)),a)

は命題であることが分かる。この型が要素を持つことを確認するには、

\lambda (y,f).a\cdot f:\prod _{y:C}\mathord {\textnormal {\textsf {よ}}}(C)(x)(y)\to A(y)

が前層の射であることを確かめればよいが、それは前層の公理から容易である。

[006V] 系

関数外延性を仮定する。 $$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏とする。米田埋め込み $\mathord {\textnormal {\textsf {よ}}}(C):\mathord {\textnormal {\textsf {Fun}}}(C,\mathord {\textnormal {\textsf {Psh}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C))$ は充満忠実である。

証明

$x_{1},x_{2}:C$ を対象とする。関数 $\lambda f.\mathord {\textnormal {\textsf {よ}}}(C)(f):\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\to \mathord {\textnormal {\textsf {Map}}}(\mathord {\textnormal {\textsf {よ}}}(C)(x_{1}),\mathord {\textnormal {\textsf {よ}}}(C)(x_{2}))$ と $\lambda h.h(\mathord {\textnormal {\textsf {gen}}}(x_{1})):\mathord {\textnormal {\textsf {Map}}}(\mathord {\textnormal {\textsf {よ}}}(C)(x_{1}),\mathord {\textnormal {\textsf {よ}}}(C)(x_{2}))\to \mathord {\textnormal {\textsf {よ}}}(C)(x_{2})(x_{1})$ の合成は $\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$ 上の恒等関数と同一であることが分かる。よって、[002E]と[006T]から $\lambda f.\mathord {\textnormal {\textsf {よ}}}(C)(f)$ は同値である。

多くの圏論的な概念は、ある前層が表現可能であるという性質で定義される。

[0070] 定義

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

- $\mathord {\textnormal {\textsf {obj}}}:C$
- $\mathord {\textnormal {\textsf {elem}}}:A(\mathord {\textnormal {\textsf {obj}}})$
- $\_:\forall _{x:C}\mathord {\textnormal {\textsf {IsEquiv}}}(\lambda (f:\mathord {\textnormal {\textsf {Map}}}(x,\mathord {\textnormal {\textsf {obj}}})).\mathord {\textnormal {\textsf {elem}}}\cdot f)$

\mathord {\textnormal {\textsf {IsRepr}}}(A)

の要素がある時、

\(A\)

は表現可能(representable)であると言う。また、

\mathord {\textnormal {\textsf {IsRepr}}}(A)

の要素のことを

\(A\)

の普遍要素(universal element)と呼ぶ。

従来の圏論では、 $$C$$ 上の前層 $$A$$ の普遍要素は「同型を除いて一意」であることが知られている。ホモトピー型理論においては、 $$C$$ が圏と仮定して普遍要素は一意であること、つまり $\mathord {\textnormal {\textsf {IsRepr}}}(A)$ は命題であることが分かる([0073])。

[0071] 補題

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

\mathord {\textnormal {\textsf {IsRepr}}}(A)\simeq \mathord {\textnormal {\textsf {Fiber}}}^{\cong }(\mathord {\textnormal {\textsf {よ}}}(C),A)

を構成できる。

証明

[006T]と[0072]から従う。

[0073] 命題

関数外延性を仮定する。 $$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $A:\mathord {\textnormal {\textsf {Psh}}}(C)$ を前層とする。 $$C$$ が圏ならば、 $\mathord {\textnormal {\textsf {IsRepr}}}(A)$ は命題である。

証明

[0071]と[006V]と[006Z]から従う。