comp_distTriang_mor_zero₁₂ — Mathlib

English

Attach to each distinguished triangle a natural short complex built from its first two morphisms, which is exact at the middle term when the triangle is distinguished.

Русский

К каждому выделенному треугольнику естественным образом привязан короткий комплекс, построенный из первых двух морфизмов, который в середине точен при условии выделенности треугольника.

LaTeX

$$shortComplexOfDistTriangle(T,hT)$$

Lean4

/-- Given any distinguished triangle
```
      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧
```
the composition `f ≫ g = 0`. -/
@[reassoc, stacks 0146]
theorem comp_distTriang_mor_zero₁₂ (T) (H : T ∈ distTriang C) : T.mor₁ ≫ T.mor₂ = 0 :=
  by
  obtain ⟨c, hc⟩ :=
    complete_distinguished_triangle_morphism _ _ (contractible_distinguished T.obj₁) H (𝟙 T.obj₁) T.mor₁ rfl
  simpa only [contractibleTriangle_mor₂, zero_comp] using hc.left.symm

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