shiftFunctorAdd'_zero_add_hom_app

English

The hom component of shiftAdd' with left zero is given by the inv of shiftFunctorZero applied to a and then mapped by F.

Русский

Гом-компонента ShiftAdd'_zero_add задаётся как образ инверсии shiftFunctorZero и далее отображается через F.

LaTeX

$$$(shiftFunctorAdd'_zero_add_hom_app\\,a,\\,X).hom.app = ((shiftFunctorZero\\,C\\,A)^{-1}.app X)⟨a⟩'$$$

Lean4

theorem shiftFunctorAdd'_zero_add_hom_app (a : A) (X : C) :
    (shiftFunctorAdd' C 0 a a (zero_add a)).hom.app X = ((shiftFunctorZero C A).inv.app X)⟦a⟧' := by
  simpa using NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd'_zero_add C a)) X

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