mappingConeCompTriangleh_distinguished

English

There is a full, robust triangulated structure on the Homotopy category of cochain complexes, i.e., it carries a compatible class of distinguished triangles satisfying the axioms.

Русский

Гомотопическая категория комплексoв коchain обладает полной триангулированной структурой, включающей допустимый набор выделенных треугольников, удовлетворяющих аксиомам.

LaTeX

$$$\text{IsTriangulated} \big(\mathrm{HomotopyCategory}(V,c)\big)$$$

Lean4

theorem mappingConeCompTriangleh_distinguished :
    (mappingConeCompTriangleh f g) ∈ distTriang (HomotopyCategory C (ComplexShape.up ℤ)) :=
  by
  refine ⟨_, _, (mappingConeCompTriangle f g).mor₁, ⟨?_⟩⟩
  refine
    Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)) (by cat_disch)
      (by simp) ?_
  dsimp [mappingConeCompTriangleh]
  rw [CategoryTheory.Functor.map_id, comp_id, ← Functor.map_comp_assoc]
  congr 2
  exact (mappingConeCompHomotopyEquiv_comm₂ f g).symm

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