shift_distinguished_triangle — Mathlib

English

The shift by n of a distinguished triangle is again distinguished.

Русский

Сдвиг на n выделенного треугольника вновь является выделенным.

LaTeX

$$$ (\\text{Triangle.shiftFunctor} _ n).obj T \\in \\text{distinguishedTriangles}$$$

Lean4

theorem shift_distinguished_triangle (T : Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
    (hT : T ∈ distinguishedTriangles C) (n : ℤ) : (Triangle.shiftFunctor _ n).obj T ∈ distinguishedTriangles C :=
  by
  obtain ⟨K, L, φ, ⟨e⟩⟩ := hT
  exact ⟨_, _, _, ⟨Functor.mapIso _ e ≪≫ CochainComplex.mappingCone.shiftTrianglehIso φ n⟩⟩

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