【圏論メモ】米田の補題の証明

# 命題
$\textbf{C}$ を局所小圏、$X \in \textbf{Ob(C)}$とする。任意の前層 $\mathcal{P}$ に対して、同型：

```math
\textrm{Nat}(\textrm{Hom}_{\textbf{C}}(-,X), \mathcal{P}) \cong \mathcal{P}X
```

が成り立つ。

# 定義
## 局所小圏
$\forall A, B \in \textbf{Ob(C)}$ について、$\textrm{Hom}_{\textbf{C}}(A, B)$ が集合となるような圏 $\textbf{C}$ を**局所小圏**と呼ぶ。

## HomC(A, B)
圏 $\textbf{C}$ の対象 $A, B \in \textbf{Ob(C)}$ 間の射の全体を $\textrm{Hom}_{\textbf{C}}(A, B)$ で表す。

## 前層、前層の圏
反変関手 $\textbf{C} \rightarrow \textbf{Set}$ を**前層**と呼ぶ。
関手圏 $\textbf{Set}^{\textbf{C}^{\textrm{op}}}$ を**前層の圏**と呼ぶ。

$\textbf{C}$ が局所小圏ならば、$\forall A \in \textbf{C}$ について $\textrm{Hom}\_{\textbf{C}}(A, X)$ は集合であるから、$\textrm{Hom}\_{\textbf{C}}(-, X)$ は $\textbf{C} \rightarrow \textbf{Set}$ の反変関手と解釈でき、前層となる。
（逆に $\textbf{C}$ が局所小圏でない場合に $\textrm{Hom}\_{\textbf{C}}(-, X)$ がどこへの関手となるのかそもそも関手と呼べるのかは未調査。ここでは $\textbf{C}$ を局所小圏と仮定しているので気にすることはない。）

## 反変関手
$\textbf{C}^{\textrm{op}}$ から $\textbf{D}$ への関手を $\textbf{C}$ から $\textbf{D}$ への **反変関手** と呼ぶ。

## 関手圏
圏 $\textbf{C}, \textbf{D}$ に対し、次のような圏を関手圏と言い、 $\textbf{D}^{\textbf{C}}$ と表す：

- 対象：$\textbf{C}$ から $\textbf{D}$ への任意の関手 $\mathcal{F}: \textbf{C} \rightarrow \textbf{D}$
- 射：関手 $\mathcal{F}$ から関手 $\mathcal{G}$ への任意の自然変換 $\vartheta: \mathcal{F} \rightarrow \mathcal{G}$
- 射の合成：自然変換の合成

## Nat
関手圏 $\textbf{D}^{\textbf{C}}$ の対象 $\mathcal{F}, \mathcal{G} \in \textbf{Ob}(\textbf{D}^{\textbf{C}})$ 間の射の全体を $\textrm{Nat}(\mathcal{F}, \mathcal{G})$ で表す。すなわち、

```math
\textrm{Nat}(\mathcal{F}, \mathcal{G}) = \textrm{Hom}_{\textbf{D}^\textbf{C}}(\mathcal{F}, \mathcal{G})
```

である。

## HomC(-, A)
圏 $\textbf{C}$ とその対象 $X \in \textbf{Ob(C)}$ を一つ固定すると、$\textrm{Hom}_{\textbf{C}}(-, X)$ は反変関手 $\textbf{C} \rightarrow \textbf{Set}$ つまり前層となる：

```math
\begin{array}{ccc}
\textbf{Ob(C)} & \longrightarrow & \textbf{Ob(Set)} & \\
⟒ & & ⟒ \\
A & \longmapsto & \textrm{Hom}_{\textbf{C}}(A, X)\\
\\
\textbf{Hom(C)} & \longrightarrow & \textbf{Hom(Set)} & \\
⟒ & & ⟒ \\
f: A \rightarrow B & \longmapsto & \textrm{Hom}_{\textbf{C}}(f, X):& \textrm{Hom}_{\textbf{C}}(B, X) & \rightarrow & \textrm{Hom}_{\textbf{C}}(A, X) \\
& & & ⟒ & & ⟒\\
& & & g & \mapsto & g \circ f
\end{array}
```

# 証明
## 概要
どの空間をベースに話しているのかに注意する。
$\textbf{C}, \textbf{D}$ が局所小圏であっても、関手圏 $\textbf{D}^{\textbf{C}}$ が局所小圏であるとは限らない（と思うが、証明については未調査）。したがって $\textrm{Nat}(\textrm{Hom}\_{\textbf{C}}(-,X), \mathcal{P})$ もこの時点では集合であるかまだわからない。
一方、$\mathcal{P}X \in \textbf{Ob(Set)}$ は集合であるから、こことの（集合としての）同型が言えれば、$\textrm{Nat}(\textrm{Hom}\_{\textbf{C}}(-,X), \mathcal{P})$ も集合だと主張できる。

そこで、2つの写像：

```math
\begin{eqnarray}
\phi&:& \mathcal{P}X \rightarrow \textrm{Nat}(\textrm{Hom}_{\textbf{C}}(-, X), \mathcal{P}) \\
\psi&:& \textrm{Nat}(\textrm{Hom}_{\textbf{C}}(-, X), \mathcal{P}) \rightarrow \mathcal{P}X \\
\end{eqnarray}
```

を作り、これらが互いに逆写像になっていることを確認する。

$\phi$ の定義では、$\forall x \in \mathcal{P}X$ に対し $\vartheta = \phi(x)$ が $\textrm{Hom}_{\textbf{C}}(-, X)$ から $\mathcal{P}$ への自然変換であることを確認する。そのためには、

- $\forall A \in \textbf{Ob(C)}, \vartheta_A$ が $\textrm{Hom}_{\textbf{C}}(A, X)$ から $\mathcal{P}A$ への写像になっていること
- $\forall f: A \rightarrow B \in \textbf{Hom(C)}, \mathcal{P}f \circ \vartheta_B = \vartheta_A \circ \textrm{Hom}_{\textbf{C}}(f, X)$

を確認する必要がある。

$\psi$ の定義では、$\forall \vartheta \in \textrm{Nat}(\textrm{Hom}_{\textbf{C}}(-, X), \mathcal{P})$ に対し $x = \psi(\vartheta) \in \mathcal{P}X$ を確認する。

## φの定義
各 $x \in \mathcal{P}X$ に対し、自然変換 $\vartheta$ を次のように定義する

```math
\begin{array}{cccc}
in \textbf{C} & in \textbf{C}^{\textrm{op}} & & in \textbf{Set}\\
& & \textrm{Hom}_{\textbf{C}}(-, X) & & \mathcal{P}\\
B & B & \textrm{Hom}_{\textbf{C}}(B, X) & \overset{\vartheta_B} \longrightarrow & \mathcal{P}B\\
\phantom{f}\Bigg\uparrow f & \phantom{f}\Bigg\downarrow f & \phantom{\textrm{Hom}_{\textbf{C}}(f, X)}\Bigg\downarrow \textrm{Hom}_{\textbf{C}}(f, X) & \circlearrowright & \phantom{\mathcal{P}f}\Bigg\downarrow \mathcal{P}f\\
A & A & \textrm{Hom}_{\textbf{C}}(A, X) & \overset{\vartheta_A} \longrightarrow & \mathcal{P}A\\
& & ⟒ & & ⟒\\
& & g & \longmapsto & \vartheta_A(g) = \mathcal{P}g(x)
\end{array}
```

### θ_A が Hom_C(A, X) から FA への写像になっていることの確認

$\forall A \in \textbf{Ob(C)}, \forall g \in \textrm{Hom}(A, X)$ に対し、反変関手 $\mathcal{P}$ で移した $\mathcal{P}g$ は

```math
\begin{array}{lrccc}
in \textbf{C} & g: & X & \longleftarrow & A\\
in \textbf{C}^{\textrm{op}} & g: & X & \longrightarrow & A\\
in \textbf{Set} & \mathcal{P}g: & \mathcal{P}X & \longrightarrow & \mathcal{P}A\\
\end{array}
```

となる。よって $\forall x \in \mathcal{P}X$ に対し $\mathcal{P}g(x) \in\mathcal{P}A$ であり、$x, A$ を固定すれば $g$ を $\mathcal{P}g(x)$ に移す写像 $\vartheta_A$ が得られる。

```math
\begin{array}{lccc}
\vartheta_A: &\textrm{Hom}_{\textbf{C}}(A, X) & \longrightarrow & \mathcal{P}A\\
& ⟒ & & ⟒\\
& g & \longmapsto & \vartheta_A(g) = \mathcal{P}g(x)
\end{array}
```

### 図式が可換になっていることの証明
図式：

```math
\begin{array}{cccc}
in \textbf{C} & in \textbf{C}^{\textrm{op}} & & in \textbf{Set}\\
& & \textrm{Hom}_{\textbf{C}}(-, X) & & \mathcal{P}\\
B & B & \textrm{Hom}_{\textbf{C}}(B, X) & \overset{\vartheta_B} \longrightarrow & \mathcal{P}B\\
\phantom{f}\Bigg\uparrow f & \phantom{f}\Bigg\downarrow f & \phantom{\textrm{Hom}_{\textbf{C}}(f, X)}\Bigg\downarrow \textrm{Hom}_{\textbf{C}}(f, X) & \circlearrowright & \phantom{\mathcal{P}f}\Bigg\downarrow \mathcal{P}f\\
A & A & \textrm{Hom}_{\textbf{C}}(A, X) & \overset{\vartheta_A} \longrightarrow & \mathcal{P}A\\
& & ⟒ & & ⟒\\
& & g & \longmapsto & \vartheta_A(g) = \mathcal{P}g(x)
\end{array}
```

の、 $\circlearrowright$ の部分を示す。つまり、$x \in \textbf{F}(X)$ を固定し、$\forall A, B \in \textbf{Ob(C)}, \forall f \in \textrm{Hom}_{\textbf{C}}(A, B)$ に対し、

```math
\vartheta_A \circ \textrm{Hom}_{\textbf{C}}(f, X) = \mathcal{P}f \circ \vartheta_B
```

を示したい。これは集合の写像としての等号なので、

```math
\forall g \in \textrm{Hom}_{\textbf{C}}(B, X), \bigl(\vartheta_A \circ \textrm{Hom}_{\textbf{C}}(f, X)\bigr)(g) = \bigl(\mathcal{P}f \circ \vartheta_B\bigr)(g)
```

が言えれば良い。実際、$\forall g \in \textrm{Hom}_{\textbf{C}}(B, X)$ について、

```math
\begin{eqnarray}
\bigl(\vartheta_A \circ \textrm{Hom}_{\textbf{C}}(f, X)\bigr)(g) & = & \vartheta_A\bigl(\textrm{Hom}_{\textbf{C}}(f, X)(g)\bigr)\\
& = & \vartheta_A\bigl(g \circ f\bigr)\\
& = & \mathcal{P}(g \circ f)(x)\\
& = & \bigl(\mathcal{P}f \circ \mathcal{P}g\bigr)(x)\\
& = & \mathcal{P}f\bigl(\mathcal{P}g(x)\bigr)\\
& = & \mathcal{P}f\bigl(\vartheta_B(g)\bigr)\\
& = & \bigl(\mathcal{P}f \circ \vartheta_B\bigr)(g)\\
\end{eqnarray}
```

であるから、図式が可換となり、 $\vartheta$ が自然変換であることが言えた。

ここまでで、 $x \in \mathcal{P}X$ に対して 自然変換 $\vartheta$ を一つ対応させることが出来た。この対応が写像 $\phi$ である。

## ψの定義
$\vartheta \in \textrm{Nat}(\textrm{Hom}_{\textbf{C}}(-, X), \mathcal{P})$ を一つ取る。

```math
\vartheta_X: \textrm{Hom}_{\textbf{C}}(X, X) \rightarrow \mathcal{P}X
```

であるから、$id_X: X \rightarrow X$ に対して $\vartheta_X(id_X) \in \mathcal{P}X$ である。

そこで、$\vartheta \in \textrm{Nat}(\textrm{Hom}\_{\textbf{C}}(-, X), \mathcal{P})$ から $x = \vartheta\_X(id\_X)$ への対応を考えることができる。この対応が写像 $\psi$ である。

## ψ ∘ φ = id の確認

2つの写像 $\phi, \psi$ が互いに逆写像であることを示す。そのために、まず $\psi \circ \phi = id_{\mathcal{P}X}$ を示す。$\forall x \in \mathcal{P}X$ に対して、

```math
\begin{eqnarray}
\bigl(\psi \circ \phi\bigr)(x) & = & \psi\bigl(\phi(x)\bigr)\\
& = & \bigl(\phi(x)\bigr)_X(id_X)\\
& = & \mathcal{P}(id_X)(x)\\
& = & id_{\mathcal{P}X}(x)\\
\end{eqnarray}
```

$x \in \mathcal{P}X$ は任意であったから、 $\psi \circ \phi = id_{\mathcal{P}X}$ である。

## φ ∘ ψ = id の確認
最後に、 $\phi \circ \psi = id_{\textrm{Nat}(\textrm{Hom}\_{\textbf{C}}(-, X), \mathcal{P})}$ を示す。そのためには、 $\forall \vartheta \in \textrm{Nat}(\textrm{Hom}_{\textbf{C}}(-, X), \mathcal{P})$ について

```math
\bigl( \phi \circ \psi \bigr)(\vartheta) = \vartheta
```

が言えれば良い。

2つの自然変換が同じであることを示すには、$\forall A \in \textbf{Ob(C)}$に対し

```math
\Bigl( \bigl( \phi \circ \psi \bigr)(\vartheta) \Bigr)_A = \vartheta_A
```

が言えれば良い。 これは $\textbf{Set}$ の射 $\textrm{Hom}_{\textbf{C}}(A, X) \rightarrow \textbf{F}(A)$ 同士の比較である。

2つの写像が同じであることを示すには、 $\forall g \in \textrm{Hom}_{\textbf{C}}(A, X)$ に対し

```math
\Bigl( \bigl( \phi \circ \psi \bigr)(\vartheta) \Bigr)_A(g) = \vartheta_A(g)
```

が言えればよい。そこで、左辺を変形して右辺と一致することを目指す。以下で、 $\vartheta, A, g$ は任意である。$\phi$ の定義と $\psi$ の定義、及び以下の可換図式：

```math
\begin{array}{cccc}
in \textbf{C} & in \textbf{C}^{\textrm{op}} & & in \textbf{Set}\\
& & \textrm{Hom}_{\textbf{C}}(-, X) & & \mathcal{P}\\
X & X & \textrm{Hom}_{\textbf{C}}(X, X) & \overset{\vartheta_X} \longrightarrow & \mathcal{P}X\\
\phantom{g}\Bigg\uparrow g & \phantom{g}\Bigg\downarrow g & \phantom{\textrm{Hom}_{\textbf{C}}(g, X)}\Bigg\downarrow \textrm{Hom}_{\textbf{C}}(g, X) & \circlearrowright & \phantom{\mathcal{P}g}\Bigg\downarrow \mathcal{P}g\\
A & A & \textrm{Hom}_{\textbf{C}}(A, X) & \overset{\vartheta_A} \longrightarrow & \mathcal{P}A\\
& & ⟒ & & ⟒\\
& & g & \longmapsto & \phi(x)_A(g) = \mathcal{P}g(x)
\end{array}
```

に注意して、

```math
\begin{eqnarray}
\Bigl( \bigl( \phi \circ \psi \bigr)(\vartheta) \Bigr)_A(g) & = & \Bigl( \phi \bigl( \psi(\vartheta) \bigr) \Bigr)_A(g)\\
& = & \mathcal{P}g\bigl(\psi(\vartheta)\bigr)\\
& = & \mathcal{P}g\bigl(\vartheta_X(id_X)\bigr)\\
& = & \bigl(\mathcal{P}g \circ \vartheta_X\bigr)(id_X)\\
& = & \bigl(\vartheta_A \circ \textrm{Hom}_{\textbf{C}}(g, X)\bigr)(id_X)\\
& = & \vartheta_A\bigl(\textrm{Hom}_{\textbf{C}}(g, X)(id_X)\bigr)\\
& = & \vartheta_A(id_X \circ g)\\
& = & \vartheta_A(g)\\
\end{eqnarray}
```

$g$ は任意であったから、

```math
\Bigl( \bigl( \phi \circ \psi \bigr)(\vartheta) \Bigr)_A = \vartheta_A
```

$A$ は任意であったから、

```math
\bigl( \phi \circ \psi \bigr)(\vartheta) = \vartheta
```

$\vartheta$ は任意であったから、

```math
\phi \circ \psi = id_{\textrm{Nat}(\textrm{Hom}\_{\textbf{C}}(-, X), \mathcal{P})}
```

が言えた。

以上により、

```math
\textrm{Nat}(\textrm{Hom}_{\textbf{C}}(-,X), \mathcal{P}) \cong \mathcal{P}X
```

であることが証明された。