shiftFunctorAdd'_inv_app_f' — Mathlib

English

If a + b = ab, the inverse-app f-coordinate of the shifted-add' iso equals the IsoOfEq hom part, simplifying to a standard expression.

Русский

Если a + b = ab, f-компонента обратного приложения для shiftFunctorAdd' совпадает с заданной формой IsoOfEq.

LaTeX

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

Lean4

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

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