shiftFunctorAdd_inv_app_f — Mathlib

English

The inverse of the shift-add isomorphism evaluated at a complex K acts on the f-component by the same iso data, equivalently giving an Iso-of-K expression.

Русский

Обратный отображатель для изоморфизма совместного сдвига и сложения действует на f-компоненте так же, как и исходное изоморфное описание для K.

LaTeX

$$$$((\mathrm{shiftFunctorAdd}(CochainComplex, Cℤ) a b).inv.app K).f_n = (K.XIsoOfEq (by dsimp; rw [\])).hom.$$$$

Lean4

theorem shiftFunctorAdd_inv_app_f (K : CochainComplex C ℤ) (a b n : ℤ) :
    ((shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n =
      (K.XIsoOfEq (by dsimp; rw [add_comm a, add_assoc])).hom :=
  rfl

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