instIsTriangulatedIntUpMapHomotopyCategory

English

In the HomotopyCategory, any additive functor G yields a triangulated functor, i.e. it preserves distinguished triangles.

Русский

В гомотопийной категории любой аддитивный функтор G образует триангулированный функтор, сохраняющий выделенные треугольники.

LaTeX

$$$\\text{instance } (G : C \\to D) [G.Additive] : (G.mapHomotopyCategory (ComplexShape.up \\mathbb{Z})).IsTriangulated$$$

Lean4

instance (G : C ⥤ D) [G.Additive] : (G.mapHomotopyCategory (ComplexShape.up ℤ)).IsTriangulated where
  map_distinguished := by
    rintro T ⟨K, L, f, ⟨e⟩⟩
    exact
      ⟨_, _, _,
        ⟨(G.mapHomotopyCategory (ComplexShape.up ℤ)).mapTriangle.mapIso e ≪≫
            CochainComplex.mappingCone.mapTrianglehIso f G⟩⟩

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