shiftFunctorZero_inv_app_f — Mathlib

English

The inverse of the zero-shift iso evaluated at K gives the same IsoOfEq hom component as the zero-shift expression.

Русский

Обратное применяемое к нулевому сдвигу изоморфизмом при K даёт тот же гомоморфизм IsoOfEq, что и нулевой сдвиг.

LaTeX

$$$$((\mathrm{shiftFunctorZero}(CochainComplex, ℤ) , ℤ).inv.app K).f n = (K.XIsoOfEq (by dsimp; rw [add_zero])).hom.$$$$

Lean4

theorem shiftFunctorZero_inv_app_f (K : CochainComplex C ℤ) (n : ℤ) :
    ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n =
      (K.XIsoOfEq (by dsimp; rw [add_zero])).hom :=
  rfl

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