Lean4
/-- Given a `CommShift` structure on `F`, this is the corresponding `CommShift` structure on
`OppositeShift.functor F` (for the naive shifts on the opposite categories).
-/
noncomputable instance commShiftOp [CommShift F A] : CommShift (OppositeShift.functor A F) A
where
iso a := (NatIso.op (F.commShiftIso a)).symm
zero := by
rw [commShiftIso_zero]
ext
simp only [op_obj, comp_obj, Iso.symm_hom, NatIso.op_inv, NatTrans.op_app, CommShift.isoZero_inv_app, op_comp,
CommShift.isoZero_hom_app]
erw [oppositeShiftFunctorZero_inv_app, oppositeShiftFunctorZero_hom_app]
rfl
add a
b := by
rw [commShiftIso_add]
ext
simp only [op_obj, comp_obj, Iso.symm_hom, NatIso.op_inv, NatTrans.op_app, CommShift.isoAdd_inv_app, op_comp,
Category.assoc, CommShift.isoAdd_hom_app]
erw [oppositeShiftFunctorAdd_inv_app, oppositeShiftFunctorAdd_hom_app]
rfl
