Theorems · Definition · category theory

CategoryTheory.ShortComplex.ShortExact.singleTriangleIso

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        {S : CategoryTheory.ShortComplex C} → (hS : S.ShortExact) → hS.singleTriangle ≅ DerivedCategory.triangleOfSES ⋯

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.

Defined in

Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle

Cited by

7 results in Mathlib

Foundations

Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianHasDerivedCategory