導来圏は三角圏

定理 4.3（「導来圏と全導来関手」§4）・ ✓公理まで証明済み

$\mathcal{A}$ をアーベル圏とする。

$\mathrm{D}^{*}(\mathcal{A})$ は三角圏で、 $Q : \mathrm{K}^{*}(\mathcal{A}) \to \mathrm{D}^{*}(\mathcal{A})$ は三角関手である。 $\mathrm{K}^{*}(\mathcal{A})$ の射 $f$ について、 $Q(f)$ が同型であることと $f$ が擬同型であることは同値である。
擬同型を同型に送る関手 $F : \mathrm{K}^{*}(\mathcal{A}) \to \mathcal{E}$ は、関手 $\bar F$ によって $F = \bar F Q$ とただ一通りに分解する。 $F$ が三角関手なら $\bar F$ も三角関手である。
$H^0$ は $Q$ を経由してコホモロジー的関手 $H^0 : \mathrm{D}(\mathcal{A}) \to \mathcal{A}$ を与え、 $H^0(X[n]) = H^n(X)$ である。

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

閉包の状態

✓ 公理まで証明済み

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

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

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

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

擬同型は乗法系をなす✓命題 4.1・導来圏と全導来関手
- $H^0$ はコホモロジー的✓命題 5.6・三角圏とホモトピー圏の三角構造（上で展開済み）
- コホモロジー的関手の核は厚い✓命題 4.7・三角圏とホモトピー圏の三角構造
  - 加法関手と双積✓命題 3.7・加法圏とアーベル圏この先をたどる →
  - コホモロジー的関手の長完全列✓命題 4.2・三角圏とホモトピー圏の三角構造この先をたどる →
  - 有限積・有限余積・双積の一致✓命題 3.3・加法圏とアーベル圏
- 擬同型と錐の非輪状性✓系 5.4・鎖複体とホモトピー圏
  - 写像錐の長完全列✓定理 5.3・鎖複体とホモトピー圏この先をたどる →
  - 完全性の判定✓補題 5.2・加法圏とアーベル圏この先をたどる →
  - アーベル圏の mono・epi と平衡性✓命題 4.3・加法圏とアーベル圏この先をたどる →
- Verdier 商の存在✓定理 3.1・導来圏と全導来関手（上で展開済み）
Verdier 商の存在✓定理 3.1・導来圏と全導来関手
- Hom の完全性✓命題 3.2・三角圏とホモトピー圏の三角構造
  - 完全三角形の基本性質✓命題 3.1・三角圏とホモトピー圏の三角構造
- 完全三角形の基本性質✓命題 3.1・三角圏とホモトピー圏の三角構造
- 三角形のシフト✓系 3.9・三角圏とホモトピー圏の三角構造
  - TR2 の後半は他の公理から従う✓補題 3.8・三角圏とホモトピー圏の三角構造（上で展開済み）
- 加法圏の局所化✓命題 2.4・導来圏と全導来関手
  - 分数の圏による局所化✓定理 2.3・導来圏と全導来関手（上で展開済み）
  - 加群のフィルター余極限は完全✓系 6.5・極限と余極限この先をたどる →
  - 双積定義 3.2・加法圏とアーベル圏
  - 加法圏定義 3.4・加法圏とアーベル圏
- Verdier 商の TR3✓補題 8.5・導来圏と全導来関手
  - 分数の圏による局所化✓定理 2.3・導来圏と全導来関手（上で展開済み）
  - 錐の取り替え✓補題 8.4・導来圏と全導来関手この先をたどる →
- Verdier 商の TR4✓補題 8.6・導来圏と全導来関手
  - Verdier 商の TR3✓補題 8.5・導来圏と全導来関手（上で展開済み）
  - 錐の一意性✓系 3.5・三角圏とホモトピー圏の三角構造この先をたどる →
- TR2 の後半は他の公理から従う✓補題 3.8・三角圏とホモトピー圏の三角構造
  - 錐の一意性✓系 3.5・三角圏とホモトピー圏の三角構造この先をたどる →
- 三角形の五項補題✓命題 3.4・三角圏とホモトピー圏の三角構造
  - Hom の完全性✓命題 3.2・三角圏とホモトピー圏の三角構造（上で展開済み）
  - Hom による五項補題✓補題 3.3・三角圏とホモトピー圏の三角構造この先をたどる →
  - 完全三角形の基本性質✓命題 3.1・三角圏とホモトピー圏の三角構造
- 分数の圏による局所化✓定理 2.3・導来圏と全導来関手
  - 宇宙の公理公理 2.2・圏・関手・自然変換
  - 宇宙の閉性✓命題 2.3・圏・関手・自然変換この先をたどる →
  - フィルター圏・順極限・逆極限定義 6.1・極限と余極限
  - 集合のフィルター余極限の記述✓命題 6.3・極限と余極限この先をたどる →
圏の局所化定義 2.2・導来圏と全導来関手
$H^0$ はコホモロジー的✓命題 5.6・三角圏とホモトピー圏の三角構造
- ホモトピー圏は三角圏✓定理 5.5・三角圏とホモトピー圏の三角構造この先をたどる →
- コホモロジー的関手定義 4.1・三角圏とホモトピー圏の三角構造
- コホモロジー的関手の核は厚い✓命題 4.7・三角圏とホモトピー圏の三角構造（上で展開済み）
- 錐の一意性✓系 3.5・三角圏とホモトピー圏の三角構造この先をたどる →
- ホモトピー圏は加法圏✓命題 4.4・鎖複体とホモトピー圏この先をたどる →
- シフト定義 2.5・鎖複体とホモトピー圏
- 写像錐の長完全列✓定理 5.3・鎖複体とホモトピー圏この先をたどる →
- 完全性の判定✓補題 5.2・加法圏とアーベル圏この先をたどる →
- 擬同型と錐の非輪状性✓系 5.4・鎖複体とホモトピー圏（上で展開済み）

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

アーベル圏は導来圏に充満忠実に入る✓命題 4.5・導来圏と全導来関手
D⁺(A) の局所的な小ささ✓系 5.4・導来圏と全導来関手
導来関手の再定式化✓系 6.4・導来圏と全導来関手

導来圏は三角圏

閉包の状態

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

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

関連するノック 2 問

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

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