Commit 2024-12-19 17:27 49ac6bf0

feat(CategoryTheory/Shift): commutation with shifts and adjunctions (#20033) Given categories C and D that have shifts by an additive group A, functors F : C ⥤ D and G : C ⥤ D, an adjunction F ⊣ G and a CommShift structure on F, construct a CommShift structure on G. As an easy application, if E : C ≌ D is an equivalence and E.functor has a CommShift structure, we get a CommShift structure on E.inverse. The CommShift structure on G must be compatible with the one on F in the following sense (cf. Adjunction.CommShift): for every a in A, the natural transformation adj.unit : 𝟭 C ⟶ G ⋙ F commutes with the isomorphism shiftFunctor C A ⋙ G ⋙ F ≅ G ⋙ F ⋙ shiftFunctor C A induces by F.commShiftIso a and G.commShiftIso a. We actually require a similar condition for adj.counit, but it follows from the one for adj.unit. In order to simplify the construction of the CommShift structure on G, we first introduce the compatibility condition on adj.unit for a fixed a in A and for isomorphisms e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a and e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a. We then prove that:

• If e₁ and e₂ satusfy this condition, then e₁ uniquely determines e₂ and vice versa.
• If a = 0, the isomorphisms Functor.CommShift.isoZero F and Functor.CommShift.isoZero G satisfy the condition.
• The condition is stable by addition on A, if we use Functor.CommShift.isoAdd to deduce commutation isomorphism for a + b from such isomorphism from a and b.
• Given commutation isomorphisms for F, our candidate commutation isomorphisms for G, constructed in Adjunction.RightAdjointCommShift.iso, satisfy the compatibility condition. Once we have established all this, the compatibility of the commutation isomorphism for F expressed in CommShift.zero and CommShift.add immediately implies the similar statements for the commutation isomorphisms for G. TODO: Construct a CommShift structure on F from a CommShift structure on G, using opposite categories.