comp_distTriang_mor_zero₂₃ — Mathlib

English

Isomorphisms between distinguished triangles induce isomorphisms between their attached short complexes.

Русский

Изоморфизмы между выделенными треугольниками индуцируют изоморфизмы между присоединёнными к ним короткими комплексами.

LaTeX

$$shortComplexOfDistTriangleIsoOfIso$$

Lean4

/-- Given any distinguished triangle
```
      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧
```
the composition `g ≫ h = 0`. -/
@[reassoc, stacks 0146]
theorem comp_distTriang_mor_zero₂₃ (T : Triangle C) (H : T ∈ distTriang C) : T.mor₂ ≫ T.mor₃ = 0 :=
  comp_distTriang_mor_zero₁₂ T.rotate (rot_of_distTriang T H)

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