English
There is an isomorphism between the special triangle coming from a short exact sequence via SES and the standard SES-derived triangle after applying the single functor.
Русский
Существует изоморфизм между треугольником, полученным из SES через единичный функтор, и стандартным треугольником SES-производной категории.
LaTeX
$$$$ hS.singleTriangle \cong \mathrm{triangleOfSES}(hS.map_of_exact(\mathrm{HomologicalComplex.single}(C, (ComplexShape.up \mathbb{Z}) , 0))) $$$$
Lean4
/-- Given a short exact complex `S` in `C` that is short exact (`hS`), this is the
canonical isomorphism between the triangle `hS.singleTriangle` in the derived category
and the triangle attached to the corresponding short exact sequence of cochain complexes
after the application of the single functor. -/
@[simps!]
noncomputable def singleTriangleIso :
hS.singleTriangle ≅ triangleOfSES (hS.map_of_exact (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) :=
by
let e := (SingleFunctors.evaluation _ _ 0).mapIso (singleFunctorsPostcompQIso C)
refine Triangle.isoMk _ _ (e.app S.X₁) (e.app S.X₂) (e.app S.X₃) ?_ ?_ ?_
· cat_disch
· cat_disch
· simp [singleδ, e, ← Functor.map_comp, CochainComplex.singleFunctors]
