層圏トポス: 前層の2つの定義の同値性その1

前層の第一の定義から第二の定義が導けることについて、本では詳細が割愛されていたのでそれを証明します。 (p.14)

第一の定義によって前層が定義されていると仮定して、第二の定義による前層を導きます。

第一の定義による前層の仮定

p.13~ の定義より次が仮定できます。

A : Set\\
E : A \to \mathfrak{O}(U)\\
\neg : A \times \mathfrak{O}(U) \to A\\

そして、第一の定義の４つの性質が成り立つものと仮定できます。

Fとrを具体的に構成する

ここで、 $F$ と $r_{UV}$ を次で与えます。

F: A \to A\\
F(U) := \left\{f \in A \mid Ef=U \right\} ~~ (つまりEの逆像)\\
U\subset V のとき、
r_{UV} : F(V) \to F(U) を次で与える\\
f\in F(V)について、 r_{UV}(f) := f\neg U ~~(\in F(U))

この作り方で関数 $r_{UV}$ が $F(V) \to F(U)$ に本当になっているかですが、今 $U\subset V$ であって、$Ef = V$ なので、 $E(f\neg U) = V \cap U = U$ となって大丈夫です。

第二の定義の性質を満たすことを示す

これから $F, r_{UV}$ が前層の第二の定義に従うことを示します。それは次の３つの項目でした。

1. $F(\emptyset)$ が単一集合
2. $r_{UU}$ が恒等写像
3. $U\subset V \subset W$ ならば $r_{UW} = r_{UV} \circ r_{VW}$

順番に示します。

1. について

$\forall f, g\in F(\emptyset)$ について $f = g$ を示すという方針で示します。

今、 $F$の与え方から次が成り立ちます。

F(\emptyset) = \left\{ f \mid Ef = \emptyset \right\}

なので $Ef = Eg = \emptyset$ が成り立ちます、ここで前層の第一の定義より $f\neg Ef = f$ も成り立つので、 $f\neg \emptyset = f$ となります。
同様に $g\neg \emptyset = g$ ともなります。
前層の第一の定義より $f\neg \emptyset = g\neg \emptyset$ となるため、 $f=g$ となるわけです。

($F(\emptyset)$ が空になることはありえない...?)

2. について

任意の $f \in F(U)$ について

\begin{eqnarray}
r_{UU}(f) &=& f\neg U\\
          &=& (f\neg Ef)\neg U\\
          &=& f \neg (U \cap U)\\
          &=& f \neg U\\
          &=& f
\end{eqnarray}

よって恒等写像になります。

3. について

$U \subset V \subset W$のとき、任意の $f \in F(W)$ について、 $r_{UW}(f) = r_{UV}(r_{VW}(f))$ を示します。

\begin{eqnarray}
(右辺) &=& r_{UV}(r_{VW}(f))\\
       &=& r_{UV}(f \neg V)\\
       &=& (f\neg V) \neg U\\
       &=& f \neg (V\cap U)\\
       &=& f \neg U\\
       &=& (左辺)
\end{eqnarray}

以上です。