English
The standard triangle associated to a morphism φ in a cochain category is realized as the image of a triangle in the homotopy/derived category, built from φ, inr φ, and the shifted cokernel map.
Русский
Стандартный треугольник, связанный с морфизмом φ в когэпойнтовом категории, реализуется как образ треугольника в гомотопической/производной категории, построенного из φ, inr φ и сдвинутого сопряженного отображения.
LaTeX
$$$\\triangle φ = (φ: K \\to L) \\to (inr φ: L \\to \\mathrm{mappingCone}\\,φ) \\to ( -\\mathrm{fst} φ: \\mathrm{mappingCone} φ \\to K⟦1⟧) $$$
Lean4
/-- The standard triangle `K ⟶ L ⟶ mappingCone φ ⟶ K⟦(1 : ℤ)⟧` in `CochainComplex C ℤ`
attached to a morphism `φ : K ⟶ L`. It involves `φ`, `inr φ : L ⟶ mappingCone φ` and
the morphism induced by the `1`-cocycle `-mappingCone.fst φ`. -/
@[simps! obj₁ obj₂ obj₃ mor₁ mor₂]
noncomputable def triangle : Triangle (CochainComplex C ℤ) :=
Triangle.mk φ (inr φ) (Cocycle.homOf ((-fst φ).rightShift 1 0 (zero_add 1)))
