shiftFunctor_map_f' — Mathlib

English

For a morphism φ between cochain complexes, shifting commutes with φ componentwise: the f-component of the shifted map at p equals φ.f at p+n.

Русский

Для морфизма φ между когнечными комплексами сдвиг коммутирует с φ компонентно: f-компонента сдвинутого отображения в p равна f-компоненте φ в p+n.

LaTeX

$$$$((\mathrm{Shift}(C, n))\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\lex)\mathrm{map}\;\varphi)^{f}_{p}=\varphi^{f}_{p+n}.$$$$

Lean4

@[simp]
theorem shiftFunctor_map_f' {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n p : ℤ) :
    ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ).f p = φ.f (p + n) :=
  rfl

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