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.

instance CategoryTheory.Pretriangulated.instIsHomologicalAddCommGrpObjOppositeFunctorPreadditiveCoyoneda {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (A : Cᵒᵖ) : (CategoryTheory.preadditiveCoyoneda.obj A).IsHomological

Equations

• ⋯ = ⋯

instance CategoryTheory.Pretriangulated.instIsHomologicalOppositeAddCommGrpObjFunctorPreadditiveYoneda {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (B : C) : (CategoryTheory.preadditiveYoneda.obj B).IsHomological

Equations

• ⋯ = ⋯

theorem CategoryTheory.Pretriangulated.preadditiveYoneda_map_distinguished {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (B : C) : ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).op.map (CategoryTheory.preadditiveYoneda.obj B)).Exact

noncomputable instance CategoryTheory.Pretriangulated.instShiftSequenceAddCommGrpObjOppositeFunctorPreadditiveCoyonedaInt {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (A : Cᵒᵖ) : (CategoryTheory.preadditiveCoyoneda.obj A).ShiftSequence ℤ

Equations

• CategoryTheory.Pretriangulated.instShiftSequenceAddCommGrpObjOppositeFunctorPreadditiveCoyonedaInt A = CategoryTheory.Functor.ShiftSequence.tautological (CategoryTheory.preadditiveCoyoneda.obj A) ℤ

theorem CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (A : Cᵒᵖ) (T : CategoryTheory.Pretriangulated.Triangle C) (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) (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₁))