Documentation

Mathlib.CategoryTheory.Triangulated.Yoneda

The Yoneda functors are homological #

Let C be a pretriangulated category. In this file, we show that the functors preadditiveCoyoneda.obj A : C ⥤ AddCommGrp for A : Cᵒᵖ and preadditiveYoneda.obj B : Cᵒᵖ ⥤ AddCommGrp for B : C are homological functors.

theorem CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ] (T : CategoryTheory.Pretriangulated.Triangle C) (n₀ : ) (n₁ : ) (h : n₀ + 1 = n₁) {A : Cᵒᵖ} (x : Opposite.unop A (CategoryTheory.shiftFunctor C n₀).obj T.obj₃) :
((CategoryTheory.preadditiveCoyoneda.obj A).homologySequenceδ T n₀ n₁ h) x = CategoryTheory.CategoryStruct.comp x (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n₀).map T.mor₃) ((CategoryTheory.shiftFunctorAdd' C 1 n₀ n₁ ).inv.app T.obj₁))