comp_δ — Mathlib

English

The connecting morphism δ in the homology sequence associated to a distinguished triangle is defined via a derived shift and maps between nth and (n+1) homology objects.

Русский

Соединяющий морфизм δ в гомологической последовательности, связанной с особенностной треугольной диаграммой, задаётся через сдвиг и отображения между гомологиями в n‑й и (n+1)-й степенях.

LaTeX

$$$\\delta(T;n_0,n_1,h) : (\\mathrm{homologyFunctor} \\ C\\ n_0).\\text{obj }T.obj_3 \\to (\\mathrm{homologyFunctor} \\ C\\ n_1).\\text{obj }T.obj_1$$$

Lean4

@[reassoc (attr := simp)]
theorem comp_δ : (homologyFunctor C n₀).map T.mor₂ ≫ δ T n₀ n₁ h = 0 :=
  (homologyFunctor C 0).comp_homologySequenceδ _ hT _ _ h

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