oppositeShiftFunctorAdd'_inv_app — Mathlib

English

The inverse component of the opposite Shift Add' is given by the opposite of the hom component with unop.

Русский

Обратный компонент Opposite Shift Add' задаётся через обращение гом компонента с unop.

LaTeX

$$$ (shiftFunctorAdd' (OppositeShift C A) a b c h).inv.app X = ((shiftFunctorAdd' C a b c h).hom.app X.unop).op $$$

Lean4

theorem oppositeShiftFunctorAdd'_inv_app :
    (shiftFunctorAdd' (OppositeShift C A) a b c h).inv.app X = ((shiftFunctorAdd' C a b c h).hom.app X.unop).op :=
  by
  subst h
  simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, oppositeShiftFunctorAdd_inv_app]

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