English
Let C be an abelian category with HasExt and HasDerivedCategory. For any X and a short exact S, and for indices n0, n1 with n0 + 1 = n1, the boundary map δ in the Coyoneda homology sequence associated to the single triangle agrees with the Ext boundary given by composing with the ext-class hS.extClass. In particular, for any x in Ext(X, S.X3, n0), the δ-image of x.hom equals the hom of x composed with hS.extClass h.
Русский
Пусть C — абелева категория с наличии Ext и Derived. Для объекта X и короткой точной последовательности S, и для цифр n0, n1 с n0 + 1 = n1, граница δ в гомологической последовательности Coyoneda, связанной с единичным треугольником, совпадает с границей Ext и достигается композицией с_extClass. В частности, для любого x ∈ Ext(X, S.X3, n0) образ δ на x.hom равен гомоморфизму x, скомпонованному с hS.extClass h.
LaTeX
$$$\\Big(\\mathrm{preadditiveCoyoneda}(\\mathrm{op}((\\mathrm{singleFunctor} C 0).obj X))\\Big)\\mathrm{homologySequence}\\delta_{hS.singleTriangle}^{n_0,n_1}(x.\\mathrm{hom}) = (x.\\mathrm{comp} hS.extClass h).\\mathrm{hom}$$$
Lean4
theorem preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply [HasDerivedCategory.{w'} C] {X : C} {n₀ : ℕ}
(x : Ext X S.X₃ n₀) {n₁ : ℕ} (h : n₀ + 1 = n₁) :
(preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle n₀ n₁ (by cutsat)
x.hom =
(x.comp hS.extClass h).hom :=
by
rw [Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply, comp_hom, hS.extClass_hom, ShiftedHom.comp]
rfl
