mapHomologicalComplexXIso_eq — Mathlib

English

An isomorphism in the homotopy category between the image of the mapping cone under H and the mapping cone of the mapped morphism, degreewise.

Русский

Изоморфизм в гомотопической категории между образом отображающего конуса под действием H и отображающим конусом отображенного морфа по степеням.

LaTeX

$$$\\forall n: \\mathbb{Z},\\ ((H.mapHomologicalComplex(ComplexShape.up\\,\\mathbb{Z})).obj(\\mathrm{mappingCone}\\,φ)).X_n \\cong (\\mathrm{mappingCone}((H.mapHomologicalComplex(ComplexShape.up\\,\\mathbb{Z}).map\\,φ)).X_n)$$$

Lean4

theorem mapHomologicalComplexXIso_eq (n m : ℤ) (hnm : n + 1 = m) :
    mapHomologicalComplexXIso φ H n = mapHomologicalComplexXIso' φ H n m hnm :=
  by
  subst hnm
  rfl

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