shiftFunctorAdd'_add_zero_inv_app

English

Let a ∈ A and X ∈ Ob(C). Then the inverse component (shiftFunctorAdd' C a 0 a (add_zero a)).inv.app X equals the hom component of shiftFunctorZero at (X⟦a⟧).

Русский

Пусть a ∈ A и X ∈ Ob(C). Тогда inv.app X компонента shiftFunctorAdd' равен hom.app (X⟦a⟧) компоненты shiftFunctorZero.

LaTeX

$$$ (\\mathrm{shiftFunctorAdd'} \\, C \\, a \\, 0 \\, a \\, (\\mathrm{add_zero} \\, a)).inv.\\mathrm{app} \\, X = (\\mathrm{shiftFunctorZero} \\, C \\, A).hom.\\mathrm{app} (X\\\\langle a \\\\rangle ) $$$

Lean4

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

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