shiftFunctor_obj_d' — Mathlib

English

The differential of the shifted complex at i, j equals n.negOnePow times the original differential.

Русский

Дифференциал сдвинутого комплекса в точках i, j равен n.negOnePow умноженному на исходный дифференциал.

LaTeX

$$$$\big(\mathrm{Shift}(C, n)\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\).d_{i j}= n^{-1} \cdot d_{i j}.$$$$

Lean4

@[simp]
theorem shiftFunctor_obj_d' (K : CochainComplex C ℤ) (n i j : ℤ) :
    ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = n.negOnePow • K.d _ _ :=
  rfl

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