mapCochainComplexShiftIso — Mathlib

English

Equivalence of shift isomorphisms under mapHomologicalComplex; the commShiftIso equals the cochain shift iso.

Русский

Эквивалентность изоморфизмов сдвига при mapHomologicalComplex: commShiftIso совпадает с коchain-shift iso.

LaTeX

$$$$ (F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n = F.mapCochainComplexShiftIso n. $$$$

Lean4

/-- The commutation with the shift isomorphism for the functor on cochain complexes
induced by an additive functor between preadditive categories. -/
@[simps!]
def mapCochainComplexShiftIso (n : ℤ) :
    shiftFunctor _ n ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ) ≅
      F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ shiftFunctor _ n :=
  NatIso.ofComponents (fun K => HomologicalComplex.Hom.isoOfComponents (fun _ => Iso.refl _) (by simp))
    (fun _ => by ext; dsimp; rw [id_comp, comp_id])

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