薄い圏の考察(6).薄い圏における射の集まりたちに関係を入れて新たな薄い圏をつくる。

類Aを任意に固定する。
薄い圏C(A,f)とC(A,g)において、$f_{ij}$が定義されるすべてのi,j$ \in$Aに対して$g_{ij}$が定義されているとき、f$\prec$gと書く。
この（広義の）関係$\prec$について、以下の性質が成り立つ。

1.　f$\prec$f.
2.　f$\prec$gかつg$\prec$hならば、f$\prec$h.
3.　C(A,g)が強連結のとき、任意のC(A,f)に対してf$\prec$gが成り立つ。
4.　C(A,g)が離散的なとき、すなわち「$g_{ij}$が定義されるのはi=jのときのみ恒等射として」なとき、任意のC(A,f)に対してg$\prec$fが成り立つ。

(1~4の証明は$\prec$の定義から直接的に得られます）

Aに対して定義できる「射のあつまり」をすべてあつめたものを$ H_A$と置く（すなわち$H_A=$ {$f $|$ f=$ {$f_{ij} $ } $_{i,j\in A}$}）と、$\prec$が性質1,2を満たすことを『薄い圏の考察１』の例５に当てはめることによって薄い圏$C(H_A,\prec)$が定義できる。
性質3.と4.より圏$C(H_A,\prec)$において、C(A,f)を離散的とする射の集まりfは始対象となり、強連結とするfは終対象となる。

類AとBを任意に固定する。各$f,f'\in H_A$と$g,g'\in H_B$に対して充満な関手$F:C(A,f)\to C(B,g),F':C(A,f')\to C(B,g')$が定まっているとする。それに基づいて
$C(H_A,\prec)$から$C(H_B,\prec)$への関手$ \bar{F}$を
$ \bar{F}(f):=F(f)=${g$_{F(i)F(j)}$}$_{i,j\in A},$
$ \bar{F}(\prec_{ff'}):=\prec_{F(f)F'(f')}$
で定義する。
　まずFが関手であることより、任意の$f_{ij}$に対して$g_{F(i)F(j)}$は存在するので$ \bar{F}(f)=F(f)=${g$_{F(i)F(j)}$}$_{i,j\in A}$はwell-defined。
また$f_{ij}$が存在する任意のi,jに対して$f'_{ij}$が存在するならば、g$_{F(i)F(j)}$が存在する任意のi,jに対してFの充満性より$f_{ij}$が存在することから$f'_{ij}$が存在するので、Fの関手性よりg'$_{F'(i)F'(j)}$も存在して$ \bar{F}(\prec_{ff'})$はwell-defined。

このとき、以下が成り立つ。

命題。任意の$g\in H_B$ に対して、充満かつ本質的に全射な関手$F:C(A,f)\to C(B,g)$と$f\in H_A$が存在するとする。このとき$\bar{F}:C(H_A,\prec)\to C(H_B,\prec)$は圏同値となる。

（証明）$\bar{F}$が本質的に全射な忠実充満関手であることを示す。
(忠実性)
$C(H_A,\prec)$は薄い圏なので「薄い圏の考察(6)」の命題3の1より$\bar{F}$は忠実関手。
（充満性）仮定より$g\prec g'$なる$g,g'\in H_B$ に対して、ある充満関手$F:C(A,f)\to C(B,g),F':C(A,f')\to C(B,g')$と$f,f'\in H_A$が存在して、任意の$i,j\in A$に対して
g$_{F(i)F(j)}=F(f_{ij})$かつg'$_{F'(i)F'(j)}=F'(f'_{ij}).$
よって$F(f)_{ij}$が存在する任意の$i,j\in A$に対して$F(f)_{ij}=g_{F(i)F(j)}$が存在するとすると、$f_{ij}$が存在する任意の$i,j\in A$に対して$F'(f')_{ij}=g'_{F'(i)F'(j)}$が存在すると言える。これは$\bar{F}$が充満関手であることを示している。
(本質的全射性）$F$が本質的に全射なことより、$g_{kl}$が存在する任意の$k,l\in B$に対して$g_{kF(i)},g_{lF(j)}$が存在する$i,j\in A$がとれる。またFの関手性より$g_{F(i)F(j)}$が存在する。これは$ \prec_{g\bar{F}(f)}$の存在を示す。他方、Fの関手性より任意の$i,j\in A$に対してk=F(i)とl=F(j)となる$k,l\in B$は取れるので$g_{F(i)F(j)}$が存在するならば$g_{kl}=g_{F(i)F(j)}$は存在。これは$ \prec_{\bar{F}(f)g}$の存在を意味する。よって関手$\bar{F}$は本質的に全射であるといえる。
以上より$\bar{F}$は本質的に全射な忠実充満関手なので、圏同値となる。（証明終）

系。任意の$g\in H_B$ に対して、同値な関手$F:C(A,f)\to C(B,g)$と$f\in H_A$が存在するとする。このとき$\bar{F}:C(H_A,\prec)\to C(H_B,\prec)$は圏同値となる。
（証明）圏同値ならば本質的に全射な関手であることを上命題に適用する。（証明終）