English
Let C be a preadditive category endowed with an integer-graded shift, and T a triangle in C. For integers n0, n1 with n0 + 1 = n1 and any morphism x: T.obj1 ⟶ B⟦n0⟧, the δ-map in the preadditive Yoneda homology sequence applied to T and B sends x to the composite T.mor3 followed by the shifted x and the inverse of the shift-add morphism: δ(x) = T.mor3 ≫ x⟦1⟧' ≫ (shiftFunctorAdd' C n0 1 n1 h).inv.app B.
Русский
Пусть C — прeд-addитивная категория с целочисленным сдвигом; T — треугольник в C. Пусть n0, n1 ∈ ℤ и n0 + 1 = n1, и дано отображение x: T.obj1 ⟶ B⟦n0⟧. Тогда δ в последовательности Хоноеды ( Yoneda ) применительно к T и B отправляет x в композицию T.mor3 ∘ x^{(1)} ∘ (shiftFunctorAdd' C n0 1 n1 h)^{-1}_{B}.
LaTeX
$$$$(\text{preadditiveYoneda.obj } B).homologySequenceδ ((\triangleOpEquivalence _).functor.obj (\text{op } T))_{n_0 n_1 h} \, x = T.mor_3 \circ x^{(1)} \circ \bigl(\text{shiftFunctorAdd}' C\; n_0\; 1\; n_1\; h\bigr)^{-1}_{B}.$$$$
Lean4
theorem preadditiveYoneda_homologySequenceδ_apply (T : Triangle C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {B : C}
(x : T.obj₁ ⟶ B⟦n₀⟧) :
(preadditiveYoneda.obj B).homologySequenceδ ((triangleOpEquivalence _).functor.obj (op T)) n₀ n₁ h x =
T.mor₃ ≫ x⟦(1 : ℤ)⟧' ≫ (shiftFunctorAdd' C n₀ 1 n₁ h).inv.app B :=
by
simp only [Functor.homologySequenceδ, preadditiveYoneda_shiftMap_apply, ShiftedHom.comp, ← Category.assoc]
congr 2
apply (ShiftedHom.opEquiv _).injective
rw [Equiv.apply_symm_apply]
rfl
