ホモトピー可換な正方形から錐の射を作る

補題 5.2（「三角圏とホモトピー圏の三角構造」§5）・ ✓公理まで証明済み

鎖写像 $f\colon X \to Y$ 、 $f_1\colon X_1 \to Y_1$ 、 $a\colon X \to X_1$ 、 $b\colon Y \to Y_1$ と、射の族 $h^n\colon X^n \to Y_1^{n-1}$ で

b f - f_1 a = d h + h d

を満たすものが与えられたとする。このとき

c_h\colon \operatorname{Cone}(f) \to \operatorname{Cone}(f_1), \qquad c_h(x, y) = (a x,\ b y + h x)

（ $x \in X^{n+1}$ 、 $y \in Y^n$ 、 $h x \in Y_1^n$ ）は鎖写像で、 $c_h i = i_1 b$ 、 $p_1 c_h = a[1] p$ が鎖写像として成り立つ。

閉包の状態

✓ 公理まで証明済み

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

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

証明は Rikai の他の定理を参照していません（定義と論理だけで示されています）。