English
For A in Cᵒᵖ, the object preadditiveCoyoneda.obj A carries a ShiftSequence ℤ structure.
Русский
Для A в Cᵒᵖ объект preadditiveCoyoneda.obj A имеет структуру ShiftSequence ℤ.
LaTeX
$$$(\\text{preadditiveCoyoneda.obj } A).\\text{ShiftSequence} \\mathbb{Z}$$$
Lean4
instance (B : C) : (preadditiveYoneda.obj B).IsHomological where
exact T
hT := by
rw [ShortComplex.ab_exact_iff]
intro (x₂ : T.obj₂.unop ⟶ B) (hx₂ : T.mor₂.unop ≫ x₂ = 0)
obtain ⟨x₃, hx₃⟩ := Triangle.yoneda_exact₂ _ (unop_distinguished T hT) x₂ hx₂
exact ⟨x₃, hx₃.symm⟩
