Shift induced from a category to another #

In this file, we introduce a sufficient condition on a functor F : C ⥤ D so that a shift on C by a monoid A induces a shift on D. More precisely, when the functor (D ⥤ D) ⥤ C ⥤ D given by the precomposition with F is fully faithful, and that all the shift functors on C can be lifted to functors D ⥤ D (i.e. we have functors s a : D ⥤ D for all a : A, and isomorphisms F ⋙ s a ≅ shiftFunctor C a ⋙ F), then these functors s a are the shift functors of a term of type HasShift D A.

As this condition on the functor F is satisfied for quotient and localization functors, the main construction HasShift.induced in this file shall be used for both quotient and localized shifts.

The add field of the ShiftMkCore structure for the induced shift.

Instances For

    When F : C ⥤ D is a functor satisfying suitable technical assumptions, this is the induced term of type HasShift D A deduced from [HasShift C A].

    Instances For

      When the target category of a functor F : C ⥤ D is equipped with the induced shift, this is the compatibility of F with the shifts on the categories C and D.

      Instances For