Commit 2025-01-10 18:19 0479fde8

feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): CommShift structures on adjunctions are compatible with opposites and pullbacks (#20363) Suppose that we use categories C and D equiped with a shifts by an additive monoid A, functors F,F' : C ⥤ D, a functor G : D ⥤ C, a natural transformation τ : F ⟶ F' and an adjunction adj between F and G.

• For any map of additive monoids φ : B →+ A, we define type synonyms PullbackShift.functor F φ for F, PullbackShift.natTrans τ φ for τ, and PullbackShift.adjunction adj φ for adj. We then prove that a CommShift structure on F (resp. τ, resp. adj) induces a CommShift structure on PullbackShift.functor F φ (resp. PullbackShift.natTrans τ φ, resp. PullbackShift.adjunction adj φ ).
• Similarly, we define type synonyms OppositeShift.functor A F for F.op, OppositeShift.natTrans A τ for τ.op and OppositeShift.adjunction A adj for adj.op, and prove that a CommShift structure on F (resp. τ, resp. adj) induces a CommShift structure on OppositeShift.functor A F (resp. OppositeShift.natTrans A τ, resp. OppositeShift.adjunction A adj ) for the naive shifts on the opposite categories.
• The point of the second part is to reserve F.op etc to carry CommShift structures for the modified shift on the opposite categories used in the theory of (pre)triangulated categories. We illustrate this by simplifying the definition of the instance commShiftOpInt (a CommShift ℤ instance on F.op for the modified shifts) in the file Triangulated.Opposite.Functor.

• depends on: #20364