shiftFunctorAdd'_hom_app_f' — Mathlib

English

The hom-component of the ShiftAdd' isomorphism equals the IsoOfEq hom part after shifting by a+b.

Русский

Гомоморфная часть изоморфизма ShiftAdd' равна соответствующей части IsoOfEq после сдвига на a+b.

LaTeX

$$$$((\mathrm{shiftFunctorAdd'}(CochainComplex, ℤ) a b ab h).hom.app K).f n = (K.XIsoOfEq (by dsimp; rw [← h, add_assoc, add_comm a])).hom.$$$$

Lean4

theorem shiftFunctorAdd'_hom_app_f' (K : CochainComplex C ℤ) (a b ab : ℤ) (h : a + b = ab) (n : ℤ) :
    ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).hom.app K).f n =
      (K.XIsoOfEq (by dsimp; rw [← h, add_assoc, add_comm a])).hom :=
  by
  subst h
  rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_hom_app_f]

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