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

Stacks Tag 0149

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

Stacks Tag 0149

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

@[instance_reducible]

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 ℤ

Equations

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

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 ⟶ T.obj₃⟦n₀⟧) : (ConcreteCategory.hom ((preadditiveCoyoneda.obj A).homologySequenceδ T n₀ n₁ h)) x = CategoryStruct.comp x (CategoryStruct.comp (T.mor₃⟦n₀⟧') ((shiftFunctorAdd' C 1 n₀ n₁ ⋯).inv.app T.obj₁))

@[instance_reducible]

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 ℤ

Equations

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

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 ⟶ Y⟦n⟧) (a a' : ℤ) (h : n + a = a') (z : Opposite.unop X ⟶ B⟦a⟧) : (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₁ ⟶ B⟦n₀⟧) : (ConcreteCategory.hom ((preadditiveYoneda.obj B).homologySequenceδ ((triangleOpEquivalence C).functor.obj (Opposite.op T)) n₀ n₁ h)) x = CategoryStruct.comp T.mor₃ (CategoryStruct.comp (x⟦1⟧') ((shiftFunctorAdd' C n₀ 1 n₁ h).inv.app B))