shiftFunctorCompIsoId_zero_zero_inv_app

English

The inverse component for zero shift recovers the inverse of shift by zero with a standard composition pattern.

Русский

Обратный компонент для нулевого сдвига восстанавливает обращение к сдвигу на ноль через стандартную композицию.

LaTeX

$$$ ((\\mathrm{shiftFunctorCompIsoId} \\ C 0 0 (add_zero 0)).inv.app X) = (\\mathrm{shiftFunctorZero} \\ C A).inv.app X \\gg ((\\mathrm{shiftFunctorZero} \\ C A).inv.app X)⟦0⟧' $$$

Lean4

theorem shiftFunctorCompIsoId_zero_zero_inv_app (X : C) :
    (shiftFunctorCompIsoId C 0 0 (add_zero 0)).inv.app X =
      (shiftFunctorZero C A).inv.app X ≫ ((shiftFunctorZero C A).inv.app X)⟦0⟧' :=
  by simp [shiftFunctorCompIsoId, shiftFunctorAdd'_zero_add_hom_app]

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