instComp — Mathlib

English

IsTriangulated is invariant under isomorphism of functors: F1 ≅ F2 implies F1.IsTriangulated ⇔ F2.IsTriangulated.

Русский

Свойство триангулированности сохраняется при изоморфизме функторов.

LaTeX

$$$F_1 \\cong F_2 \\Rightarrow (F_1.IsTriangulated \\iff F_2.IsTriangulated)$$$

Lean4

instance [F.IsTriangulated] [G.IsTriangulated] : (F ⋙ G).IsTriangulated where
  map_distinguished T
    hT :=
    isomorphic_distinguished _ (G.map_distinguished _ (F.map_distinguished T hT)) _ ((mapTriangleCompIso F G).app T)

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