isomorphic_distinguished — Mathlib

English

If T1 is a distinguished triangle in the homotopy category and T2 is isomorphic to T1, then T2 is also distinguished.

Русский

Если T1 — выделенный треугольник в гомотопийной категории, и T2 изоморфен T1, то T2 тоже является выделенным.

LaTeX

$$$\\text{If } T_1 \\simeq T_2, \\text{ and } T_1 \\text{ is distinguished then } T_2 \\text{ is distinguished}.$$$

Lean4

theorem isomorphic_distinguished (T₁ : Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
    (hT₁ : T₁ ∈ distinguishedTriangles C) (T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))) (e : T₂ ≅ T₁) :
    T₂ ∈ distinguishedTriangles C := by
  obtain ⟨X, Y, f, ⟨e'⟩⟩ := hT₁
  exact ⟨X, Y, f, ⟨e ≪≫ e'⟩⟩

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