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.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject 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.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject 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.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject 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 ℤ] (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₁))

noncomputable instance CategoryTheory.Pretriangulated.instShiftSequenceOppositeAddCommGrpObjFunctorPreadditiveYonedaInt {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (B : C) : (CategoryTheory.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (B : C) {X Y : Cᵒᵖ} (n : ℤ) (f : X ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ n).obj Y) (a a' : ℤ) (h : n + a = a') (z : Opposite.unop X ⟶ (CategoryTheory.shiftFunctor C a).obj B) : ((CategoryTheory.preadditiveYoneda.obj B).shiftMap f a a' h) z = ((CategoryTheory.ShiftedHom.opEquiv n).symm f).comp z ⋯

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