shiftFunctorAdd_zero_add_hom_app — Mathlib

English

The hom component of shiftFunctorAdd with zero on the left equals the image under shiftFunctor of the inverse of shiftFunctorZero.

Русский

Гом-компонента shiftFunctorAdd с нулём слева равна образу под shiftFunctor от обратной shiftFunctorZero.

LaTeX

$$$(shiftFunctorAdd C 0 a).hom.app X = eqToHom (by dsimp; rw [zero_add]) \\;\\gg\\; (shiftFunctorZero C A)^{-1}.app X ⟨a⟩'$$$

Lean4

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

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