English
The boundary δ in the preadditive Yoneda homology sequence for the single triangle, applied to x.hom, coincides with the Ext-boundary given by hS.extClass.
Русский
Граница δ в гомологической последовательности Юона для одинокого треугольника, применённая к x.hom, совпадает с границей Ext, заданной hS.extClass.
LaTeX
$$$\\text{preadditiveYoneda}_{\\,C}((\\mathrm{singleFunctor} C 0).obj Y)\\mathrm{homologySequence\\delta}((\\triangleOpEquivalence _).functor.obj (op hS.singleTriangle)) n_0 n_1 (\\text{by cutsat}) x.hom = (hS.extClass \\cdot x).hom$$$
Lean4
theorem preadditiveYoneda_homologySequenceδ_singleTriangle_apply [HasDerivedCategory.{w'} C] {Y : C} {n₀ : ℕ}
(x : Ext S.X₁ Y n₀) {n₁ : ℕ} (h : 1 + n₀ = n₁) :
(preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
((triangleOpEquivalence _).functor.obj (op hS.singleTriangle)) n₀ n₁ (by cutsat) x.hom =
(hS.extClass.comp x h).hom :=
by
rw [preadditiveYoneda_homologySequenceδ_apply, comp_hom, hS.extClass_hom, ShiftedHom.comp]
rfl
