shiftFunctorAdd'_zero_add_inv_app

English

The inv component of shiftAdd'_zero_add is given by the hom component of shiftFunctorZero composed with the shift by a.

Русский

Обратный компонент ShiftAdd'_zero_add задаётся как композиция гом-компоненты shiftFunctorZero и сдвига на a.

LaTeX

$$$(shiftFunctorAdd'_zero_add).inv.app X = ((shiftFunctorZero C A).hom.app X)⟦a⟧'$$$

Lean4

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

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