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