shiftFunctorAdd'_add_zero_hom_app

English

The hom component of shiftFunctorAdd' with a and 0 on the right equals the inverse of shiftFunctorZero applied to X shifted by a.

Русский

Гомоморфизм ShiftFunctorAdd' с аргументами a и 0 справа равен обратному shiftFunctorZero, применённому к X со сдвигом a.

LaTeX

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

Lean4

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

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