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} [Category.{u_2, 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.instIsHomologicalOppositeAddCommGrpObjFunctorPreadditiveYoneda {C : Type u_1} [Category.{u_2, 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.{u_2, 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.instShiftSequenceAddCommGrpObjOppositeFunctorPreadditiveCoyonedaInt {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [HasShift C ℤ] (A : Cᵒᵖ) : (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} [Category.{u_2, 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₃) : ((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.instShiftSequenceOppositeAddCommGrpObjFunctorPreadditiveYonedaInt {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (B : C) : (preadditiveYoneda.obj B).ShiftSequence ℤ

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply {C : Type u_1} [Category.{u_2, 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) : ((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.{u_2, 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) : ((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))