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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) {A : Type u_5} [AddMonoid A] [HasShift C A] (s : A → Functor D D) (i : (a : A) → F.comp (s a) ≅ (shiftFunctor C a).comp F) [((whiskeringLeft C D D).obj F).Full] [((whiskeringLeft C D D).obj F).Faithful] :
s 0 ≅ 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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) {A : Type u_5} [AddMonoid A] [HasShift C A] (s : A → Functor D D) (i : (a : A) → F.comp (s a) ≅ (shiftFunctor C a).comp F) [((whiskeringLeft C D D).obj F).Full] [((whiskeringLeft C D D).obj F).Faithful] (a b : A) :
    s (a + b) ≅ (s a).comp (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} [Category.{u_4, u_5} C] [Category.{u_1, u_2} D] (F : Functor C D) {A : Type u_3} [AddMonoid A] [HasShift C A] (s : A → Functor D D) (i : (a : A) → F.comp (s a) ≅ (shiftFunctor C a).comp F) [((whiskeringLeft C D D).obj F).Full] [((whiskeringLeft C D D).obj F).Faithful] (X : C) :
      (zero F s i).hom.app (F.obj X) = CategoryStruct.comp ((i 0).hom.app X) (F.map ((shiftFunctorZero C A).hom.app X))
      source
      @[simp]
      theorem CategoryTheory.HasShift.Induced.zero_inv_app_obj {C : Type u_4} {D : Type u_2} [Category.{u_3, u_4} C] [Category.{u_1, u_2} D] (F : Functor C D) {A : Type u_5} [AddMonoid A] [HasShift C A] (s : A → Functor D D) (i : (a : A) → F.comp (s a) ≅ (shiftFunctor C a).comp F) [((whiskeringLeft C D D).obj F).Full] [((whiskeringLeft C D D).obj F).Faithful] (X : C) :
      (zero F s i).inv.app (F.obj X) = CategoryStruct.comp (F.map ((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} [Category.{u_4, u_5} C] [Category.{u_1, u_2} D] (F : Functor C D) {A : Type u_3} [AddMonoid A] [HasShift C A] (s : A → Functor D D) (i : (a : A) → F.comp (s a) ≅ (shiftFunctor C a).comp F) [((whiskeringLeft C D D).obj F).Full] [((whiskeringLeft C D D).obj F).Faithful] (a b : A) (X : C) :
      (add F s i a b).hom.app (F.obj X) = CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryStruct.comp (F.map ((shiftFunctorAdd C a b).hom.app X)) (CategoryStruct.comp ((i b).inv.app ((shiftFunctor C a).obj X)) ((s b).map ((i a).inv.app X))))
      source
      @[simp]
      theorem CategoryTheory.HasShift.Induced.add_inv_app_obj {C : Type u_4} {D : Type u_2} [Category.{u_3, u_4} C] [Category.{u_1, u_2} D] (F : Functor C D) {A : Type u_5} [AddMonoid A] [HasShift C A] (s : A → Functor D D) (i : (a : A) → F.comp (s a) ≅ (shiftFunctor C a).comp F) [((whiskeringLeft C D D).obj F).Full] [((whiskeringLeft C D D).obj F).Faithful] (a b : A) (X : C) :
      (add F s i a b).inv.app (F.obj X) = CategoryStruct.comp ((s b).map ((i a).hom.app X)) (CategoryStruct.comp ((i b).hom.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp (F.map ((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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) (A : Type u_5) [AddMonoid A] [HasShift C A] (s : A → Functor D D) (i : (a : A) → F.comp (s a) ≅ (shiftFunctor C a).comp F) [((whiskeringLeft C D D).obj F).Full] [((whiskeringLeft C D D).obj F).Faithful] :
      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
        theorem CategoryTheory.shiftFunctor_of_induced {C : Type u_4} {D : Type u_1} [Category.{u_5, u_4} C] [Category.{u_2, u_1} D] (F : Functor C D) {A : Type u_3} [AddMonoid A] [HasShift C A] (s : A → Functor D D) (i : (a : A) → F.comp (s a) ≅ (shiftFunctor C a).comp F) [((whiskeringLeft C D D).obj F).Full] [((whiskeringLeft C D D).obj F).Faithful] (a : A) :
        shiftFunctor D a = s a
        source
        @[simp]
        theorem CategoryTheory.shiftFunctorZero_hom_app_obj_of_induced {C : Type u_4} {D : Type u_2} [Category.{u_5, u_4} C] [Category.{u_1, u_2} D] (F : Functor C D) (A : Type u_3) [AddMonoid A] [HasShift C A] (s : A → Functor D D) (i : (a : A) → F.comp (s a) ≅ (shiftFunctor C a).comp F) [((whiskeringLeft C D D).obj F).Full] [((whiskeringLeft C D D).obj F).Faithful] (X : C) :
        (shiftFunctorZero D A).hom.app (F.obj X) = CategoryStruct.comp ((i 0).hom.app X) (F.map ((shiftFunctorZero C A).hom.app X))
        source
        @[simp]
        theorem CategoryTheory.shiftFunctorZero_inv_app_obj_of_induced {C : Type u_4} {D : Type u_2} [Category.{u_3, u_4} C] [Category.{u_1, u_2} D] (F : Functor C D) (A : Type u_5) [AddMonoid A] [HasShift C A] (s : A → Functor D D) (i : (a : A) → F.comp (s a) ≅ (shiftFunctor C a).comp F) [((whiskeringLeft C D D).obj F).Full] [((whiskeringLeft C D D).obj F).Faithful] (X : C) :
        (shiftFunctorZero D A).inv.app (F.obj X) = CategoryStruct.comp (F.map ((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} [Category.{u_5, u_4} C] [Category.{u_1, u_2} D] (F : Functor C D) {A : Type u_3} [AddMonoid A] [HasShift C A] (s : A → Functor D D) (i : (a : A) → F.comp (s a) ≅ (shiftFunctor C a).comp F) [((whiskeringLeft C D D).obj F).Full] [((whiskeringLeft C D D).obj F).Faithful] (a b : A) (X : C) :
        (shiftFunctorAdd D a b).hom.app (F.obj X) = CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryStruct.comp (F.map ((shiftFunctorAdd C a b).hom.app X)) (CategoryStruct.comp ((i b).inv.app ((shiftFunctor C a).obj X)) ((s b).map ((i a).inv.app X))))
        source
        @[simp]
        theorem CategoryTheory.shiftFunctorAdd_inv_app_obj_of_induced {C : Type u_4} {D : Type u_2} [Category.{u_5, u_4} C] [Category.{u_1, u_2} D] (F : Functor C D) {A : Type u_3} [AddMonoid A] [HasShift C A] (s : A → Functor D D) (i : (a : A) → F.comp (s a) ≅ (shiftFunctor C a).comp F) [((whiskeringLeft C D D).obj F).Full] [((whiskeringLeft C D D).obj F).Faithful] (a b : A) (X : C) :
        (shiftFunctorAdd D a b).inv.app (F.obj X) = CategoryStruct.comp ((s b).map ((i a).hom.app X)) (CategoryStruct.comp ((i b).hom.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp (F.map ((shiftFunctorAdd C a b).inv.app X)) ((i (a + b)).inv.app X)))
        source
        noncomputable def CategoryTheory.Functor.CommShift.ofInduced {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) (A : Type u_5) [AddMonoid A] [HasShift C A] (s : A → Functor D D) (i : (a : A) → F.comp (s a) ≅ (shiftFunctor C a).comp F) [((whiskeringLeft C D D).obj F).Full] [((whiskeringLeft C D D).obj F).Faithful] :
        F.CommShift 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} [Category.{u_4, u_1} C] [Category.{u_2, u_3} D] (F : Functor C D) (A : Type u_5) [AddMonoid A] [HasShift C A] (s : A → Functor D D) (i : (a : A) → F.comp (s a) ≅ (shiftFunctor C a).comp F) [((whiskeringLeft C D D).obj F).Full] [((whiskeringLeft C D D).obj F).Faithful] (a : A) :
          F.commShiftIso a = (i a).symm