preadditiveCoyoneda_homologySequenceδ_apply

English

A δ-shaped morphism in the homology sequence respects the shift map δ and composition with mor-sequencing maps.

Русский

Морфизм δ в гомологической последовательности совместим с отображением сдвига и композициями mor-секвенций.

LaTeX

$$$\\text{preadditiveCoyoneda.obj A}.homologySequenceδ T n_0 n_1 h x = x \\;\\cdot\\; T.mor_3^{n_0} \\;\\cdot\\; (\\text{shiftFunctorAdd'} C 1 n_0 n_1)^{-1}_{\\text{app}}$$$

Lean4

theorem preadditiveCoyoneda_homologySequenceδ_apply (T : Triangle C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {A : Cᵒᵖ}
    (x : A.unop ⟶ T.obj₃⟦n₀⟧) :
    (preadditiveCoyoneda.obj A).homologySequenceδ T n₀ n₁ h x =
      x ≫ T.mor₃⟦n₀⟧' ≫ (shiftFunctorAdd' C 1 n₀ n₁ (by cutsat)).inv.app _ :=
  by apply Category.assoc

Похожие утверждения