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).obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).obj F)) :

s 0 ≅ CategoryTheory.Functor.id D

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

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).obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).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.

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).obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).obj F)) (X : C) :

(CategoryTheory.HasShift.Induced.zero F s i hF).hom.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((i 0).hom.app X) (F.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).obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).obj F)) (X : C) :

(CategoryTheory.HasShift.Induced.zero F s i hF).inv.app (F.obj X) = CategoryTheory.CategoryStruct.comp (F.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).obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).obj F)) (a : A) (b : A) (X : C) :

(CategoryTheory.HasShift.Induced.add F s i hF a b).hom.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).inv.app ((CategoryTheory.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} [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).obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).obj F)) (a : A) (b : A) (X : C) :

(CategoryTheory.HasShift.Induced.add F s i hF a b).inv.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((s b).map ((i a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp (F.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).obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).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].

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).obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).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).obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).obj F)) (X : C) :

(CategoryTheory.shiftFunctorZero D A).hom.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((i 0).hom.app X) (F.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).obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).obj F)) (X : C) :

(CategoryTheory.shiftFunctorZero D A).inv.app (F.obj X) = CategoryTheory.CategoryStruct.comp (F.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).obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).obj F)) (a : A) (b : A) (X : C) :

(CategoryTheory.shiftFunctorAdd D a b).hom.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).inv.app ((CategoryTheory.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} [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).obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).obj F)) (a : A) (b : A) (X : C) :

(CategoryTheory.shiftFunctorAdd D a b).inv.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((s b).map ((i a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp (F.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).obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).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.

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).obj F)) ∧ CategoryTheory.Faithful ((CategoryTheory.whiskeringLeft C D D).obj F)) (a : A) :

CategoryTheory.Functor.commShiftIso F a = (i a).symm