Induced shift sequences

When G : C ⥤ A is a functor from a category equipped with a shift by a monoid M, we have defined in the file CategoryTheory.Shift.ShiftSequence a type class G.ShiftSequence M which provides functors G.shift a : C ⥤ A for all a : M, isomorphisms shiftFunctor C n ⋙ G.shift a ≅ G.shift a' when n + a = a', and isomorphisms G.isoShift a : shiftFunctor C a ⋙ G ≅ G.shift a for all a, all of which satisfy good coherence properties. The idea is that it allows to use functors G.shift a which may have better definitional properties than shiftFunctor C a ⋙ G. The typical example shall be [(homologyFunctor C (ComplexShape.up ℤ) 0).ShiftSequence ℤ] for any abelian category C (TODO).

Similarly as a shift on a category may induce a shift on a quotient or a localized category (see the file CategoryTheory.Shift.Induced), this file shows that under certain assumptions, there is an induced "shift sequence". The main application will be the construction of a shift sequence for the homology functor on the homotopy category of cochain complexes (TODO), and also on the derived category (TODO).

@[irreducible]

noncomputable def CategoryTheory.Functor.ShiftSequence.induced.isoZero {C : Type u_1} {D : Type u_2} {A : Type u_3} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] [Category.{u_7, u_3} A] {L : Functor C D} {F : Functor D A} {G : Functor C A} (e : L.comp F ≅ G) (M : Type u_4) [AddMonoid M] [HasShift C M] [G.ShiftSequence M] (F' : M → Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m) [((whiskeringLeft C D A).obj L).Full] [((whiskeringLeft C D A).obj L).Faithful] : F' 0 ≅ F

The isoZero field of the induced shift sequence.

Equations

• CategoryTheory.Functor.ShiftSequence.induced.isoZero e M F' e' = ((CategoryTheory.whiskeringLeft C D A).obj L).preimageIso (e' 0 ≪≫ G.isoShiftZero M ≪≫ e.symm)

theorem CategoryTheory.Functor.ShiftSequence.induced.isoZero_hom_app_obj {C : Type u_1} {D : Type u_2} {A : Type u_3} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} A] {L : Functor C D} {F : Functor D A} {G : Functor C A} (e : L.comp F ≅ G) (M : Type u_4) [AddMonoid M] [HasShift C M] [G.ShiftSequence M] (F' : M → Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m) [((whiskeringLeft C D A).obj L).Full] [((whiskeringLeft C D A).obj L).Faithful] (X : C) : (isoZero e M F' e').hom.app (L.obj X) = CategoryStruct.comp ((e' 0).hom.app X) (CategoryStruct.comp ((G.isoShiftZero M).hom.app X) (e.inv.app X))

@[irreducible]

noncomputable def CategoryTheory.Functor.ShiftSequence.induced.shiftIso {C : Type u_1} {D : Type u_2} {A : Type u_3} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] [Category.{u_7, u_3} A] (L : Functor C D) (G : Functor C A) (M : Type u_4) [AddMonoid M] [HasShift C M] [G.ShiftSequence M] (F' : M → Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m) [((whiskeringLeft C D A).obj L).Full] [((whiskeringLeft C D A).obj L).Faithful] [HasShift D M] [L.CommShift M] (n a a' : M) (ha' : n + a = a') : (shiftFunctor D n).comp (F' a) ≅ F' a'

The shiftIso field of the induced shift sequence.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Functor.ShiftSequence.induced.shiftIso_hom_app_obj {C : Type u_1} {D : Type u_2} {A : Type u_3} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} A] (L : Functor C D) (G : Functor C A) (M : Type u_4) [AddMonoid M] [HasShift C M] [G.ShiftSequence M] (F' : M → Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m) [((whiskeringLeft C D A).obj L).Full] [((whiskeringLeft C D A).obj L).Faithful] [HasShift D M] [L.CommShift M] (n a a' : M) (ha' : n + a = a') (X : C) : (shiftIso L G M F' e' n a a' ha').hom.app (L.obj X) = CategoryStruct.comp ((F' a).map ((L.commShiftIso n).inv.app X)) (CategoryStruct.comp ((e' a).hom.app ((shiftFunctor C n).obj X)) (CategoryStruct.comp ((G.shiftIso n a a' ha').hom.app X) ((e' a').inv.app X)))

noncomputable def CategoryTheory.Functor.ShiftSequence.induced {C : Type u_1} {D : Type u_2} {A : Type u_3} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] [Category.{u_7, u_3} A] {L : Functor C D} {F : Functor D A} {G : Functor C A} (e : L.comp F ≅ G) (M : Type u_4) [AddMonoid M] [HasShift C M] [G.ShiftSequence M] (F' : M → Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m) [((whiskeringLeft C D A).obj L).Full] [((whiskeringLeft C D A).obj L).Faithful] [HasShift D M] [L.CommShift M] : F.ShiftSequence M

Given an isomorphism of functors e : L ⋙ F ≅ G relating functors L : C ⥤ D, F : D ⥤ A and G : C ⥤ A, an additive monoid M, a family of functors F' : M → D ⥤ A equipped with isomorphisms e' : ∀ m, L ⋙ F' m ≅ G.shift m, this is the shift sequence induced on F induced by a shift sequence for the functor G, provided that the functor (whiskeringLeft C D A).obj L of precomposition by L is fully faithful.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.ShiftSequence.induced_isoShiftZero_hom_app_obj {C : Type u_1} {D : Type u_2} {A : Type u_3} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} A] {L : Functor C D} {F : Functor D A} {G : Functor C A} (e : L.comp F ≅ G) (M : Type u_4) [AddMonoid M] [HasShift C M] [G.ShiftSequence M] (F' : M → Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m) [((whiskeringLeft C D A).obj L).Full] [((whiskeringLeft C D A).obj L).Faithful] [HasShift D M] [L.CommShift M] (X : C) : (F.isoShiftZero M).hom.app (L.obj X) = CategoryStruct.comp ((e' 0).hom.app X) (CategoryStruct.comp ((G.isoShiftZero M).hom.app X) (e.inv.app X))

theorem CategoryTheory.Functor.ShiftSequence.induced_isoShiftZero_hom_app_obj_assoc {C : Type u_1} {D : Type u_2} {A : Type u_3} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} A] {L : Functor C D} {F : Functor D A} {G : Functor C A} (e : L.comp F ≅ G) (M : Type u_4) [AddMonoid M] [HasShift C M] [G.ShiftSequence M] (F' : M → Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m) [((whiskeringLeft C D A).obj L).Full] [((whiskeringLeft C D A).obj L).Faithful] [HasShift D M] [L.CommShift M] (X : C) {Z : A} (h : F.obj (L.obj X) ⟶ Z) : CategoryStruct.comp ((F.isoShiftZero M).hom.app (L.obj X)) h = CategoryStruct.comp ((e' 0).hom.app X) (CategoryStruct.comp ((G.isoShiftZero M).hom.app X) (CategoryStruct.comp (e.inv.app X) h))

@[simp]

theorem CategoryTheory.Functor.ShiftSequence.induced_shiftIso_hom_app_obj {C : Type u_1} {D : Type u_2} {A : Type u_3} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} A] {L : Functor C D} {F : Functor D A} {G : Functor C A} (e : L.comp F ≅ G) (M : Type u_4) [AddMonoid M] [HasShift C M] [G.ShiftSequence M] (F' : M → Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m) [((whiskeringLeft C D A).obj L).Full] [((whiskeringLeft C D A).obj L).Faithful] [HasShift D M] [L.CommShift M] (n a a' : M) (ha' : n + a = a') (X : C) : (F.shiftIso n a a' ha').hom.app (L.obj X) = CategoryStruct.comp ((F.shift a).map ((L.commShiftIso n).inv.app X)) (CategoryStruct.comp ((e' a).hom.app ((shiftFunctor C n).obj X)) (CategoryStruct.comp ((G.shiftIso n a a' ha').hom.app X) ((e' a').inv.app X)))

theorem CategoryTheory.Functor.ShiftSequence.induced_shiftIso_hom_app_obj_assoc {C : Type u_1} {D : Type u_2} {A : Type u_3} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} A] {L : Functor C D} {F : Functor D A} {G : Functor C A} (e : L.comp F ≅ G) (M : Type u_4) [AddMonoid M] [HasShift C M] [G.ShiftSequence M] (F' : M → Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m) [((whiskeringLeft C D A).obj L).Full] [((whiskeringLeft C D A).obj L).Faithful] [HasShift D M] [L.CommShift M] (n a a' : M) (ha' : n + a = a') (X : C) {Z : A} (h : (F.shift a').obj (L.obj X) ⟶ Z) : CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app (L.obj X)) h = CategoryStruct.comp ((F.shift a).map ((L.commShiftIso n).inv.app X)) (CategoryStruct.comp ((e' a).hom.app ((shiftFunctor C n).obj X)) (CategoryStruct.comp ((G.shiftIso n a a' ha').hom.app X) (CategoryStruct.comp ((e' a').inv.app X) h)))

theorem CategoryTheory.Functor.ShiftSequence.induced_shiftMap {C : Type u_1} {D : Type u_2} {A : Type u_3} [Category.{u_5, u_1} C] [Category.{u_7, u_2} D] [Category.{u_6, u_3} A] {L : Functor C D} {F : Functor D A} {G : Functor C A} (e : L.comp F ≅ G) (M : Type u_4) [AddMonoid M] [HasShift C M] [G.ShiftSequence M] (F' : M → Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m) [((whiskeringLeft C D A).obj L).Full] [((whiskeringLeft C D A).obj L).Faithful] [HasShift D M] [L.CommShift M] {n : M} {X Y : C} (f : X ⟶ (shiftFunctor C n).obj Y) (a a' : M) (h : n + a = a') : F.shiftMap (CategoryStruct.comp (L.map f) ((L.commShiftIso n).hom.app Y)) a a' h = CategoryStruct.comp ((e' a).hom.app X) (CategoryStruct.comp (G.shiftMap f a a' h) ((e' a').inv.app Y))

theorem CategoryTheory.Functor.ShiftSequence.induced_shiftMap_assoc {C : Type u_1} {D : Type u_2} {A : Type u_3} [Category.{u_5, u_1} C] [Category.{u_7, u_2} D] [Category.{u_6, u_3} A] {L : Functor C D} {F : Functor D A} {G : Functor C A} (e : L.comp F ≅ G) (M : Type u_4) [AddMonoid M] [HasShift C M] [G.ShiftSequence M] (F' : M → Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m) [((whiskeringLeft C D A).obj L).Full] [((whiskeringLeft C D A).obj L).Faithful] [HasShift D M] [L.CommShift M] {n : M} {X Y : C} (f : X ⟶ (shiftFunctor C n).obj Y) (a a' : M) (h : n + a = a') {Z : A} (h✝ : (F.shift a').obj (L.obj Y) ⟶ Z) : CategoryStruct.comp (F.shiftMap (CategoryStruct.comp (L.map f) ((L.commShiftIso n).hom.app Y)) a a' h) h✝ = CategoryStruct.comp ((e' a).hom.app X) (CategoryStruct.comp (G.shiftMap f a a' h) (CategoryStruct.comp ((e' a').inv.app Y) h✝))