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

noncomputable def CategoryTheory.HasShift.Induced.zero {C : Type u_1} {D : Type u_2} [] [] (F : ) {A : Type u_5} [] [] (s : A) (i : (a : A) → ) (hF : Nonempty (CategoryTheory.Full (().obj F)) CategoryTheory.Faithful (().obj F)) :

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

Instances For
noncomputable def CategoryTheory.HasShift.Induced.add {C : Type u_1} {D : Type u_2} [] [] (F : ) {A : Type u_5} [] [] (s : A) (i : (a : A) → ) (hF : Nonempty (CategoryTheory.Full (().obj F)) CategoryTheory.Faithful (().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
@[simp]
theorem CategoryTheory.HasShift.Induced.zero_hom_app_obj {C : Type u_5} {D : Type u_2} [] [] (F : ) {A : Type u_3} [] [] (s : A) (i : (a : A) → ) (hF : Nonempty (CategoryTheory.Full (().obj F)) CategoryTheory.Faithful (().obj F)) (X : C) :
().hom.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((i 0).hom.app X) (F.map (().hom.app X))
@[simp]
theorem CategoryTheory.HasShift.Induced.zero_inv_app_obj {C : Type u_4} {D : Type u_2} [] [] (F : ) {A : Type u_5} [] [] (s : A) (i : (a : A) → ) (hF : Nonempty (CategoryTheory.Full (().obj F)) CategoryTheory.Faithful (().obj F)) (X : C) :
().inv.app (F.obj X) = CategoryTheory.CategoryStruct.comp (F.map (().inv.app X)) ((i 0).inv.app X)
@[simp]
theorem CategoryTheory.HasShift.Induced.add_hom_app_obj {C : Type u_5} {D : Type u_2} [] [] (F : ) {A : Type u_3} [] [] (s : A) (i : (a : A) → ) (hF : Nonempty (CategoryTheory.Full (().obj F)) CategoryTheory.Faithful (().obj F)) (a : A) (b : A) (X : C) :
().hom.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryTheory.CategoryStruct.comp (F.map (().hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).inv.app (().obj X)) ((s b).map ((i a).inv.app X))))
@[simp]
theorem CategoryTheory.HasShift.Induced.add_inv_app_obj {C : Type u_4} {D : Type u_2} [] [] (F : ) {A : Type u_5} [] [] (s : A) (i : (a : A) → ) (hF : Nonempty (CategoryTheory.Full (().obj F)) CategoryTheory.Faithful (().obj F)) (a : A) (b : A) (X : C) :
().inv.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((s b).map ((i a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).hom.app (().obj X)) (CategoryTheory.CategoryStruct.comp (F.map (().inv.app X)) ((i (a + b)).inv.app X)))
noncomputable def CategoryTheory.HasShift.induced {C : Type u_1} {D : Type u_2} [] [] (F : ) (A : Type u_5) [] [] (s : A) (i : (a : A) → ) (hF : Nonempty (CategoryTheory.Full (().obj F)) CategoryTheory.Faithful (().obj F)) :

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
@[simp]
theorem CategoryTheory.shiftFunctor_of_induced {C : Type u_4} {D : Type u_1} [] [] (F : ) {A : Type u_3} [] [] (s : A) (i : (a : A) → ) (hF : Nonempty (CategoryTheory.Full (().obj F)) CategoryTheory.Faithful (().obj F)) (a : A) :
= s a
@[simp]
theorem CategoryTheory.shiftFunctorZero_hom_app_obj_of_induced {C : Type u_4} {D : Type u_2} [] [] (F : ) (A : Type u_3) [] [] (s : A) (i : (a : A) → ) (hF : Nonempty (CategoryTheory.Full (().obj F)) CategoryTheory.Faithful (().obj F)) (X : C) :
().hom.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((i 0).hom.app X) (F.map (().hom.app X))
@[simp]
theorem CategoryTheory.shiftFunctorZero_inv_app_obj_of_induced {C : Type u_4} {D : Type u_2} [] [] (F : ) (A : Type u_5) [] [] (s : A) (i : (a : A) → ) (hF : Nonempty (CategoryTheory.Full (().obj F)) CategoryTheory.Faithful (().obj F)) (X : C) :
().inv.app (F.obj X) = CategoryTheory.CategoryStruct.comp (F.map (().inv.app X)) ((i 0).inv.app X)
@[simp]
theorem CategoryTheory.shiftFunctorAdd_hom_app_obj_of_induced {C : Type u_4} {D : Type u_2} [] [] (F : ) {A : Type u_3} [] [] (s : A) (i : (a : A) → ) (hF : Nonempty (CategoryTheory.Full (().obj F)) CategoryTheory.Faithful (().obj F)) (a : A) (b : A) (X : C) :
().hom.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryTheory.CategoryStruct.comp (F.map (().hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).inv.app (().obj X)) ((s b).map ((i a).inv.app X))))
@[simp]
theorem CategoryTheory.shiftFunctorAdd_inv_app_obj_of_induced {C : Type u_4} {D : Type u_2} [] [] (F : ) {A : Type u_3} [] [] (s : A) (i : (a : A) → ) (hF : Nonempty (CategoryTheory.Full (().obj F)) CategoryTheory.Faithful (().obj F)) (a : A) (b : A) (X : C) :
().inv.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((s b).map ((i a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).hom.app (().obj X)) (CategoryTheory.CategoryStruct.comp (F.map (().inv.app X)) ((i (a + b)).inv.app X)))
def CategoryTheory.Functor.CommShift.ofInduced {C : Type u_1} {D : Type u_2} [] [] (F : ) (A : Type u_5) [] [] (s : A) (i : (a : A) → ) (hF : Nonempty (CategoryTheory.Full (().obj F)) CategoryTheory.Faithful (().obj F)) :

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
theorem CategoryTheory.Functor.commShiftIso_eq_ofInduced {C : Type u_1} {D : Type u_3} [] [] (F : ) (A : Type u_5) [] [] (s : A) (i : (a : A) → ) (hF : Nonempty (CategoryTheory.Full (().obj F)) CategoryTheory.Faithful (().obj F)) (a : A) :
= (i a).symm