shiftFunctorAdd_zero_add_inv_app — Mathlib

English

The inv component of shiftFunctorAdd with zero on the right corresponds to mapping through shiftFunctor and applying shiftFunctorZero's hom.

Русский

Обратный компонент ShiftFunctorAdd при правом нуле соответствует отображению через shiftFunctor и применению гомоморфизма shiftFunctorZero.

LaTeX

$$$(shiftFunctorAdd C 0 a a).inv.app X = (shiftFunctor C a).map ((shiftFunctorZero C A).hom.app X)$$$

Lean4

theorem shiftFunctorAdd_zero_add_inv_app (a : A) (X : C) :
    (shiftFunctorAdd C 0 a).inv.app X = ((shiftFunctorZero C A).hom.app X)⟦a⟧' ≫ eqToHom (by dsimp; rw [zero_add]) := by
  simp [← shiftFunctorAdd'_zero_add_inv_app, shiftFunctorAdd']

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