Documentation

Mathlib.CategoryTheory.Shift.ShiftSequence

Sequences of functors from a category equipped with a shift

Let F : C ⥤ A be a functor from a category C that is equipped with a shift by an additive monoid M. In this file, we define a typeclass F.ShiftSequence M which includes the data of a sequence of functors F.shift a : C ⥤ A for all a : A. For each a : A, we have an isomorphism F.isoShift a : shiftFunctor C a ⋙ F ≅ F.shift a which satisfies some coherence relations. This allows to state results (e.g. the long exact sequence of an homology functor (TODO)) using functors F.shift a rather than shiftFunctor C a ⋙ F. The reason for this design is that we can often choose functors F.shift a that have better definitional properties than shiftFunctor C a ⋙ F. For example, if C is the derived category (TODO) of an abelian category A and F is the homology functor in degree 0, then for any n : ℤ, we may choose F.shift n to be the homology functor in degree n.

class CategoryTheory.Functor.ShiftSequence {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) (M : Type u_3) [AddMonoid M] [CategoryTheory.HasShift C M] :
Type (max (max (max (max u_1 u_2) u_3) u_4) u_5)

A shift sequence for a functor F : C ⥤ A when C is equipped with a shift by a monoid M involves a sequence of functor sequence n : C ⥤ A for all n : M which behave like shiftFunctor C n ⋙ F.

Instances

    The tautological shift sequence on a functor.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem CategoryTheory.Functor.shiftIso_hom_naturality {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] {X : C} {Y : C} (n : M) (a : M) (a' : M) (ha' : n + a = a') (f : X Y) :
      @[simp]
      theorem CategoryTheory.Functor.shiftIso_inv_naturality {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] {X : C} {Y : C} (n : M) (a : M) (a' : M) (ha' : n + a = a') (f : X Y) :

      The canonical isomorphism F.shift 0 ≅ F.

      Equations
      Instances For

        The canonical isomorphism shiftFunctor C n ⋙ F ≅ F.shift n.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem CategoryTheory.Functor.shiftIso_add_hom_app {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) (m : M) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
          (CategoryTheory.Functor.shiftIso F (m + n) a a'' (_ : m + n + a = a'')).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F a).toPrefunctor.map ((CategoryTheory.shiftFunctorAdd C m n).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).toPrefunctor.obj X)) ((CategoryTheory.Functor.shiftIso F m a' a'' ha'').hom.app X))
          theorem CategoryTheory.Functor.shiftIso_add_inv_app {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) (m : M) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
          (CategoryTheory.Functor.shiftIso F (m + n) a a'' (_ : m + n + a = a'')).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F m a' a'' ha'').inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').inv.app ((CategoryTheory.shiftFunctor C m).toPrefunctor.obj X)) ((CategoryTheory.Functor.shift F a).toPrefunctor.map ((CategoryTheory.shiftFunctorAdd C m n).inv.app X)))
          theorem CategoryTheory.Functor.shiftIso_add'_hom_app {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) (m : M) (mn : M) (hnm : m + n = mn) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
          (CategoryTheory.Functor.shiftIso F mn a a'' (_ : mn + a = a'')).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F a).toPrefunctor.map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).toPrefunctor.obj X)) ((CategoryTheory.Functor.shiftIso F m a' a'' ha'').hom.app X))
          theorem CategoryTheory.Functor.shiftIso_add'_inv_app {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) (m : M) (mn : M) (hnm : m + n = mn) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
          (CategoryTheory.Functor.shiftIso F mn a a'' (_ : mn + a = a'')).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F m a' a'' ha'').inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').inv.app ((CategoryTheory.shiftFunctor C m).toPrefunctor.obj X)) ((CategoryTheory.Functor.shift F a).toPrefunctor.map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).inv.app X)))
          theorem CategoryTheory.Functor.shiftIso_hom_app_comp_assoc {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) (m : M) (mn : M) (hnm : m + n = mn) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) {Z : A} (h : (CategoryTheory.Functor.shift F a'').toPrefunctor.obj X Z) :
          theorem CategoryTheory.Functor.shiftIso_hom_app_comp {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.Functor.ShiftSequence F M] (n : M) (m : M) (mn : M) (hnm : m + n = mn) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
          CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso F n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).toPrefunctor.obj X)) ((CategoryTheory.Functor.shiftIso F m a' a'' ha'').hom.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shift F a).toPrefunctor.map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).inv.app X)) ((CategoryTheory.Functor.shiftIso F mn a a'' (_ : mn + a = a'')).hom.app X)