zero_add_inv_app — Mathlib

English

The inverse component of shift with 0 addition is given by mapping the zero morphism through F and then applying a correction via eqToHom.

Русский

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

LaTeX

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

Lean4

theorem zero_add_inv_app (h : ShiftMkCore C A) (n : A) (X : C) :
    (h.add 0 n).inv.app X = (h.F n).map (h.zero.hom.app X) ≫ eqToHom (by dsimp; rw [zero_add]) := by
  rw [← cancel_epi ((h.add 0 n).hom.app X), Iso.hom_inv_id_app, h.zero_add_hom_app, Category.assoc, ←
    Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id, Category.id_comp, eqToHom_trans, eqToHom_refl]

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