mappingCone_triangleh_distinguished

English

There is an isomorphism on the level of distinguished triangles after applying the additive functor G to a morphism φ: K → L.

Русский

После применения аддитивного функторы G к морфизму φ: K→L сохраняется изоморфизм на уровне выделенных треугольников.

LaTeX

$$$ (\\mathrm{mapTrianglehIso} \\phi G) \\;:\\; (G.mapHomotopyCategory (up \\mathbb{Z})).mapTriangle.obj (triangle \\phi) \\cong \\text{triangle}( (G.mapHomologicalComplex (up \\mathbb{Z}).map \\phi)) $$$

Lean4

theorem mappingCone_triangleh_distinguished {X Y : CochainComplex C ℤ} (f : X ⟶ Y) :
    CochainComplex.mappingCone.triangleh f ∈ distTriang (HomotopyCategory _ _) :=
  ⟨_, _, f, ⟨Iso.refl _⟩⟩

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