homologySequenceδ_comp — Mathlib

English

Another form of exactness involving δ and shifted morphisms yields an exact three-term sequence.

Русский

Еще одна форма точности, включающая δ и сдвинутые морфизмы, образует точную трёхчленную последовательность.

LaTeX

$$$\text{Exact}_{δ,1,2,3}$$$

Lean4

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

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