comp_homologySequenceδ — Mathlib

English

A certain three-term short complex built from the shifted triangle is exact.

Русский

Указанный трёхструнный краткий комплекс, полученный из сдвинутого треугольника, точен.

LaTeX

$$$(\text{ShortComplex})\; \text{with } (F.shift n_0).map T.mor_1, (F.shift n_0).map T.mor_2, δ_{F,T,n_0,n_1,h}$ is exact$$

Lean4

@[reassoc]
theorem comp_homologySequenceδ : (F.shift n₀).map T.mor₂ ≫ F.homologySequenceδ T n₀ n₁ h = 0 :=
  by
  dsimp only [homologySequenceδ]
  rw [← F.shiftMap_comp', comp_distTriang_mor_zero₂₃ _ hT, shiftMap_zero]

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