English
If an adjunction F ⊣ G is compatible with CommShift on F and G, then the opposite adjunction also carries a compatible CommShift structure.
Русский
Если пара F ⊣ G совместима с CommShift на F и G, то противоположная сопряжённость также имеет совместимую структуру CommShift.
LaTeX
$$$ (OppositeShift.adjunction A adj).CommShift A $$$
Lean4
/-- If an adjunction `F ⊣ G` is compatible with `CommShift` structures on `F` and `G`, then
the opposite adjunction `OppositeShift.adjunction adj` is compatible with the opposite
`CommShift` structures.
-/
instance commShift_op [F.CommShift A] [G.CommShift A] [adj.CommShift A] :
Adjunction.CommShift (OppositeShift.adjunction A adj) A
where
commShift_unit := by dsimp [OppositeShift.adjunction]; infer_instance
commShift_counit := by dsimp [OppositeShift.adjunction]; infer_instance
