trianglehOfDegreewiseSplit — Mathlib

English

There exists a canonical isomorphism between the triangle built from a degreewise split short exact sequence and the mapping cone triangle of the corresponding homomorphism.

Русский

Существует каноническое изоморфизм между треугольником, построенным из разложенной по степеням короткой точной последовательности, и треугольником\MappingCone соответствующего гомоморфизма.

LaTeX

$$$\\triangle_{deg\\-split} \\cong \\text{mappingCone}(\\text{homOfDegreewiseSplit})$$$

Lean4

/-- The (distinguished) triangle in `HomotopyCategory C (ComplexShape.up ℤ)` attached to a
degreewise split short exact sequence of cochain complexes. -/
noncomputable abbrev trianglehOfDegreewiseSplit : Triangle (HomotopyCategory C (ComplexShape.up ℤ)) :=
  (HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj (triangleOfDegreewiseSplit S σ)

Похожие утверждения