isTriangulated_iff_of_iso — Mathlib

English

There is a canonical CommShift structure on mapTriangle for all n ∈ Z, compatible with shift and additive structure.

Русский

Существует каноническая структура CommShift на mapTriangle для всех n ∈ Z, совместимая со сдвигом и аддитивной структурой.

LaTeX

$$$\\forall n\\in\\mathbb{Z}, (\\text{shiftFunctor } C\\, n).Additive$ and $(\\text{shiftFunctor } D\\, n).Additive$$$

Lean4

theorem isTriangulated_iff_of_iso {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ]
    [NatTrans.CommShift e.hom ℤ] : F₁.IsTriangulated ↔ F₂.IsTriangulated :=
  by
  constructor
  · intro
    exact isTriangulated_of_iso e
  · intro
    have : NatTrans.CommShift e.symm.hom ℤ := inferInstanceAs (NatTrans.CommShift e.inv ℤ)
    exact isTriangulated_of_iso e.symm

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