Documentation

Mathlib.CategoryTheory.Shift.Induced

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.

source
noncomputable def CategoryTheory.HasShift.Induced.zero {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D) (i : (a : A) → CategoryTheory.Functor.comp F (s a) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F) (hF : Nonempty (CategoryTheory.Full ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) :
s 0 ≅ CategoryTheory.Functor.id D

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def CategoryTheory.HasShift.Induced.add {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D) (i : (a : A) → CategoryTheory.Functor.comp F (s a) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F) (hF : Nonempty (CategoryTheory.Full ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) (a : A) (b : A) :
    s (a + b) ≅ CategoryTheory.Functor.comp (s a) (s b)

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.HasShift.Induced.zero_hom_app_obj {C : Type u_5} {D : Type u_2} [CategoryTheory.Category.{u_4, u_5} C] [CategoryTheory.Category.{u_1, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_3} [AddMonoid A] [CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D) (i : (a : A) → CategoryTheory.Functor.comp F (s a) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F) (hF : Nonempty (CategoryTheory.Full ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) (X : C) :
      (CategoryTheory.HasShift.Induced.zero F s i hF).hom.app (F.toPrefunctor.obj X) = CategoryTheory.CategoryStruct.comp ((i 0).hom.app X) (F.toPrefunctor.map ((CategoryTheory.shiftFunctorZero C A).hom.app X))
      source
      @[simp]
      theorem CategoryTheory.HasShift.Induced.zero_inv_app_obj {C : Type u_4} {D : Type u_2} [CategoryTheory.Category.{u_3, u_4} C] [CategoryTheory.Category.{u_1, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D) (i : (a : A) → CategoryTheory.Functor.comp F (s a) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F) (hF : Nonempty (CategoryTheory.Full ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) (X : C) :
      (CategoryTheory.HasShift.Induced.zero F s i hF).inv.app (F.toPrefunctor.obj X) = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map ((CategoryTheory.shiftFunctorZero C A).inv.app X)) ((i 0).inv.app X)
      source
      @[simp]
      theorem CategoryTheory.HasShift.Induced.add_hom_app_obj {C : Type u_5} {D : Type u_2} [CategoryTheory.Category.{u_4, u_5} C] [CategoryTheory.Category.{u_1, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_3} [AddMonoid A] [CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D) (i : (a : A) → CategoryTheory.Functor.comp F (s a) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F) (hF : Nonempty (CategoryTheory.Full ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) (a : A) (b : A) (X : C) :
      (CategoryTheory.HasShift.Induced.add F s i hF a b).hom.app (F.toPrefunctor.obj X) = CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).inv.app ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X)) ((s b).toPrefunctor.map ((i a).inv.app X))))
      source
      @[simp]
      theorem CategoryTheory.HasShift.Induced.add_inv_app_obj {C : Type u_4} {D : Type u_2} [CategoryTheory.Category.{u_3, u_4} C] [CategoryTheory.Category.{u_1, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D) (i : (a : A) → CategoryTheory.Functor.comp F (s a) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F) (hF : Nonempty (CategoryTheory.Full ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) (a : A) (b : A) (X : C) :
      (CategoryTheory.HasShift.Induced.add F s i hF a b).inv.app (F.toPrefunctor.obj X) = CategoryTheory.CategoryStruct.comp ((s b).toPrefunctor.map ((i a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).hom.app ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map ((CategoryTheory.shiftFunctorAdd C a b).inv.app X)) ((i (a + b)).inv.app X)))
      source
      noncomputable def CategoryTheory.HasShift.induced {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D) (i : (a : A) → CategoryTheory.Functor.comp F (s a) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F) (hF : Nonempty (CategoryTheory.Full ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) :
      CategoryTheory.HasShift D A

      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].

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.shiftFunctor_of_induced {C : Type u_4} {D : Type u_1} [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) {A : Type u_3} [AddMonoid A] [CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D) (i : (a : A) → CategoryTheory.Functor.comp F (s a) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F) (hF : Nonempty (CategoryTheory.Full ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) (a : A) :
        CategoryTheory.shiftFunctor D a = s a
        source
        @[simp]
        theorem CategoryTheory.shiftFunctorZero_hom_app_obj_of_induced {C : Type u_4} {D : Type u_2} [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Category.{u_1, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_3) [AddMonoid A] [CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D) (i : (a : A) → CategoryTheory.Functor.comp F (s a) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F) (hF : Nonempty (CategoryTheory.Full ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) (X : C) :
        (CategoryTheory.shiftFunctorZero D A).hom.app (F.toPrefunctor.obj X) = CategoryTheory.CategoryStruct.comp ((i 0).hom.app X) (F.toPrefunctor.map ((CategoryTheory.shiftFunctorZero C A).hom.app X))
        source
        @[simp]
        theorem CategoryTheory.shiftFunctorZero_inv_app_obj_of_induced {C : Type u_4} {D : Type u_2} [CategoryTheory.Category.{u_3, u_4} C] [CategoryTheory.Category.{u_1, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D) (i : (a : A) → CategoryTheory.Functor.comp F (s a) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F) (hF : Nonempty (CategoryTheory.Full ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) (X : C) :
        (CategoryTheory.shiftFunctorZero D A).inv.app (F.toPrefunctor.obj X) = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map ((CategoryTheory.shiftFunctorZero C A).inv.app X)) ((i 0).inv.app X)
        source
        @[simp]
        theorem CategoryTheory.shiftFunctorAdd_hom_app_obj_of_induced {C : Type u_4} {D : Type u_2} [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Category.{u_1, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_3} [AddMonoid A] [CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D) (i : (a : A) → CategoryTheory.Functor.comp F (s a) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F) (hF : Nonempty (CategoryTheory.Full ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) (a : A) (b : A) (X : C) :
        (CategoryTheory.shiftFunctorAdd D a b).hom.app (F.toPrefunctor.obj X) = CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).inv.app ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X)) ((s b).toPrefunctor.map ((i a).inv.app X))))
        source
        @[simp]
        theorem CategoryTheory.shiftFunctorAdd_inv_app_obj_of_induced {C : Type u_4} {D : Type u_2} [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Category.{u_1, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_3} [AddMonoid A] [CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D) (i : (a : A) → CategoryTheory.Functor.comp F (s a) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F) (hF : Nonempty (CategoryTheory.Full ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) (a : A) (b : A) (X : C) :
        (CategoryTheory.shiftFunctorAdd D a b).inv.app (F.toPrefunctor.obj X) = CategoryTheory.CategoryStruct.comp ((s b).toPrefunctor.map ((i a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).hom.app ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map ((CategoryTheory.shiftFunctorAdd C a b).inv.app X)) ((i (a + b)).inv.app X)))
        source
        def CategoryTheory.Functor.CommShift.ofInduced {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D) (i : (a : A) → CategoryTheory.Functor.comp F (s a) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F) (hF : Nonempty (CategoryTheory.Full ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) :
        CategoryTheory.Functor.CommShift F A

        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.

        Equations
        Instances For
          source
          theorem CategoryTheory.Functor.commShiftIso_eq_ofInduced {C : Type u_1} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_2, u_3} D] (F : CategoryTheory.Functor C D) (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D) (i : (a : A) → CategoryTheory.Functor.comp F (s a) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F) (hF : Nonempty (CategoryTheory.Full ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).toPrefunctor.obj F)) (a : A) :
          CategoryTheory.Functor.commShiftIso F a = (i a).symm