豊穣圏の導入 第1回: 集合の圏は有限積をもつ
導入
素朴集合論の基礎 (集合と写像，空集合など) に親しみがあり，圏の定義を知っていることを仮定する．また，この記事を通して，以下の記法を用いる (主に [1] で扱われているものを採用している):
- 空集合 (empty set) を$\es$で表す．
- $x,y$に対して，$x$と$y$の対 (pair) $(x,y)$を$(x,y):=\{\{x\},\{x,y\}\}$で定める．$x,x',y,y'$に対して，$(x,y)=(x',y')$ならば，$x=x'$かつ$y=y'$が成り立つことが知られている．
- 圏 (category) $\cat{C}$に対して，$X$が$\cat{C}$の対象 (object) であることを，記号$\in$を用いて$X\in\cat{C}$で表す．
- 圏$\cat{C}$と$X,Y\in\cat{C}$に対して，$X$から$Y$への$\cat{C}$での射 (morphism) の全体は集合であることを仮定して，この集合を$\mor{\cat{C}}{X}{Y}$で表す．すなわち，以下で扱う圏は全て 局所小圏 (locally small category) である．
- 圏$\cat{C}$に対して，$X,Y\in\cat{C}$であり，$f$が$X$から$Y$への射であるとき，「($\cat{C}$の) 射$\func{f}{X}{Y}$に対して...」などの略記を用いることがある．
- 通常の定義とは異なるが，圏$\cat{C}$と$Z,Y,X\in\cat{C}$に対して，$\cat{C}$での合成 (composition) $\circ$を$\mor{\cat{C}}{Y}{Z}\times\mor{\cat{C}}{X}{Y}$から$\mor{\cat{C}}{X}{Z}$への写像として定義する．
- 圏$\cat{C}$と$\cat{C}$での射$\func{g}{Y}{Z}$と$\func{f}{X}{Y}$に対して，$\cat{C}$での射$\func{\mathop{\circ}(g,f)}{X}{Z}$を$g$と$f$の$\cat{C}$での合成 (composition) とよび，$g\circ f$や$gf$で表す．
- 圏$\cal{C}$と$X\in\cat{C}$に対して，$X$の$\cat{C}$での恒等射 (identity) を$\id{X}$で表す．
集合の圏
集合の圏の構成
圏$\set$を以下で定める:
- $\set$の対象とは，集合のことである．
- $\set$の対象$X$と$Y$に対して，$X$から$Y$への$\set$での射とは，$X$から$Y$への写像のことである．すなわち，集合$\mor{\set}{X}{Y}$を，$X$から$Y$への写像の全体と定める．
- $\set$での射$\func{g}{Y}{Z}$と$\func{f}{X}{Y}$に対して，$g$と$f$の合成$\func{gf}{X}{Z}$を，各$x\in X$に対して$(gf)(x):=g(f(x))$で定める．すなわち，$\set$の対象$Z$と$Y$と$X$に対して，写像$$\func{\circ}{\mor{\set}{Y}{Z}\times\mor{\set}{X}{Y}}{\mor{\set}{X}{Z}},(g,f)\mapsto\mathop{\circ}(g,f)$$を，各$g\in\mor{\set}{Y}{Z}$と$f\in\mor{\set}{X}{Y}$と$x\in X$に対して$(\mathop{\circ}(g,f))(x):=g(f(x))$で定める．
$\set$は圏をなす．
実際，$\set$の各対象$X$に対して，$\set$での射$\func{\id{X}}{X}{X}$が，各$x\in X$に対して$\id{X}(x):=x$で定まる．$\set$での任意の射$\func{f}{X}{Y}$に対して，$(\id{Y}f)(x)=\id{Y}(f(x))=f(x)$及び$(f\,\id{X})(x)=f(\id{X}(x))=f(x)$が各$x\in X$に対して成り立つので，$\id{Y}f=f=f\,\id{X}$である．
また，$\set$での任意の射$\func{h}{Z}{W}$と$\func{g}{Y}{Z}$と$\func{f}{X}{Y}$に対して，
$$(h(gf))(x)=h((gf)(x))=h(g(f(x)))=(hg)(f(x))=((hg)f)(x),$$
が各$x\in X$に対して成り立つので，$h(gf)=(hg)f$である．
ゆえに，$\set$は圏をなし，各$X\in\set$に対して，$\id{X}$は$X$の$\set$での恒等射である．
圏$\set$を集合の圏 (category of sets)とよぶ．
集合の全体は"集合としては定義出来ない"ことが知られている．そのため，上で定めた圏$\set$は 小圏 (small category) ではない．しかし，ここでは グロタンディーク宇宙 (Grothendieck universe) や 強到達不能基数 (strongly inaccessible cardinal) などの道具を用いて圏の大きさに制限を設けることはせずに，集合全体の"集まり"なども集合のように扱うことにする．詳しくは [2, §1.2.15] や [2, §A.1] の冒頭を参照されたい．
集合の圏$\set$は良い性質をたくさんもつことが知られているが，ここでは以下の二つのみを紹介する:
- $\set$が終対象をもつこと (命題 3)．
- $\set$が積をもつこと (命題 6)．
準備
終対象と積を導入する前に，同型射について述べておこう．
$\cat{C}$を圏とする．
$X,Y\in\cat{C}$とする．$f$が$X$から$Y$への同型射 (isomorphism) であるとは，$f$が$X$から$Y$への射であり，$gf=\id{X}$かつ$fg=\id{Y}$をみたす射$\func{g}{Y}{X}$が存在することをいう．$f$が$X$から$Y$への同型射であることを，$\func{f}{X}{Y}$が同型射であるという．
射$\func{f}{X}{Y}$と$\func{g}{Y}{X}$に対して，$gf=\id{X}$であることは，
$$\xymatrix{X\ar[r]^f\ar[rd]_{\id{X}}&Y\ar[d]^g\\
&X}$$
という図式 (diagram) が可換 (commutative)であると表される．同様に，$fg=\id{Y}$であることは，図式
$$\xymatrix{Y\ar[r]^g\ar[rd]_{\id{Y}}&X\ar[d]^f\\
&Y}$$
が可換であると表される．図式及びその可換性の正確な定義は述べないが，以下ではしばしば図式の可換性という形式で，条件を記述することがある．
$\func{f}{X}{Y}$を射とする．射$\func{g,g'}{Y}{X}$に対して，$gf=\id{X}$かつ$fg'=\id{Y}$ならば，$g=g'$である．
$$g=g\,\id{Y}=gfg'=\id{X}g'=g',$$
よりわかる．
射$\func{f}{X}{Y}$を取る．射$\func{g,g'}{Y}{X}$が$gf=\id{X}$かつ$fg=\id{Y}$，及び$g'f=\id{X}$かつ$fg'=\id{Y}$をみたすならば，特に$gf=\id{X}$かつ$fg'=\id{Y}$であり，命題 1 より$g=g'$が成り立つ．ゆえに，$\func{f}{X}{Y}$が同型射ならば，$gf=\id{X}$かつ$fg=\id{Y}$をみたす射$\func{g}{Y}{X}$が一意に存在することがわかる．これを$f$の逆 (inverse) とよび，$f^{-1}$で表す．
集合の圏は終対象をもつ
$\cat{C}$を圏として，$X\in\cat{C}$とする．$X$が終対象 (terminal object) であるとは，任意の$Y\in\cat{C}$に対して，$Y$から$X$への射が一意に存在することをいう．
$\cat{C}$を圏として，$X,X'\in\cat{C}$とする．$X$と$X'$が終対象ならば，$X$から$X'$への同型射が一意に存在する．
- $X$から$X'$への同型射が存在すること: $X'$は$\cat{C}$の終対象だから，射$\func{f}{X}{X'}$が取れる．また，$X$は$\cat{C}$の終対象だから，射$\func{g}{X'}{X}$が取れる．
$gf$と$\id{X}$は$X$から$X$への射であり，$X$が終対象であることから，$gf=\id{X}$を得る．また，$fg$と$\id{X'}$は$X'$から$X'$への射であり，$X'$が終対象であることから，$fg=\id{X'}$を得る．
ゆえに，$f$は$X$から$X'$への同型射である． - $X$から$X'$への同型射が一意であること: $X'$が終対象であり，$X$から$X'$への同型射は$X$から$X'$への射であることから，任意の同型射$\func{f'}{X}{X'}$に対して，$f'=f$である．
$\{\es\}$は$\set$の終対象である．
集合$Y$を任意に取る．
(1) $Y$から$\{\es\}$への写像が存在すること: 写像$\func{f}{Y}{\{\es\}}$が，各$y\in Y$に対して$f(y):=\es$で定まる．
(2) $Y$から$\{\es\}$への写像が一意であること: 写像$\func{f'}{Y}{\{\es\}}$を任意に取る．各$y\in Y$に対して，$f'(y)\in\{\es\}$だから，$f'(y)=\es=f(y)$であり，$f'=f$である．
ゆえに，$\set$は終対象をもつ．
集合の圏は積をもつ
$\cat{C}$を圏として，$X,Y\in\cat{C}$とする．$Z\in\cat{C}$と射$\func{p_{X,Y}}{Z}{X}$と$\func{q_{X,Y}}{Z}{Y}$に対して，組$(Z,p_{X,Y},q_{X,Y})$が$X$と$Y$の積 (product) であるとは，任意の$W\in\cat{C}$と任意の射$\func{f}{W}{X}$と$\func{g}{W}{Y}$に対して，$p_{X,Y}h=f$かつ$q_{X,Y}h=g$をみたす射$\func{h}{W}{Z}$が一意に存在することをいう:
$$\xymatrix{&W\ar[ld]_f\ar[rd]^g\ar@{-->}[dd]^h\\
X&&Y\\
&Z\ar[lu]^{p_{X,Y}}\ar[ru]_{q_{X,Y}}}$$
$\cat{C}$を圏として，$X,Y,Z\in\cat{C}$として，$\func{p_{X,Y}}{Z}{X}$と$\func{q_{X,Y}}{Z}{Y}$を射として，$(Z,p_{X,Y},q_{X,Y})$は$X$と$Y$の積であるとする．射$\func{f}{Z}{Z}$が$p_{X,Y}f=p_{X,Y}$かつ$q_{X,Y}f=q_{X,Y}$をみたすならば，$f=\id{Z}$である．
$p_{X,Y}\id{Z}=p_{X,Y}$かつ$q_{X,Y}\id{Z}=q_{X,Y}$であり，$(Z,p_{X,Y},q_{X,Y})$が$X$と$Y$の積であることから，$f=\id{Z}$を得る．
$\cat{C}$を圏として，$X,Y,Z,Z'\in\cat{C}$として，$\func{p_{X,Y}}{Z}{X}$と$\func{q_{X,Y}}{Z}{Y}$と$\func{p'_{X,Y}}{Z'}{X}$と$\func{q'_{X,Y}}{Z'}{Y}$を射とする．$(Z,p_{X,Y},q_{X,Y})$と$(Z',p'_{X,Y},q'_{X,Y})$が$X$と$Y$の積ならば，$p'_{X,Y}h=p_{X,Y}$かつ$q'_{X,Y}h=q_{X,Y}$をみたす$Z$から$Z'$への同型射$h$が一意に存在する:
$$\xymatrix{&Z\ar[ld]_{p_{X,Y}}\ar[rd]^{q_{X,Y}}\ar@{-->}[dd]^h\\
X&&Y\\
&Z'\ar[lu]^{p'_{X,Y}}\ar[ru]_{q'_{X,Y}}}$$
- $p'_{X,Y}h=p_{X,Y}$かつ$q'_{X,Y}h=q_{X,Y}$をみたす$Z$から$Z'$への同型射$h$が存在すること: $(Z',p'_{X,Y},q'_{X,Y})$は$X$と$Y$の積だから，$p'_{X,Y}h=p_{X,Y}$かつ$q'_{X,Y}h=q_{X,Y}$をみたす射$\func{h}{Z}{Z'}$が取れる:
$$\xymatrix{&Z\ar[ld]_{p_{X,Y}}\ar[rd]^{q_{X,Y}}\ar@{-->}[dd]^h\\ X&&Y\\ &Z'\ar[lu]^{p'_{X,Y}}\ar[ru]_{q'_{X,Y}}}$$
また，$(Z,p_{X,Y},q_{X,Y})$は$X$と$Y$の積だから，$p_{X,Y}i=p'_{X,Y}$かつ$q_{X,Y}i=q'_{X,Y}$をみたす射$\func{i}{Z'}{Z}$が取れる:
$$\xymatrix{&Z'\ar[ld]_{p'_{X,Y}}\ar[rd]^{q'_{X,Y}}\ar@{-->}[dd]^i\\ X&&Y\\ &Z\ar[lu]^{p_{X,Y}}\ar[ru]_{q_{X,Y}}}$$
このとき，$p_{X,Y}ih=p'_{X,Y}h=p_{X,Y}$及び$q_{X,Y}ih=q'_{X,Y}h=q_{X,Y}$であり，$(Z,p_{X,Y},q_{X,Y})$が$X$と$Y$の積であることから，補題 4 より$ih=\id{Z}$を得る．また，$p_{X,Y}'hi=p_{X,Y}i=p'_{X,Y}$及び$q_{X,Y}'hi=q_{X,Y}i=q'_{X,Y}$であり，$(Z',p'_{X,Y},q'_{X,Y})$が$X$と$Y$の積であることから，補題 4 より$hi=\id{Z'}$を得る．ゆえに，$h$は$Z$から$Z'$への同型射である．
$h$の定め方から，$p'_{X,Y}h=p_{X,Y}$かつ$q'_{X,Y}h=q_{X,Y}$が成り立つ． - $p'_{X,Y}h=p_{X,Y}$かつ$q'_{X,Y}h=q_{X,Y}$をみたす$Z$から$Z'$への同型射$h$が一意であること: $(Z',p'_{X,Y},q'_{X,Y})$が$X$と$Y$の積であり，$Z$から$Z'$への同型射は$Z$から$Z'$への射であることから，$p'_{X,Y}h'=p_{X,Y}$かつ$q'_{X,Y}h'=q_{X,Y}$をみたす任意の同型射$\func{h'}{Z}{Z'}$に対して，$h'=h$である．
定義 1 にも現れたが，集合$X$と$Y$に対して，$X$と$Y$の積 (product) とは，$X\times Y:=\{(x,y):x\in X,y\in Y\}$で定まる集合$X\times Y$のことである．ただし，$\{(x,y):x\in X,y\in Y\}$とは$\{z:z=(x,y)\,\text{をみたす}\,x\in X\,\text{と}\,y\in Y\,\text{が存在する}\}$の略記である．集合$X$と$Y$に対して，写像$\func{p_{X,Y}}{X\times Y}{X}$と$\func{q_{X,Y}}{X\times Y}{Y}$が，各$(x,y)\in X\times Y$に対して$p_{X,Y}((x,y)):=x$と$q_{X,Y}((x,y)):=y$で定まる．
集合$X$と$Y$に対して，$(X\times Y,p_{X,Y},q_{X,Y})$は$X$と$Y$の$\set$での積である．
集合$W$と写像$\func{f}{W}{X}$と$\func{g}{W}{Y}$を任意に取る．
- $p_{X,Y}h=f$かつ$q_{X,Y}h=g$をみたす写像$\func{h}{W}{X\times Y}$が存在すること: 写像$\func{h}{W}{X\times Y}$が，各$w\in W$に対して$h(w):=(f(w),g(w))$で定まる．$(p_{X,Y}h)(w)=p_{X,Y}(h(w))=p_{X,Y}((f(w),g(w)))=f(w)$及び$(q_{X,Y}h)(w)=q_{X,Y}(h(w))=q_{X,Y}((f(w),g(w)))=g(w)$が各$w\in W$に対して成り立つので，$p_{X,Y}h=f$かつ$q_{X,Y}h=g$である．
- $p_{X,Y}h=f$かつ$q_{X,Y}h=g$をみたす写像$\func{h}{W}{X\times Y}$が一意であること: $p_{X,Y}h'=f$かつ$q_{X,Y}h'=g$をみたす写像$\func{h'}{W}{X\times Y}$を任意に取る．各$w\in W$に対して，$h'(w)\in X\times Y$だから，$h'(w)=(x_w,y_w)$をみたす$x_w\in X$と$y_w\in Y$が存在して，
$$\begin{align} h'(w)&=(x_w,y_w)=(p_{X,Y}((x_w,y_w)),q_{X,Y}((x_w,y_w)))\\ &=(p_{X,Y}(h'(w)),q_{X,Y}(h'(w)))=((p_{X,Y}h')(w),(q_{X,Y}h')(w))=(f(w),g(w))=h(w), \end{align}$$
であり，$h'=h$である．
ゆえに，$\set$は積をもつ．
まとめ
この記事では，集合の圏$\set$を構成して，$\set$が終対象と積をもつことを確認した．一般に，圏$\cat{C}$が終対象と積をもつとき，$\cat{C}$は有限積をもつ (have finite products) ということがある([
3
,
Tag 001R
])．
有限積をもつ圏は自然な「モノイダル構造」をもつことが知られている．次の記事では，モノイダル構造や「モノイダル圏」を定義して，$\set$上のモノイダル構造を構成する．また，$\set$上のモノイダル構造が「対称モノイダル閉構造」であることを示す．
付録: 命題 5 の別証明
以下では，命題 5 の別証明を与える．この証明は，準備は少し大変かもしれないが，見通しがよいと思う．
$\cat{C}$を圏として，$X,Y,Z,Z'\in\cat{C}$として，$\func{p_{X,Y}}{Z}{X}$と$\func{q_{X,Y}}{Z}{Y}$と$\func{p'_{X,Y}}{Z'}{X}$と$\func{q'_{X,Y}}{Z'}{Y}$を射とする．$(Z,p_{X,Y},q_{X,Y})$と$(Z',p'_{X,Y},q'_{X,Y})$が$X$と$Y$の積ならば，$p'_{X,Y}h=p_{X,Y}$かつ$q'_{X,Y}h=q_{X,Y}$をみたす$Z$から$Z'$への同型射$h$が一意に存在する:
$$\xymatrix{&Z\ar[ld]_{p_{X,Y}}\ar[rd]^{q_{X,Y}}\ar@{-->}[dd]^h\\
X&&Y\\
&Z'\ar[lu]^{p'_{X,Y}}\ar[ru]_{q'_{X,Y}}}$$
$\cat{C}$を圏として，$X,Y\in\cal{C}$とする．
圏$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$を以下で定める:
(1) $\cat{C}_{X\leftarrow\,\bullet\,\to Y}$の対象とは，$Z\in\cat{C}$と$\cat{C}$での射$\func{p}{Z}{X}$と$\func{q}{Z}{Y}$の組$(Z,p,q)$のことである．
(2) $\cat{C}_{X\leftarrow\,\bullet\,\to Y}$の対象$(Z,p,q)$と$(Z',p',q')$に対して，$(Z,p,q)$から$(Z',p',q')$への$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での射とは，$p'f=p$かつ$q'f=q$をみたす$\cat{C}$での射$\func{f}{Z}{Z'}$のことである:
$$\xymatrix{&Z\ar[ld]_p\ar[rd]^q\ar[dd]^f\\
X&&Y\\
&Z'\ar[lu]^{p'}\ar[ru]_{q'}}$$
すなわち，集合$\mor{\cat{C}_{X\leftarrow\,\bullet\,\to Y}}{(Z,p,q)}{(Z',p',q')}$を，
$$\mor{\cat{C}_{X\leftarrow\,\bullet\,\to Y}}{(Z,p,q)}{(Z',p',q')}:=\{f\in\mor{\cat{C}}{Z}{Z'}:p'f=p,q'f=q\}.$$
で定める．
(3) $\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での射$\func{g}{(Z,p,q)}{(Z',p',q')}$と$\func{f}{(Z'',p'',q'')}{(Z,p,q)}$に対して，$g$と$f$の$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での合成$g\circ f$を，$g$と$f$の$\cat{C}$での合成$gf$として定める．すなわち，$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$の対象$(Z'',p'',q'')$と$(Z',p',q')$と$(Z,p,q)$に対して，写像
$$\begin{align}
\circ\colon\cat{C}_{X\leftarrow\,\bullet\,\to Y}((Z,p,q),(Z',&p',q'))\times\mor{\cat{C}_{X\leftarrow\,\bullet\,\to Y}}{(Z'',p'',q'')}{(Z,p,q)}\\
&\to\mor{\cat{C}_{X\leftarrow\,\bullet\,\to Y}}{(Z'',p'',q'')}{(Z',p',q')},(g,f)\mapsto g\circ f
\end{align}$$
を，各$g\in\mor{\cat{C}_{X\leftarrow\,\bullet\,\to Y}}{(Z,p,q)}{(Z',p',q')}$と$f\in\mor{\cat{C}_{X\leftarrow\,\bullet\,\to Y}}{(Z'',p'',q'')}{(Z,p,q)}$に対して$\mathop{\circ}((g,f)):=gf$で定める．
$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での射$\func{g}{(Z,p,q)}{(Z',p',q')}$と$\func{f}{(Z'',p'',q'')}{(Z,p,q)}$を取る．このとき，$g\circ f$が$(Z'',p'',q'')$から$(Z',p',q')$への$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での射であることは，以下のように示される．
まず，$g$は$(Z,p,q)$から$(Z',p',q')$への$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での射だから，$g$は$Z$から$Z'$への$\cat{C}$での射であり，$p'g=p$かつ$q'g=q$をみたす:
$$\xymatrix{&Z\ar[ld]_p\ar[rd]^q\ar[dd]^g\\
X&&Y\\
&Z'\ar[lu]^{p'}\ar[ru]_{q'}}$$
また，$f$は$(Z'',p'',q'')$から$(Z,p,q)$への$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での射だから，$f$は$Z''$から$Z$への$\cat{C}$での射であり，$pf=p''$かつ$qf=q''$をみたす:
$$\xymatrix{&Z''\ar[ld]_{p''}\ar[rd]^{q''}\ar[dd]^f\\
X&&Y\\
&Z\ar[lu]^p\ar[ru]_q}$$
このとき，$g$と$f$の$\cat{C}$での合成$gf$が$Z''$から$Z'$への$\cat{C}$での射として定まり，$p'gf=pf=p''$及び$q'gf=qf=q''$をみたす:
$$\xymatrix{&&Z''\ar[dd]^f\ar@/_1.2pc/[lldd]_{p''}\ar@/^1.2pc/[rrdd]^{q''}\\\\
X&&Z\ar[ll]_p\ar[rr]^q\ar[dd]^g&&Y\\\\\
&&Z'\ar@/^1.2pc/[lluu]^{p'}\ar@/_1.2pc/[rruu]_{q'}}$$
これは，$g\circ f=gf$が$(Z'',p'',q'')$から$(Z',p',q')$への$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での射であることを示している．
$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$は圏をなす．実際，$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$の各対象$(Z,p,q)$に対して，$Z$の$\cat{C}$での恒等射$\id{Z}$は，$Z$から$Z$への$\cat{C}$での射であり，$p\,\id{Z}=p$かつ$q\,\id{Z}=q$をみたす:
$$\xymatrix{&Z\ar[ld]_p\ar[rd]^q\ar[dd]^{\id{Z}}\\
X&&Y\\
&Z\ar[lu]^p\ar[ru]_q}$$
ゆえに，$\id{Z}$は$(Z,p,q)$から$(Z,p,q)$への$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での射である．$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での任意の射$\func{f}{(Z,p,q)}{(Z',p',q')}$に対して，$\id{Z'}\circ f=\id{Z'}f=f=f\,\id{Z}=f\circ\id{Z}$である．
また，$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での任意の射$\func{h}{(Z'',p'',q'')}{(Z''',p''',q''')}$と$\func{g}{(Z',p',q')}{(Z'',p'',q'')}$と$\func{f}{(Z,p,q)}{(Z',p',q')}$に対して，
$$h\circ(g\circ f)=h(g\circ f)=h(gf)=(hg)f=(h\circ g)f=(h\circ g)\circ f,$$
である．
ゆえに，$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$は圏をなし，各$(Z,p,q)\in\cat{C}_{X\leftarrow\,\bullet\,\to Y}$に対して，$\id{Z}$は$(Z,p,q)$の$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での恒等射である．
$(Z,p,q),(Z',p',q')\in\cat{C}_{X\leftarrow\,\bullet\,\to Y}$として，$\func{h}{Z}{Z'}$を$\cat{C}$での射とする．このとき，以下は同値である:
(i) $h$は$(Z,p,q)$から$(Z',p',q')$への$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での同型射である．
(ii) $h$は$Z$から$Z'$への$\cat{C}$での同型射であり，$p'h=p$かつ$q'h=q$をみたす:
$$\xymatrix{&Z\ar[ld]_p\ar[rd]^q\ar[dd]^h\\
X&&Y\\
&Z'\ar[lu]^{p'}\ar[ru]_{q'}}$$
(i)$\Rightarrow$(ii): (i) が成り立つならば，$i\circ h=\id{(Z,p,q)}$かつ$h\circ i=\id{(Z',p',q')}$をみたす$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での射$\func{i}{(Z',p',q')}{(Z,p,q)}$が取れる．定義 5, (2) より$i$は$Z$から$Z'$への$\cat{C}$での射である．また，定義 5, (3) と$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$が圏をなすことの議論から，$ih=i\circ h=\id{(Z,p,q)}=\id{Z}$及び$hi=h\circ i=\id{(Z',p',q')}=\id{Z'}$が成り立つ．ゆえに，(ii) が成り立つ．
(ii)$\Rightarrow$(i): (ii) が成り立つならば，$jh=\id{Z}$かつ$hj=\id{Z'}$をみたす$\cat{C}$での射$\func{j}{Z'}{Z}$が取れる．$pj=p'hj=p'\id{Z'}=p'$及び$qj=,q'hj=q'\id{Z'}=q'$だから，定義 5, (2) より$j$は$(Z',p',q')$から$(Z,p,q)$への$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での射である:
$$\xymatrix{&&Z'\ar[dd]^j\ar@/_1.2pc/[lldd]_{p'}\ar@/^3pc/[dddd]^{\,\,\id{Z'}}&&&Z'\ar@/_3pc/[dddd]\ar[dd]_j\ar@/^1.2pc/[rrdd]^{q'}\\\\
X&&Z\ar[ll]_p\ar[dd]^h&&&Z\ar[dd]_h\ar[rr]^q&&Y\\\\
&&Z'\ar@/^1.2pc/[lluu]^{p'}&&&Z'\ar@/_1.2pc/[rruu]_{q'}}$$
また，定義 5, (3) と$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$が圏をなすことの議論から，$j\circ h=jh=\id{Z}=\id{(Z,p,q)}$及び$h\circ j=hj=\id{Z'}=\id{(Z',p',q')}$が成り立つ．ゆえに，(i) が成り立つ．
我々が示したいのは，以下の主張であった:
$Z,Z'\in\cat{C}$として，$\func{p_{X,Y}}{Z}{X}$と$\func{q_{X,Y}}{Z}{Y}$と$\func{p'_{X,Y}}{Z'}{X}$と$\func{q'_{X,Y}}{Z'}{Y}$を$\cat{C}$での射とする．$(Z,p_{X,Y},q_{X,Y})$と$(Z',p'_{X,Y},q'_{X,Y})$が$X$と$Y$の$\cat{C}$での積ならば，$p'_{X,Y}h=p_{X,Y}$かつ$q'_{X,Y}h=q_{X,Y}$をみたす$Z$から$Z'$への$\cat{C}$での同型射$h$が一意に存在する:
$$\xymatrix{&Z\ar[ld]_{p_{X,Y}}\ar[rd]^{q_{X,Y}}\ar@{-->}[dd]^h\\
X&&Y\\
&Z'\ar[lu]^{p'_{X,Y}}\ar[ru]_{q'_{X,Y}}}$$
$(Z,p_{X,Y},q_{X,Y}),(Z',p'_{X,Y},q'_{X,Y})\in\cat{C}_{X\leftarrow\,\bullet\,\to Y}$である．$(Z,p_{X,Y},q_{X,Y})$と$(Z',p'_{X,Y},q'_{X,Y})$が$X$と$Y$の$\cat{C}$での積ならば，定義 5, (2) よりこれらは$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$の終対象であり，命題 2 より$(Z,p_{X,Y},q_{X,Y})$から$(Z',p'_{X,Y},q'_{X,Y})$への$\cat{C}_{X\leftarrow\,\bullet\,\to Y}$での同型射が一意に存在して，補題 8 より主張が成立する．
追記
- 2022/2/19 21:40 命題 1 の証明を修正した．
- 2022/2/20 15:36 参考文献に第2回 (前半) の記事 [ 5 ] を加えた．
- 2022/2/23 22:28 参考文献に第2回 (後半) の記事 [ 6 ] を加えた．
- 2022/2/26 14:55 参考文献に第3回の記事 [ 7 ] を加えた．
- 2022/3/3 22:56 参考文献に第4回 (前半) の記事 [ 8 ] を加えた．
- 2022/3/3 22:56 参考文献に第4回 (後半) (1) の記事 [ 9 ] を加えた．
- 2022/3/3 23:32 参考文献に第4回 (後半) (2) の記事 [ 10 ] を加えた．
