English
The natural transformation CommShift for OppositeShift.natIsoId is compatible with shifts, giving a CommShift structure on its hom component.
Русский
Естественное преобразование CommShift для OppositeShift.natIsoId совместимо с сдвигами, образуя CommShift для его гом-компоненты.
LaTeX
$$$ NatTrans.CommShift (OppositeShift.natIsoId C A).hom A $$$
Lean4
instance commShift_op (τ : F ⟶ G) [NatTrans.CommShift τ A] : NatTrans.CommShift (OppositeShift.natTrans A τ) A where
shift_comm
_ := by
ext
rw [← cancel_mono (((OppositeShift.functor A F).commShiftIso _).inv.app _), ←
cancel_epi (((OppositeShift.functor A G).commShiftIso _).inv.app _)]
dsimp
simp only [assoc, Iso.inv_hom_id_app_assoc, Iso.hom_inv_id_app, Functor.comp_obj, comp_id]
exact (op_inj_iff _ _).mpr (NatTrans.shift_app_comm τ _ (unop _))
