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_5, u_1} C] [CategoryTheory.Category.{u_6, 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_5) u_6)

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.

• sequence : M → CategoryTheory.Functor C A

  a sequence of functors

• isoZero : CategoryTheory.Functor.ShiftSequence.sequence F 0 ≅ F

  sequence 0 identifies to the given functor

• shiftIso : (n a a' : M) → n + a = a' → ((CategoryTheory.shiftFunctor C n).comp (CategoryTheory.Functor.ShiftSequence.sequence F a) ≅ CategoryTheory.Functor.ShiftSequence.sequence F a')

  compatibility isomorphism with the shift

• shiftIso_zero : ∀ (a : M), CategoryTheory.Functor.ShiftSequence.shiftIso 0 a a ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ (CategoryTheory.Functor.ShiftSequence.sequence F a).leftUnitor
• shiftIso_add : ∀ (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a''), CategoryTheory.Functor.ShiftSequence.shiftIso (m + n) a a'' ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C m) (CategoryTheory.Functor.ShiftSequence.shiftIso n a a' ha') ≪≫ CategoryTheory.Functor.ShiftSequence.shiftIso m a' a'' ha''

theorem CategoryTheory.Functor.ShiftSequence.shiftIso_zero {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] {F : CategoryTheory.Functor C A} {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [self : F.ShiftSequence M] (a : M) : CategoryTheory.Functor.ShiftSequence.shiftIso 0 a a ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ (CategoryTheory.Functor.ShiftSequence.sequence F a).leftUnitor

theorem CategoryTheory.Functor.ShiftSequence.shiftIso_add {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] {F : CategoryTheory.Functor C A} {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [self : F.ShiftSequence M] (n : M) (m : M) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') : CategoryTheory.Functor.ShiftSequence.shiftIso (m + n) a a'' ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C m) (CategoryTheory.Functor.ShiftSequence.shiftIso n a a' ha') ≪≫ CategoryTheory.Functor.ShiftSequence.shiftIso m a' a'' ha''

noncomputable def CategoryTheory.Functor.ShiftSequence.tautological {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) (M : Type u_3) [AddMonoid M] [CategoryTheory.HasShift C M] : F.ShiftSequence M

The tautological shift sequence on a functor.

Equations

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

def CategoryTheory.Functor.shift {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] (n : M) : CategoryTheory.Functor C A

The shifted functors given by the shift sequence.

Equations

• F.shift n = CategoryTheory.Functor.ShiftSequence.sequence F n

def CategoryTheory.Functor.shiftIso {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] (n : M) (a : M) (a' : M) (ha' : n + a = a') : (CategoryTheory.shiftFunctor C n).comp (F.shift a) ≅ F.shift a'

Compatibility isomorphism shiftFunctor C n ⋙ F.shift a ≅ F.shift a' when n + a = a'.

Equations

• F.shiftIso n a a' ha' = CategoryTheory.Functor.ShiftSequence.shiftIso n a a' ha'

@[simp]

theorem CategoryTheory.Functor.shiftIso_hom_naturality_assoc {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] {X : C} {Y : C} (n : M) (a : M) (a' : M) (ha' : n + a = a') (f : X ⟶ Y) {Z : A} (h : (F.shift a').obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctor C n).map f)) (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app Y) h) = CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app X) (CategoryTheory.CategoryStruct.comp ((F.shift a').map f) h)

@[simp]

theorem CategoryTheory.Functor.shiftIso_hom_naturality {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] {X : C} {Y : C} (n : M) (a : M) (a' : M) (ha' : n + a = a') (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctor C n).map f)) ((F.shiftIso n a a' ha').hom.app Y) = CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app X) ((F.shift a').map f)

@[simp]

theorem CategoryTheory.Functor.shiftIso_inv_naturality_assoc {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] {X : C} {Y : C} (n : M) (a : M) (a' : M) (ha' : n + a = a') (f : X ⟶ Y) {Z : A} (h : (F.shift a).obj ((CategoryTheory.shiftFunctor C n).obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.shift a').map f) (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app Y) h) = CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app X) (CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctor C n).map f)) h)

@[simp]

theorem CategoryTheory.Functor.shiftIso_inv_naturality {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] {X : C} {Y : C} (n : M) (a : M) (a' : M) (ha' : n + a = a') (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((F.shift a').map f) ((F.shiftIso n a a' ha').inv.app Y) = CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app X) ((F.shift a).map ((CategoryTheory.shiftFunctor C n).map f))

def CategoryTheory.Functor.isoShiftZero {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) (M : Type u_3) [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] : F.shift 0 ≅ F

The canonical isomorphism F.shift 0 ≅ F.

Equations

• F.isoShiftZero M = CategoryTheory.Functor.ShiftSequence.isoZero

def CategoryTheory.Functor.isoShift {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] (n : M) : (CategoryTheory.shiftFunctor C n).comp F ≅ F.shift n

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

Equations

• F.isoShift n = CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C n) (F.isoShiftZero M).symm ≪≫ F.shiftIso n 0 n ⋯

theorem CategoryTheory.Functor.isoShift_hom_naturality_assoc {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] (n : M) {X : C} {Y : C} (f : X ⟶ Y) {Z : A} (h : (F.shift n).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C n).map f)) (CategoryTheory.CategoryStruct.comp ((F.isoShift n).hom.app Y) h) = CategoryTheory.CategoryStruct.comp ((F.isoShift n).hom.app X) (CategoryTheory.CategoryStruct.comp ((F.shift n).map f) h)

@[simp]

theorem CategoryTheory.Functor.isoShift_hom_naturality {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] (n : M) {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C n).map f)) ((F.isoShift n).hom.app Y) = CategoryTheory.CategoryStruct.comp ((F.isoShift n).hom.app X) ((F.shift n).map f)

theorem CategoryTheory.Functor.isoShift_inv_naturality_assoc {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] (n : M) {X : C} {Y : C} (f : X ⟶ Y) {Z : A} (h : F.obj ((CategoryTheory.shiftFunctor C n).obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.shift n).map f) (CategoryTheory.CategoryStruct.comp ((F.isoShift n).inv.app Y) h) = CategoryTheory.CategoryStruct.comp ((F.isoShift n).inv.app X) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C n).map f)) h)

theorem CategoryTheory.Functor.isoShift_inv_naturality {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] (n : M) {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((F.shift n).map f) ((F.isoShift n).inv.app Y) = CategoryTheory.CategoryStruct.comp ((F.isoShift n).inv.app X) (F.map ((CategoryTheory.shiftFunctor C n).map f))

theorem CategoryTheory.Functor.shiftIso_zero {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_6, 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] [F.ShiftSequence M] (a : M) : F.shiftIso 0 a a ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M) (F.shift a) ≪≫ (F.shift a).leftUnitor

@[simp]

theorem CategoryTheory.Functor.shiftIso_zero_hom_app {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_6, 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] [F.ShiftSequence M] (a : M) (X : C) : (F.shiftIso 0 a a ⋯).hom.app X = (F.shift a).map ((CategoryTheory.shiftFunctorZero C M).hom.app X)

@[simp]

theorem CategoryTheory.Functor.shiftIso_zero_inv_app {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_6, 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] [F.ShiftSequence M] (a : M) (X : C) : (F.shiftIso 0 a a ⋯).inv.app X = (F.shift a).map ((CategoryTheory.shiftFunctorZero C M).inv.app X)

theorem CategoryTheory.Functor.shiftIso_add {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_6, 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] [F.ShiftSequence M] (n : M) (m : M) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') : F.shiftIso (m + n) a a'' ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n) (F.shift a) ≪≫ (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n) (F.shift a) ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''

theorem CategoryTheory.Functor.shiftIso_add_hom_app {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_6, 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] [F.ShiftSequence M] (n : M) (m : M) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (F.shiftIso (m + n) a a'' ⋯).hom.app X = CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctorAdd C m n).hom.app X)) (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X)) ((F.shiftIso 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_6, 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] [F.ShiftSequence M] (n : M) (m : M) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (F.shiftIso (m + n) a a'' ⋯).inv.app X = CategoryTheory.CategoryStruct.comp ((F.shiftIso m a' a'' ha'').inv.app X) (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app ((CategoryTheory.shiftFunctor C m).obj X)) ((F.shift a).map ((CategoryTheory.shiftFunctorAdd C m n).inv.app X)))

theorem CategoryTheory.Functor.shiftIso_add' {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_6, 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] [F.ShiftSequence 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'') : F.shiftIso mn a a'' ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd' C m n mn hnm) (F.shift a) ≪≫ (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n) (F.shift a) ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''

theorem CategoryTheory.Functor.shiftIso_add'_hom_app {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_6, 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] [F.ShiftSequence 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) : (F.shiftIso mn a a'' ⋯).hom.app X = CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).hom.app X)) (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X)) ((F.shiftIso 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_6, 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] [F.ShiftSequence 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) : (F.shiftIso mn a a'' ⋯).inv.app X = CategoryTheory.CategoryStruct.comp ((F.shiftIso m a' a'' ha'').inv.app X) (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app ((CategoryTheory.shiftFunctor C m).obj X)) ((F.shift a).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_6, 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] [F.ShiftSequence 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 : (F.shift a'').obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X)) (CategoryTheory.CategoryStruct.comp ((F.shiftIso m a' a'' ha'').hom.app X) h) = CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).inv.app X)) (CategoryTheory.CategoryStruct.comp ((F.shiftIso mn a a'' ⋯).hom.app X) h)

theorem CategoryTheory.Functor.shiftIso_hom_app_comp {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_6, 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] [F.ShiftSequence 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 ((F.shiftIso n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X)) ((F.shiftIso m a' a'' ha'').hom.app X) = CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).inv.app X)) ((F.shiftIso mn a a'' ⋯).hom.app X)

def CategoryTheory.Functor.shiftMap {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] {X : C} {Y : C} {n : M} (f : X ⟶ (CategoryTheory.shiftFunctor C n).obj Y) (a : M) (a' : M) (ha' : n + a = a') : (F.shift a).obj X ⟶ (F.shift a').obj Y

The morphism (F.shift a).obj X ⟶ (F.shift a').obj Y induced by a morphism f : X ⟶ Y⟦n⟧ when n + a = a'.

Equations

• F.shiftMap f a a' ha' = CategoryTheory.CategoryStruct.comp ((F.shift a).map f) ((F.shiftIso n a a' ha').hom.app Y)

theorem CategoryTheory.Functor.shiftMap_comp_assoc {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] {X : C} {Y : C} {Z : C} {n : M} (f : X ⟶ (CategoryTheory.shiftFunctor C n).obj Y) (g : Y ⟶ Z✝) (a : M) (a' : M) (ha' : n + a = a') {Z : A} (h : (F.shift a').obj Z✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.shiftMap (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctor C n).map g)) a a' ha') h = CategoryTheory.CategoryStruct.comp (F.shiftMap f a a' ha') (CategoryTheory.CategoryStruct.comp ((F.shift a').map g) h)

theorem CategoryTheory.Functor.shiftMap_comp {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] {X : C} {Y : C} {Z : C} {n : M} (f : X ⟶ (CategoryTheory.shiftFunctor C n).obj Y) (g : Y ⟶ Z) (a : M) (a' : M) (ha' : n + a = a') : F.shiftMap (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctor C n).map g)) a a' ha' = CategoryTheory.CategoryStruct.comp (F.shiftMap f a a' ha') ((F.shift a').map g)

theorem CategoryTheory.Functor.shiftMap_comp'_assoc {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] {X : C} {Y : C} {Z : C} {n : M} (f : X ⟶ Y) (g : Y ⟶ (CategoryTheory.shiftFunctor C n).obj Z✝) (a : M) (a' : M) (ha' : n + a = a') {Z : A} (h : (F.shift a').obj Z✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.shiftMap (CategoryTheory.CategoryStruct.comp f g) a a' ha') h = CategoryTheory.CategoryStruct.comp ((F.shift a).map f) (CategoryTheory.CategoryStruct.comp (F.shiftMap g a a' ha') h)

theorem CategoryTheory.Functor.shiftMap_comp' {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] {X : C} {Y : C} {Z : C} {n : M} (f : X ⟶ Y) (g : Y ⟶ (CategoryTheory.shiftFunctor C n).obj Z) (a : M) (a' : M) (ha' : n + a = a') : F.shiftMap (CategoryTheory.CategoryStruct.comp f g) a a' ha' = CategoryTheory.CategoryStruct.comp ((F.shift a).map f) (F.shiftMap g a a' ha')

theorem CategoryTheory.Functor.shiftIso_hom_app_comp_shiftMap {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] {X : C} {Y : C} {m : M} (f : X ⟶ (CategoryTheory.shiftFunctor C m).obj Y) (n : M) (mn : M) (hnm : m + n = mn) (a : M) (a' : M) (a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') : CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app X) (F.shiftMap f a' a'' ha'') = CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctor C n).map f)) (CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).inv.app Y)) ((F.shiftIso mn a a'' ⋯).hom.app Y))

When f : X ⟶ Y⟦m⟧, m + n = mn, n + a = a' and ha'' : m + a' = a'', this lemma relates the two morphisms F.shiftMap f a' a'' ha'' and (F.shift a).map (f⟦n⟧'). Indeed, via canonical isomorphisms, they both identity to morphisms (F.shift a').obj X ⟶ (F.shift a'').obj Y.

theorem CategoryTheory.Functor.shiftIso_hom_app_comp_shiftMap_of_add_eq_zero {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {G : Type u_4} [AddGroup G] [CategoryTheory.HasShift C G] [F.ShiftSequence G] {X : C} {Y : C} {m : G} (f : X ⟶ (CategoryTheory.shiftFunctor C m).obj Y) (n : G) (hnm : n + m = 0) (a : G) (a' : G) (ha' : m + a = a') : CategoryTheory.CategoryStruct.comp ((F.shiftIso n a' a ⋯).hom.app X) (F.shiftMap f a a' ha') = (F.shift a').map (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map f) ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app Y))

If f : X ⟶ Y⟦m⟧, n + m = 0 and ha' : m + a = a', this lemma relates the two morphisms F.shiftMap f a a' ha' and (F.shift a').map (f⟦n⟧'). Indeed, via canonical isomorphisms, they both identify to morphisms (F.shift a).obj X ⟶ (F.shift a').obj Y.

instance CategoryTheory.Functor.instPreservesZeroMorphismsShift {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms A] [F.PreservesZeroMorphisms] [∀ (n : M), (CategoryTheory.shiftFunctor C n).PreservesZeroMorphisms] (n : M) : (F.shift n).PreservesZeroMorphisms

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Functor.shiftMap_zero {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_6, 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] [F.ShiftSequence M] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms A] [F.PreservesZeroMorphisms] [∀ (n : M), (CategoryTheory.shiftFunctor C n).PreservesZeroMorphisms] (X : C) (Y : C) (n : M) (a : M) (a' : M) (ha' : n + a = a') : F.shiftMap 0 a a' ha' = 0

instance CategoryTheory.Functor.instAdditiveShift {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} A] (F : CategoryTheory.Functor C A) {M : Type u_3} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive A] [F.Additive] [∀ (n : M), (CategoryTheory.shiftFunctor C n).Additive] (n : M) : (F.shift n).Additive

Equations

• ⋯ = ⋯