homologySequenceδ — Mathlib

English

For a homological functor F and a distinguished triangle T, δ is the connecting morphism in the long exact sequence built from the shifted images of T.

Русский

Для гомологического функторa F и выделенного треугольника T δ — это соединяющий морфизм в длинной точной последовательности, получаемой из сдвигов образов T.

LaTeX

$$$\delta_{F,T,n_0,n_1,h}: (F\ shift\ n_0).obj T.obj_3 \to (F\ shift\ n_1).obj T.obj_1$$$

Lean4

/-- The connecting homomorphism in the long exact sequence attached to an homological
functor and a distinguished triangle. -/
noncomputable def homologySequenceδ [F.ShiftSequence ℤ] (T : Triangle C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) :
    (F.shift n₀).obj T.obj₃ ⟶ (F.shift n₁).obj T.obj₁ :=
  F.shiftMap T.mor₃ n₀ n₁ (by rw [add_comm 1, h])

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