oppositeShiftFunctorAdd'_hom_app — Mathlib

English

The hom component of shiftFunctorAdd' on the opposite shift corresponds to the hom of the forward shift Add'

Русский

Гом компонент shiftFunctorAdd' на противоположном сдвиге соответствует гому на прямом shift Add'.

LaTeX

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

Lean4

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

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