The Yoneda functors are homological

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

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

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

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

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

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

noncomputable instance CategoryTheory.Pretriangulated.instShiftSequenceOppositeAddCommGrpCatObjFunctorPreadditiveYonedaInt {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (B : C) : (preadditiveYoneda.obj B).ShiftSequence ℤ

theorem CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (B : C) {X Y : Cᵒᵖ} (n : ℤ) (f : X ⟶ (shiftFunctor Cᵒᵖ n).obj Y) (a a' : ℤ) (h : n + a = a') (z : Opposite.unop X ⟶ (shiftFunctor C a).obj B) : (ConcreteCategory.hom ((preadditiveYoneda.obj B).shiftMap f a a' h)) z = ((ShiftedHom.opEquiv n).symm f).comp z ⋯

theorem CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (T : Triangle C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {B : C} (x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B) : (ConcreteCategory.hom ((preadditiveYoneda.obj B).homologySequenceδ ((triangleOpEquivalence C).functor.obj (Opposite.op T)) n₀ n₁ h)) x = CategoryStruct.comp T.mor₃ (CategoryStruct.comp ((shiftFunctor C 1).map x) ((shiftFunctorAdd' C n₀ 1 n₁ h).inv.app B))