oppositeShiftFunctorZero_hom_app — Mathlib

English

The hom component of opposite shift functor for addition is the opposite of the hom component of the shifted Add functor.

Русский

Гом компонент противоположного сдвигового функторa для сложения равен противоположному гом компоненту сдвигового функторa.

LaTeX

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

Lean4

theorem oppositeShiftFunctorZero_hom_app (X : OppositeShift C A) :
    (shiftFunctorZero (OppositeShift C A) A).hom.app X = ((shiftFunctorZero C A).inv.app X.unop).op :=
  by
  rw [← cancel_mono ((shiftFunctorZero (OppositeShift C A) A).inv.app X), Iso.hom_inv_id_app,
    oppositeShiftFunctorZero_inv_app, ← op_comp, Iso.hom_inv_id_app, op_id]
  rfl

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