shiftFunctorZero_eq — Mathlib

English

The shift-zero isomorphism equals the standard shift-zero constructed from the base data; i.e., the canonical zero-shift equals the base construction.

Русский

Нулевой сдвиг равен стандартной конструкции нулевого сдвига, полученной из базовых данных.

LaTeX

$$$$ \mathrm{shiftFunctorZero}(\mathrm{CochainComplex}(C,\mathbb{Z}), \mathbb{Z}) = \mathrm{shiftFunctorZero}'(C,0,rfl). $$$$

Lean4

theorem shiftFunctorZero_eq : CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ = shiftFunctorZero' C 0 rfl :=
  by
  ext
  rw [shiftFunctorZero_hom_app_f, shiftFunctorZero'_hom_app_f]

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