表題の「とあるコンマ圏」をちゃんと言うと：
- 圏 $`\mathcal{C}`$ の米田埋め込み $`よ_\mathcal{C}`$ と、$`\mathcal{C}`$ 上の前層 $`X`$ から作られるコンマ圏 $`(よ_\mathcal{C} \downarrow X)`$
表題の主張は次の圏同値があることです。
$`\quad (よ_\mathcal{C} \downarrow X) \simeq \int_\mathcal{C} X`$
この主張を示すために、前半では一応形式的〈formal〉な議論をします。が、この記事の眼目は後半です。後半において、上記の圏同値（実際は圏同型）を直感的に理解するために幾つかのポンチ絵を描きます。
米田の補題に関連する圏論的ガジェット達が、魔法のようにうまく働いて当該の主張を成立させます。このマジカルな状況を“絵解き”出来ればいいな、と。
予備知識：
- コンマ圏については comma category 参照
- 要素の圏については category of elements 参照
内容：
- コンマ圏
- 米田写像と音楽記号
- このコンマ圏は要素の圏
- Φの対象パート
- Φのホムパート
- どんな圏も、前層達の圏の部分圏
- 集合とホムセットの絵
- 米田の補題と米田写像の絵
- 射のあいだの対応の絵
- オーバー圏とファイバー付き圏
コンマ圏
以下の図式があるとき、関手 $`F`$ と関手 $`G`$ のコンマ圏〈comma category〉は $`(F\downarrow G)`$ と書きます。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\DA}{\downarrow}
\newcommand{\An}[1]{\langle #1 \rangle} % Angular
\newcommand{\twoto}{\Rightarrow}
%\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\o}[1]{\overline{#1} }
%\newcommand{\u}[1]{\underline{#1} }
\newcommand{\op}{\mathrm{op} }
\newcommand{\In}{\text{ in } }
\newcommand{\hyp}{\text{－} }
`$
$`\quad \xymatrix{
\cat{C} \ar[dr]_F
&{}
&\cat{D} \ar[dl]^G
\\
{}
&\cat{E}
&{}
}\\
\quad \In \mbf{CAT}
`$
コンマ圏 $`(F\DA G)`$ の対象は $`\An{c,\varphi, d}`$ と書きます。ここで：
- $`c\in |\cat{C}|`$
- $`d\in |\cat{D}|`$
- $`\varphi: F(c) \to G(d)\In \cat{E}`$
コンマ圏 $`(F\DA G)`$ の2つの対象 $`\An{c, \varphi, d}`$ 、$`\An{c', \varphi', d'}`$ に対して、そのあいだの射は $`\An{f, g}`$ と書きます。ここで：
- $`f: F(c)\to F(c')`$
- $`g: G(d)\to G(d')`$
- 以下の図式が可換
$`\quad \xymatrix{
F(c) \ar[r]^{\varphi} \ar[d]_f
&G(d) \ar[d]^g
\\
F(c') \ar[r]_{\varphi'}
&G(d')
}\\
\quad \text{commutative }\In \cat{E}
`$
（[追記]上記の箇条書きと図式に間違いがありました。id:u23mjag さんのご指摘により修正しました。[/追記]）
$`\mbf{I}`$ は単一対象と恒等射だけの自明圏とします。$`e\in |\cat{E}|`$ として、対象 $`e`$ をポインティングする関手を $`e^\sim`$ と書きます。
$`\quad e^\sim : \mbf{I}\to \cat{E}\In \mbf{CAT}`$
以下の図式から得られるコンマ圏は $`(F \DA e^\sim)`$ ですが、$`(F\DA e)`$ とも書きます。
$`\quad \xymatrix{
\cat{C} \ar[dr]_F
&{}
&\mrm{I} \ar[dl]^{e^\sim}
\\
{}
&\cat{E}
&{}
}\\
\quad \In \mbf{CAT}
`$
米田写像と音楽記号
$`F:\cat{C}^\op\to \mbf{Set}`$ は前層（反変関手）、$`a\in |\cat{C}|`$ とします。米田の補題〈Yoneda lemma〉によれば、次の同型があります。$`よ^\hyp`$ は米田埋め込み〈Yoneda embedding〉です。
$`\quad \mrm{Nat}(よ^a , F)\cong F(a) \In \mbf{Set}`$
この同型を与える写像は米田写像〈Yoneda {map | bijection | isomorphism}〉 $`\mbf{y}_{F, a}`$ です。
$`\quad \mbf{y}_{F, a} : \mrm{Nat}(よ^a , F)\to F(a) \In \mbf{Set}`$
「米田の補題とストリング図 // 米田同型」に従い、米田写像をフラット記号、米田写像の逆写像をシャープ記号で表すことにします
$`\quad (\hyp)^\flat : \mrm{Nat}(よ^a , F)\to F(a) \In \mbf{Set}\\
\quad (\hyp)^\sharp : F(a) \to \mrm{Nat}(よ^a , F) \In \mbf{Set}
`$
音楽記号〈musical notation symbol〉を使う記法は微分幾何で使われていて（Musical isomorphism 参照）、座標成分添字の“上げ下げ”に合わせてフラット／シャープを使っています。ここでは、抽象度を下げる（自然変換の）エンコードをフラット、抽象度を上げるデコードをシャープとしています。
このコンマ圏は要素の圏
以下の図式を考えます。
$`\quad \xymatrix {
\cat{C} \ar[dr]_{よ}
&{}
&\mrm{I} \ar[dl]^{X^\sim}
\\
{}
&{\cat{C}^\wedge}
&{}
}\\
\quad \In \mbf{CAT}
`$
ここで：
- $`\cat{C}^\wedge`$ は前層達の圏 $`\cat{C}^\wedge = [\cat{C}^\op, \cat{C}]`$
- $`よ = よ_\cat{C}`$ は米田埋め込み（右下付きの $`\cat{C}`$ は、文脈から明らかなら省略）
- $`X`$ は圏 $`\cat{C}`$ 上の前層 $`X:\cat{C}^\op \to \mbf{Set}`$
示したいことは次の圏同値です。
$`\quad (よ \DA X) \simeq \int_\cat{C} X`$
右辺はグロタンディーク構成ですが、前層のグロタンディーク構成は要素の圏〈category of elements〉と呼びます。コンマ圏から要素の圏への圏同値を与える関手 $`\Phi`$ を以下で構成します。
Φの対象パート
コンマ圏 $`(よ\DA X)`$ の対象 $`\An{a, \varphi, X}`$ を考えます。このコンマ圏の対象を $`\cat{C}^\wedge`$ 内で考えれば：
$`\quad \varphi: よ^a \to X \In \cat{C}^\wedge`$
圏達の2-圏 $`\mbf{CAT}`$ 内で考えれば：
$`\quad \varphi:: よ^a \twoto X : \cat{C}^\op \to \mbf{Set} \In \mbf{CAT}`$
米田の補題によれば、次の同型があります。
$`\quad \mrm{Nat}(よ^a , X)\cong X(a) \In \mbf{Set}`$
この同型を与える写像は米田写像 $`\mbf{y}_{X, a}`$ です。
$`\quad \mbf{y}_{X, a} : \mrm{Nat}(よ^a , X)\to X(a) \In \mbf{Set}`$
関手 $`\Phi`$ の対象パート〈object part〉は米田写像を使って定義します。
$`\quad \Phi(\An{a, \varphi, X}) := \mbf{y}_{X, a}(\varphi)\; \in X(a)`$
フラット記号を使って書けば：
$`\quad \Phi(\An{a, \varphi, X}) := \varphi^\flat \; \in X(a)`$
$`X(a)`$ は要素の圏 $`\int_\cat{C} X`$ のファイバーです。$`a`$ を固定した場合の $`\An{a, \varphi, X}`$ の形の“コンマ圏の対象”達は、ベース圏の対象 $`a\in |\cat{C}|`$ 上のファイバー $`X(a)`$ と同型になります。
$`\text{For } a\in |\cat{C}|\\
\quad \{\An{a, \varphi, X}\mid \varphi\in \mrm{Nat}(よ^a, X)\} \cong X(a) \In \mbf{Set}`$
$`a \in |\cat{C}|`$ を動かしてやると、$`\Phi`$ の像は、ファイバー $`X(a)`$ 達をすべて足した〈直和した〉集合 $`\sum_{a\in |\cat{C}|} X(a)`$ になります。これで、$`\Phi`$ の対象パートが全射になることが分かります。実際は全単射〈双射〉ですが、圏同値の条件としては全射だけで十分です。
対象パートとしての $`\Phi`$ が、総和〈シグマ型〉$`\sum_{a\in |\cat{C}|} X(a)`$ に値を取ると考える場合（通常はそう考える）は、値を依存ペアの形で書きます。
$`\quad \Phi(\An{a, \varphi, X}) = (a, \varphi^\flat)
\text{ where } a\in |\cat{C}|, \varphi^\flat \in X(a)
`$
単一の値 $`\varphi^\flat`$ と依存ペア $`(a, \varphi^\flat)`$ は置き換え可能〈interchangeable〉です。同一物だが、書き方を変えていると理解しておくのがよいでしょう。
$`\quad \varphi^\flat = (a, \varphi^\flat)`$
Φのホムパート
コンマ圏の射
コンマ圏の2つの対象 $`\An{a, \varphi, X}`$ 、$`\An{b, \psi, X}`$ を考えます。2つの対象のあいだの射は $`\An{\xi, \mrm{ID}_X}`$ の形になります。
$`\quad \An{\xi, \mrm{ID}_X} : \An{a, \varphi, X}\to \An{b, \psi, X}\In (よ\DA X)`$
ここで：
$`\quad \xymatrix{
よ^a \ar[r]^{\varphi} \ar[d]_\xi
&X \ar@{=}[d]^{\mrm{ID}_X}
\\
よ^{b} \ar[r]_{\psi}
&X
}\\
\quad \text{commutative }\In \cat{C}^\wedge
`$
米田埋め込みは充満忠実関手なので、自然変換 $`\xi`$ は $`よ^f`$ の形に書けます。
$`\quad \xymatrix{
よ^a \ar[r]^{\varphi} \ar[d]_{よ^f}
&X \ar@{=}[d]^{\mrm{ID}_X}
\\
よ^{b} \ar[r]_{\psi}
&X
}\\
\quad \text{commutative }\In \cat{C}^\wedge\\
\quad \text{where }f:a \to b \In \cat{C}
`$
コンマ圏 $`(よ\DA X)`$ の射
$`\quad \An{\xi, \mrm{ID}_X}: \An{a, \varphi, X}\to \An{b, \psi, X}`$
から $`f:a \to b \In \cat{C}`$ が一意に決まります。なので、$`\An{\xi, \mrm{ID}_X}`$ は次のように書けます。
$`\quad \An{よ^f, \mrm{ID}_X} : \An{a, \varphi, X}\to \An{b, \psi, X}\In (よ\DA X)
`$
要素の圏の射
（[追記]ここから先の何箇所かで、$`\int_\cat{C}`$ が $`\int_A`$ となっていたので修正しました。[/追記]）
圏 $`\cat{C}`$ 上の前層 $`X`$ の要素の圏 $`\int_\cat{C} X`$ の射は、3つ組 $`\An{f, s, t}`$ で表すことにします。ここで：
- $`f:a \to b \In \cat{C}`$ （ベース圏の射）
- $`s \in X(a)`$ （$`a`$ 上のファイバーの要素）
- $`t \in X(b)`$ （$`b`$ 上のファイバーの要素）
- $`X(f)(t) = s`$ を満たす。
次のように書けます。
$`\quad \An{f, s, t} : (a, s) \to (b, t) \In \int_\cat{C} X`$
$`(a, s), (b, t)`$ は、$`\int_\cat{C} X`$ の対象を依存ペアとして書いたものです。
ホムパートの定義
$`\Phi`$ のホムパートは次のような写像です。
$`\quad \Phi_{ \An{a, \varphi, X}, \An{b, \psi, X}} : \\
\qquad (よ\DA X)(\An{a, \varphi, X}, \An{b, \psi, X}) \\
\quad\qquad \to (\int_\cat{C} X)(\Phi(\An{a, \varphi, X}), \Phi(\An{b, \psi, X}))) \In \mbf{Set}
`$
$`\Phi`$ の対象パートは米田写像（フラット記号）で書けて：
$`\quad \Phi_{ \An{a, \varphi, X}, \An{b, \psi, X}} : \\
\qquad (よ\DA X)(\An{a, \varphi, X}, \An{b, \psi, X}) \\
\quad\qquad \to (\int_\cat{C} X)( (a, \varphi^\flat), (b, \psi^\flat)) \In \mbf{Set}
`$
$`\Phi_{ \An{a, \varphi, X}, \An{b, \psi, X}}`$ の定義は以下のようです。
$`\text{For }\An{よ^f, \mrm{ID}_X} : \An{a, \varphi, X} \to \An{b, \psi, X} \In (よ\DA X)\\
\quad \Phi_{ \An{a, \varphi, X}, \An{b, \psi, X}}(\An{よ^f, \mrm{ID}_X})
:= \An{f, \varphi^\flat, \psi^\flat})
`$
なんだかゴチャゴチャしてますが、定義を追いかければどんな写像かハッキリ分かるはずです。ホムパートの写像は可逆です。つまり、ホムセットのあいだの全単射〈双射〉を与えます。これは、関手 $`\Phi`$ が充満忠実であることです。
ここまでで、関手 $`\Phi`$ が“対象集合上で全射”かつ“充満忠実”であることが分かりました。圏同値に関する一般論から、$`\Phi`$ は、コンマ圏 $`(よ\DA X)`$ と要素の圏 $`\int_\cat{C}X`$ の圏同値を与えます。
$`\Phi`$ の関手性〈functoriality〉の確認は省略していますが、そこは各自補ってください。
どんな圏も、前層達の圏の部分圏
前節で、次の圏同値（実際は圏同型）を示しました。
$`\text{For }X \in |\cat{C}^\wedge|\\
\quad (よ \DA X) \simeq \int_\cat{C}X
`$
ここから先では、この圏同値（圏同型）が当たり前に見えるように説明を追加します。
まず、米田埋め込みを暗黙化します（背後に隠してしまう）。米田埋め込み $`よ : \cat{C}\to \cat{C}^\wedge`$ は埋め込みなので、$`\cat{C}`$ と埋め込み像は同一視できます。この同一視により、$`\cat{C}`$ は前層達の圏 $`\cat{C}^\wedge`$ の部分圏とみなせます。
$`\quad \cat{C} \subseteq \cat{C}^\wedge \In \mbf{CAT}`$
$`\cat{C}`$ の対象 $`a`$ は、何もしなくても $`a\in |\cat{C}^\wedge|`$ と考えます。「対象は前層でもある」とするのです。同様に、$`\cat{C}`$ の射 $`f:a \to b`$ は、何もしなくても $`f\in \cat{C}^\wedge(a, b)`$ と考えます。「射は前層のあいだの自然変換でもある」とするのです。
この状況は、以下のような絵に描けます。圏 $`\cat{C}`$ は、広い世界 $`\cat{C}^\wedge`$ のなかにスッポリ入り込んだ一部分です。
集合とホムセットの絵
集合はベン図で描きます。つまり、集合を内部を含むマル（円板）として描き、要素は円板内の一点として描きます。以下はとある集合と、その要素 $`s`$ を（赤色で）描いています。
圏のホムセットも集合ですが、一般の集合とは区別して紡錘形で描きます。紡錘形の両端の点（黒色で描いている）は圏の対象です。ホムセットの要素（圏の射）は点ではなくて矢印で描きます。以下はとあるホムセットと、その要素〈射〉 $`\varphi`$ を（赤色で）描いています。
米田の補題と米田写像の絵
$`a\in |\cat{C}|`$ 、$`X\in |\cat{C}^\wedge|`$ というセットアップでは、米田の補題は次の同型です。
$`\quad \cat{C}^\wedge(a, X) \cong X(a) \In \mbf{Set}`$
$`よ^a`$ と $`a`$ は同一視しています。上記の米田同型は、米田写像（フラット）と逆写像（シャープ）で与えられます。
$`\quad \varphi \mapsto s = \varphi^\flat \\
\quad s \mapsto \varphi = s^\sharp
`$
この状況を絵に描けば次のようになります。
左側の紡錘形は、圏 $`\cat{C}^\wedge`$ のホムセット $`\cat{C}^\wedge(a, X)`$ です。右側のマルは、要素の圏 $`\int_\cat{C} X`$ のファイバー（である集合） $`X(a)`$ です。米田の補題は、$`a`$ から $`X`$ へのホムセットとファイバー $`X(a)`$ が一対一対応することを主張しています。具体的な対応は音楽記号で表しています。
射のあいだの対応の絵
コンマ圏 $`(よ \DA X)`$ の射と、要素の圏 $`\int_\cat{C} X`$ の射は、一対一に対応します。コンマ圏の射は、$`\cat{C}`$ の射 $`f:a\to b`$ と、ホムセット $`\cat{C}^\wedge(b, X)`$ の要素で決まります。もう一方の要素の圏の射は、ベース圏の射 $`f:a\to b`$ と、ファイバー $`X(b)`$ の要素で決まります。
この状況を絵に描けば次のようになります。
左側は、カンマ圏 $`(よ\DA X)`$ の射を示しています。射は、$`f`$ と $`\psi`$ で決まります。$`\varphi`$ は $`f^*(\psi)`$ です。ここで $`f^*`$ は、$`f`$ によるプレ結合引き戻しです。
右側は、要素の圏 $`\int_\cat{C} X`$ の射を示しています。射は、$`f`$ と $`t`$ で決まります。$`s`$ は $`f^*(t)`$ です。ここで $`f^*`$ は、$`X(f)`$ のことです。
プレ結合引き戻しと $`X(f)`$ をどちらも $`f^*`$ と書きました。これらは圏同値（圏同型）を与える関手 $`\Phi`$ で対応しているのです。対応しているので同じ記号で表してもいいですが、もともとは違うメカニズムで定義されている違うモノです。そこは注意しましょう。
オーバー圏とファイバー付き圏
コンマ圏 $`(よ\DA X)`$ は、前層の圏 $`\cat{C}^\wedge`$ の部分圏 $`\cat{C}`$ に対して定義されたオーバー圏〈スライス圏〉 $`\cat{C}/X`$ と考えることができます。$`\cat{C}`$ は部分圏なので、$`X \in|\cat{C}|`$ とは限りません。
要素の圏 $`\int_\cat{C}X`$ は、グロタンディーク構成により作られたファイバー付き圏（の全体圏）です。前層 $`X`$ ごとにファイバー付き圏が構成できます。
オーバー圏 $`\cat{C}/X`$ もファイバー付き圏 $`\int_\cat{C}X`$ も、前層 $`X`$ をパラメータに持ちます。つまり、どちらも前層達の圏 $`\cat{C}^\wedge`$ 上のインデックス付き圏とみなせます。このインデックス付き圏達は、もとのコンマ圏や要素の圏より上位レベルに居る構造達です。
コンマ圏と要素の圏の対応がハッキリすれば、上位レベルの構造を調べることも出来るようになります。
