Commit 2025-01-01 17:49 504007f6
View on Github →feat(CategoryTheory/Shift/Adjunction): commutation with shifts and adjunctions, part 2 (#20273)
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 G, this file constructs a CommShift structure on F. This is a sequel to PR #20033, which was doing the construction in the other direction.