mappingConeCompTriangle — Mathlib

English

The canonical triangle encodes the relation among cones in a composable chain.

Русский

Единственный треугольник кодирует отношение между конусами в последовательной цепочке.

LaTeX

$$$ mappingConeCompTriangle : Triangle(\\text{CochainComplex } C \\mathbb{Z}) $$$

Lean4

/-- Given two composable morphisms `f : X₁ ⟶ X₂` and `g : X₂ ⟶ X₃` in the category
of cochain complexes, this is the canonical triangle
`mappingCone f ⟶ mappingCone (f ≫ g) ⟶ mappingCone g ⟶ (mappingCone f)⟦1⟧`. -/
@[simps! mor₁ mor₂ mor₃ obj₁ obj₂ obj₃]
noncomputable def mappingConeCompTriangle : Triangle (CochainComplex C ℤ) :=
  Triangle.mk (map f (f ≫ g) (𝟙 X₁) g (by rw [id_comp])) (map (f ≫ g) g f (𝟙 X₃) (by rw [comp_id]))
    ((triangle g).mor₃ ≫ (inr f)⟦1⟧')

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