層の圏は Grothendieck 圏

定理 8.2（「層」§8）・ ✓公理まで証明済み

$\mathcal{O}$ を $X$ 上の環の前層とする。開集合 $U$ に対し、 $\mathcal{O}$ 加群の前層

P_U(V) = \begin{cases} \mathcal{O}(V) & (V \subseteq U) \\ 0 & (V \not\subseteq U) \end{cases}

の層化を $\mathcal{O}_{U!}$ と書く（ $\mathcal{O}$ が層なら定義 7.1 の $j_!(\mathcal{O}|_U)$ である）。

$\mathsf{Mod}(\mathcal{O})$ は任意の小さい族の余積をもつ。茎を取る関手は余極限と交換する: $(\varinjlim_i \mathcal{F}_i)_x \cong \varinjlim_i (\mathcal{F}_i)_x$ 、とくに $(\bigoplus_\lambda \mathcal{F}_\lambda)_x \cong \bigoplus_\lambda (\mathcal{F}_\lambda)_x$ 。
$\mathsf{Mod}(\mathcal{O})$ で、フィルター余極限は完全である（AB5。定義 6.3［射影対象・入射対象と Grothendieck 圏］）。
$\mathcal{O}$ 加群の層 $\mathcal{F}$ について、 $\mathcal{F}$ について自然な全単射 $\operatorname{Hom}_{\mathsf{Mod}(\mathcal{O})}(\mathcal{O}_{U!}, \mathcal{F}) \cong \mathcal{F}(U)$ がある。族 $(\mathcal{O}_{U!})_{U}$ は生成集合で、 $\bigoplus_U \mathcal{O}_{U!}$ は生成子（定義 6.1［射影対象・入射対象と Grothendieck 圏］）である。
$\mathsf{Mod}(\mathcal{O})$ は Grothendieck 圏（定義 6.4［射影対象・入射対象と Grothendieck 圏］）であり、十分に入射対象をもつ。

とくに $\mathsf{Ab}(X)$ と、環付き空間 $(X, \mathcal{O}_X)$ の $\mathsf{Mod}(\mathcal{O}_X)$ は、十分に入射対象をもつ Grothendieck 圏である。

本文で読む（証明と前後の説明）→

閉包の状態

✓ 公理まで証明済み

証明が使う定理を前提としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 62 件、定義なども含めて 76 件）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

前提をたどる証明が使う定理・定義（直接 9 件）

▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。

層の圏はアーベル圏で、完全性は茎で判定できる✓定理 5.2・層
- 加法圏定義 3.4・加法圏とアーベル圏
- 核・余核・像・余像定義 2.1・加法圏とアーベル圏
- 層化の存在と普遍性✓定理 4.3・層（上で展開済み）
- 加群のフィルター余極限は完全✓系 6.5・極限と余極限（上で展開済み）
- 核と余核の基本性質✓補題 2.2・加法圏とアーベル圏
- 茎による単射・全射・同型の判定✓命題 3.2・層
- 芽の族の層✓補題 4.2・層
  - 茎による単射・全射・同型の判定✓命題 3.2・層
- 完全性の判定✓補題 5.2・加法圏とアーベル圏
  - 像分解✓定理 4.4・加法圏とアーベル圏この先をたどる →
  - アーベル圏の mono・epi と平衡性✓命題 4.3・加法圏とアーベル圏この先をたどる →
  - 双対圏もアーベル圏✓命題 4.2・加法圏とアーベル圏この先をたどる →
  - 加群の圏はアーベル圏✓命題 4.6・加法圏とアーベル圏この先をたどる →
- 完全関手は完全列を保つ✓命題 5.4・加法圏とアーベル圏（上で展開済み）
- 関手圏はアーベル圏✓命題 5.7・加法圏とアーベル圏（上で展開済み）
層化の存在と普遍性✓定理 4.3・層
- 芽の族の層✓補題 4.2・層（上で展開済み）
- 茎による単射・全射・同型の判定✓命題 3.2・層
- 普遍射の族から随伴✓定理 2.7・随伴関手と随伴関手定理
  - 選択公理公理 3.1・選択公理と Zorn の補題
  - 随伴の三つの定義の同値✓定理 2.3・随伴関手と随伴関手定理
  - パラメータ付きの表現可能性✓命題 5.1・米田の補題と表現可能関手この先をたどる →
- 加群のフィルター余極限は完全✓系 6.5・極限と余極限（上で展開済み）
余積から余極限へ✓補題 6.2・射影対象・入射対象と Grothendieck 圏
- 積と等化子から極限✓定理 3.1・極限と余極限
- フィルター圏・順極限・逆極限定義 6.1・極限と余極限
茎と摩天楼層の随伴✓補題 6.4・層
- 右随伴は極限を保つ✓定理 3.1・随伴関手と随伴関手定理この先をたどる →
関手圏はアーベル圏✓命題 5.7・加法圏とアーベル圏
- 関手圏は圏であり、大きさが保たれる✓命題 5.4・圏・関手・自然変換この先をたどる →
- 核と余核の基本性質✓補題 2.2・加法圏とアーベル圏
- アーベル圏の mono・epi と平衡性✓命題 4.3・加法圏とアーベル圏この先をたどる →
- 完全性の判定✓補題 5.2・加法圏とアーベル圏（上で展開済み）
加群のフィルター余極限は完全✓系 6.5・極限と余極限
- フィルター圏の有限な条件✓補題 6.2・極限と余極限
- 集合のフィルター余極限の記述✓命題 6.3・極限と余極限
  - フィルター圏の有限な条件✓補題 6.2・極限と余極限
- フィルター圏・順極限・逆極限定義 6.1・極限と余極限
完全関手は完全列を保つ✓命題 5.4・加法圏とアーベル圏
- 完全性の判定✓補題 5.2・加法圏とアーベル圏（上で展開済み）
- アーベル圏の mono・epi と平衡性✓命題 4.3・加法圏とアーベル圏この先をたどる →
- 像分解✓定理 4.4・加法圏とアーベル圏この先をたどる →
- 核と余核の基本性質✓補題 2.2・加法圏とアーベル圏
- 双対圏もアーベル圏✓命題 4.2・加法圏とアーベル圏この先をたどる →
生成子の性質✓補題 6.6・射影対象・入射対象と Grothendieck 圏
- 核と余核の基本性質✓補題 2.2・加法圏とアーベル圏
- 像分解✓定理 4.4・加法圏とアーベル圏この先をたどる →
- 宇宙の閉性✓命題 2.3・圏・関手・自然変換この先をたどる →
Grothendieck 圏は十分に入射対象をもつ✓定理 7.3・射影対象・入射対象と Grothendieck 圏この先をたどる →

これを使っている定理証明で参照している 1 件

コホモロジーと順極限の交換✓補題 6.3・層コホモロジー

層の圏は Grothendieck 圏

閉包の状態

前提をたどる 証明が使う定理・定義（直接 9 件）

これを使っている定理 証明で参照している 1 件

前提をたどる証明が使う定理・定義（直接 9 件）

これを使っている定理証明で参照している 1 件