add_zero_inv_app — Mathlib

English

The inverse component of shift with add_zero equals the image under the shift of the inverse of the zero-shift morphism.

Русский

Обратный компонент сдвига при сложении с нулём равен изображению обратного нулевого сдвига под F.

LaTeX

$$$(h.add\\,n\\,0)^{-1}.app\\,X = h.zero.hom.app\\,((h.F\\,n).obj X) \\;\\;\\text{via map}$$$

Lean4

theorem add_zero_inv_app (h : ShiftMkCore C A) (n : A) (X : C) :
    (h.add n 0).inv.app X = h.zero.hom.app ((h.F n).obj X) ≫ eqToHom (by dsimp; rw [add_zero]) := by
  rw [← cancel_epi ((h.add n 0).hom.app X), Iso.hom_inv_id_app, h.add_zero_hom_app, Category.assoc,
    Iso.inv_hom_id_app_assoc, eqToHom_trans, eqToHom_refl]

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