Documentation

Mathlib.CategoryTheory.Shift.Basic

Shift #

A Shift on a category C indexed by a monoid A is nothing more than a monoidal functor from A to C ⥤ C. A typical example to keep in mind might be the category of complexes ⋯ → C_{n-1} → C_n → C_{n+1} → ⋯. It has a shift indexed by , where we assign to each n : ℤ the functor C ⥤ C that re-indexes the terms, so the degree i term of Shift n C would be the degree i+n-th term of C.

Main definitions #

Implementation Notes #

[HasShift C A] is implemented using monoidal functors from Discrete A to C ⥤ C. However, the API of monoidal functors is used only internally: one should use the API of shifts functors which includes shiftFunctor C a : C ⥤ C for a : A, shiftFunctorZero C A : shiftFunctor C (0 : A) ≅ 𝟭 C and shiftFunctorAdd C i j : shiftFunctor C (i + j) ≅ shiftFunctor C i ⋙ shiftFunctor C j (and its variant shiftFunctorAdd'). These isomorphisms satisfy some coherence properties which are stated in lemmas like shiftFunctorAdd'_assoc, shiftFunctorAdd'_zero_add and shiftFunctorAdd'_add_zero.

class CategoryTheory.HasShift (C : Type u) (A : Type u_2) [Category.{v, u} C] [AddMonoid A] :
Type (max (max u u_2) v)

A category has a shift indexed by an additive monoid A if there is a monoidal functor from A to C ⥤ C.

Instances
    structure CategoryTheory.ShiftMkCore (C : Type u) (A : Type u_1) [Category.{v, u} C] [AddMonoid A] :
    Type (max (max u u_1) v)

    A helper structure to construct the shift functor (Discrete A) ⥤ (C ⥤ C).

    theorem CategoryTheory.ShiftMkCore.assoc_hom_app_assoc {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] (self : ShiftMkCore C A) (m₁ m₂ m₃ : A) (X : C) {Z : C} (h : (self.F m₃).obj ((self.F m₂).obj ((self.F m₁).obj X)) Z) :
    CategoryStruct.comp ((self.add (m₁ + m₂) m₃).hom.app X) (CategoryStruct.comp ((self.F m₃).map ((self.add m₁ m₂).hom.app X)) h) = CategoryStruct.comp (eqToHom ) (CategoryStruct.comp ((self.add m₁ (m₂ + m₃)).hom.app X) (CategoryStruct.comp ((self.add m₂ m₃).hom.app ((self.F m₁).obj X)) h))
    theorem CategoryTheory.ShiftMkCore.assoc_inv_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] (h : ShiftMkCore C A) (m₁ m₂ m₃ : A) (X : C) :
    CategoryStruct.comp ((h.F m₃).map ((h.add m₁ m₂).inv.app X)) ((h.add (m₁ + m₂) m₃).inv.app X) = CategoryStruct.comp ((h.add m₂ m₃).inv.app ((h.F m₁).obj X)) (CategoryStruct.comp ((h.add m₁ (m₂ + m₃)).inv.app X) (eqToHom ))
    theorem CategoryTheory.ShiftMkCore.assoc_inv_app_assoc {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] (h : ShiftMkCore C A) (m₁ m₂ m₃ : A) (X : C) {Z : C} (h✝ : (h.F (m₁ + m₂ + m₃)).obj X Z) :
    CategoryStruct.comp ((h.F m₃).map ((h.add m₁ m₂).inv.app X)) (CategoryStruct.comp ((h.add (m₁ + m₂) m₃).inv.app X) h✝) = CategoryStruct.comp ((h.add m₂ m₃).inv.app ((h.F m₁).obj X)) (CategoryStruct.comp ((h.add m₁ (m₂ + m₃)).inv.app X) (CategoryStruct.comp (eqToHom ) h✝))
    theorem CategoryTheory.ShiftMkCore.zero_add_inv_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] (h : ShiftMkCore C A) (n : A) (X : C) :
    (h.add 0 n).inv.app X = CategoryStruct.comp ((h.F n).map (h.zero.hom.app X)) (eqToHom )
    theorem CategoryTheory.ShiftMkCore.add_zero_inv_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] (h : ShiftMkCore C A) (n : A) (X : C) :
    (h.add n 0).inv.app X = CategoryStruct.comp (h.zero.hom.app ((h.F n).obj X)) (eqToHom )
    Equations
    • One or more equations did not get rendered due to their size.
    def CategoryTheory.hasShiftMk (C : Type u) (A : Type u_1) [Category.{v, u} C] [AddMonoid A] (h : ShiftMkCore C A) :

    Constructs a HasShift C A instance from ShiftMkCore.

    Equations

    The monoidal functor from A to C ⥤ C given a HasShift instance.

    Equations
    def CategoryTheory.shiftFunctor (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (i : A) :

    The shift autoequivalence, moving objects and morphisms 'up'.

    Equations
    def CategoryTheory.shiftFunctorAdd (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (i j : A) :

    Shifting by i + j is the same as shifting by i and then shifting by j.

    Equations
    def CategoryTheory.shiftFunctorAdd' (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (i j k : A) (h : i + j = k) :

    When k = i + j, shifting by k is the same as shifting by i and then shifting by j.

    Equations
    def CategoryTheory.shiftFunctorZero' (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a : A) (ha : a = 0) :

    Shifting by a such that a = 0 identifies to the identity functor.

    Equations

    shifting an object X by n is obtained by the notation X⟦n⟧

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

    shifting a morphism f by n is obtained by the notation f⟦n⟧'

    Equations
    • One or more equations did not get rendered due to their size.
    theorem CategoryTheory.shiftFunctorAdd'_assoc (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) :
    shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ≪≫ isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂) (shiftFunctor C a₃) ≪≫ (shiftFunctor C a₁).associator (shiftFunctor C a₂) (shiftFunctor C a₃) = shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ≪≫ isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃)
    theorem CategoryTheory.shiftFunctorAdd_assoc (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a₁ a₂ a₃ : A) :
    shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫ isoWhiskerRight (shiftFunctorAdd C a₁ a₂) (shiftFunctor C a₃) ≪≫ (shiftFunctor C a₁).associator (shiftFunctor C a₂) (shiftFunctor C a₃) = shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ≪≫ isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd C a₂ a₃)
    theorem CategoryTheory.shiftFunctorAdd'_zero_add_hom_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a : A) (X : C) :
    (shiftFunctorAdd' C 0 a a ).hom.app X = (shiftFunctor C a).map ((shiftFunctorZero C A).inv.app X)
    theorem CategoryTheory.shiftFunctorAdd'_zero_add_inv_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a : A) (X : C) :
    (shiftFunctorAdd' C 0 a a ).inv.app X = (shiftFunctor C a).map ((shiftFunctorZero C A).hom.app X)
    theorem CategoryTheory.shiftFunctorAdd'_add_zero_hom_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a : A) (X : C) :
    (shiftFunctorAdd' C a 0 a ).hom.app X = (shiftFunctorZero C A).inv.app ((shiftFunctor C a).obj X)
    theorem CategoryTheory.shiftFunctorAdd'_add_zero_inv_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a : A) (X : C) :
    (shiftFunctorAdd' C a 0 a ).inv.app X = (shiftFunctorZero C A).hom.app ((shiftFunctor C a).obj X)
    theorem CategoryTheory.shiftFunctorAdd'_assoc_hom_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) :
    CategoryStruct.comp ((shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ).hom.app X) ((shiftFunctor C a₃).map ((shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X)) = CategoryStruct.comp ((shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ).hom.app X) ((shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app ((shiftFunctor C a₁).obj X))
    theorem CategoryTheory.shiftFunctorAdd'_assoc_hom_app_assoc {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) {Z : C} (h : (shiftFunctor C a₃).obj ((shiftFunctor C a₂).obj ((shiftFunctor C a₁).obj X)) Z) :
    CategoryStruct.comp ((shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ).hom.app X) (CategoryStruct.comp ((shiftFunctor C a₃).map ((shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X)) h) = CategoryStruct.comp ((shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ).hom.app X) (CategoryStruct.comp ((shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app ((shiftFunctor C a₁).obj X)) h)
    theorem CategoryTheory.shiftFunctorAdd'_assoc_inv_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) :
    CategoryStruct.comp ((shiftFunctor C a₃).map ((shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X)) ((shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ).inv.app X) = CategoryStruct.comp ((shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((shiftFunctor C a₁).obj X)) ((shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ).inv.app X)
    theorem CategoryTheory.shiftFunctorAdd'_assoc_inv_app_assoc {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) {Z : C} (h : (shiftFunctor C a₁₂₃).obj X Z) :
    CategoryStruct.comp ((shiftFunctor C a₃).map ((shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X)) (CategoryStruct.comp ((shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ).inv.app X) h) = CategoryStruct.comp ((shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((shiftFunctor C a₁).obj X)) (CategoryStruct.comp ((shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ).inv.app X) h)
    theorem CategoryTheory.shiftFunctorAdd_assoc_hom_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a₁ a₂ a₃ : A) (X : C) :
    CategoryStruct.comp ((shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X) ((shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).hom.app X)) = CategoryStruct.comp ((shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ).hom.app X) ((shiftFunctorAdd C a₂ a₃).hom.app ((shiftFunctor C a₁).obj X))
    theorem CategoryTheory.shiftFunctorAdd_assoc_hom_app_assoc {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a₁ a₂ a₃ : A) (X : C) {Z : C} (h : (shiftFunctor C a₃).obj ((shiftFunctor C a₂).obj ((shiftFunctor C a₁).obj X)) Z) :
    CategoryStruct.comp ((shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X) (CategoryStruct.comp ((shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).hom.app X)) h) = CategoryStruct.comp ((shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ).hom.app X) (CategoryStruct.comp ((shiftFunctorAdd C a₂ a₃).hom.app ((shiftFunctor C a₁).obj X)) h)
    theorem CategoryTheory.shiftFunctorAdd_assoc_inv_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a₁ a₂ a₃ : A) (X : C) :
    CategoryStruct.comp ((shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).inv.app X)) ((shiftFunctorAdd C (a₁ + a₂) a₃).inv.app X) = CategoryStruct.comp ((shiftFunctorAdd C a₂ a₃).inv.app ((shiftFunctor C a₁).obj X)) ((shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ).inv.app X)
    theorem CategoryTheory.shiftFunctorAdd_assoc_inv_app_assoc {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a₁ a₂ a₃ : A) (X : C) {Z : C} (h : (shiftFunctor C (a₁ + a₂ + a₃)).obj X Z) :
    CategoryStruct.comp ((shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).inv.app X)) (CategoryStruct.comp ((shiftFunctorAdd C (a₁ + a₂) a₃).inv.app X) h) = CategoryStruct.comp ((shiftFunctorAdd C a₂ a₃).inv.app ((shiftFunctor C a₁).obj X)) (CategoryStruct.comp ((shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ).inv.app X) h)
    @[reducible, inline]
    abbrev CategoryTheory.shiftAdd {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (X : C) (i j : A) :
    (shiftFunctor C (i + j)).obj X (shiftFunctor C j).obj ((shiftFunctor C i).obj X)

    Shifting by i + j is the same as shifting by i and then shifting by j.

    Equations
    theorem CategoryTheory.shift_shift' {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (X Y : C) (f : X Y) (i j : A) :
    @[reducible, inline]
    abbrev CategoryTheory.shiftZero {C : Type u} (A : Type u_1) [Category.{v, u} C] [AddMonoid A] [HasShift C A] (X : C) :
    (shiftFunctor C 0).obj X X

    Shifting by zero is the identity functor.

    Equations
    def CategoryTheory.shiftFunctorCompIsoId (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (i j : A) (h : i + j = 0) :

    When i + j = 0, shifting by i and by j gives the identity functor

    Equations
    def CategoryTheory.shiftEquiv' (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddGroup A] [HasShift C A] (i j : A) (h : i + j = 0) :
    C C

    Shifting by i and shifting by j forms an equivalence when i + j = 0.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem CategoryTheory.shiftEquiv'_inverse (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddGroup A] [HasShift C A] (i j : A) (h : i + j = 0) :
    @[simp]
    theorem CategoryTheory.shiftEquiv'_unitIso (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddGroup A] [HasShift C A] (i j : A) (h : i + j = 0) :
    @[simp]
    theorem CategoryTheory.shiftEquiv'_counitIso (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddGroup A] [HasShift C A] (i j : A) (h : i + j = 0) :
    @[simp]
    theorem CategoryTheory.shiftEquiv'_functor (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddGroup A] [HasShift C A] (i j : A) (h : i + j = 0) :
    @[reducible, inline]
    abbrev CategoryTheory.shiftEquiv (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddGroup A] [HasShift C A] (n : A) :
    C C

    Shifting by n and shifting by -n forms an equivalence.

    Equations

    Shifting by i is an equivalence.

    @[reducible, inline]
    abbrev CategoryTheory.shiftShiftNeg {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddGroup A] [HasShift C A] (X : C) (i : A) :
    (shiftFunctor C (-i)).obj ((shiftFunctor C i).obj X) X

    Shifting by i and then shifting by -i is the identity.

    Equations
    @[reducible, inline]
    abbrev CategoryTheory.shiftNegShift {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddGroup A] [HasShift C A] (X : C) (i : A) :
    (shiftFunctor C i).obj ((shiftFunctor C (-i)).obj X) X

    Shifting by -i and then shifting by i is the identity.

    Equations
    theorem CategoryTheory.shift_shift_neg' {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddGroup A] [HasShift C A] {X Y : C} (f : X Y) (i : A) :
    theorem CategoryTheory.shift_neg_shift' {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddGroup A] [HasShift C A] {X Y : C} (f : X Y) (i : A) :
    theorem CategoryTheory.shift_shiftFunctorCompIsoId_hom_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddGroup A] [HasShift C A] (n m : A) (h : n + m = 0) (X : C) :
    theorem CategoryTheory.shift_shiftFunctorCompIsoId_inv_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddGroup A] [HasShift C A] (n m : A) (h : n + m = 0) (X : C) :
    theorem CategoryTheory.shiftFunctorCompIsoId_add'_inv_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddGroup A] [HasShift C A] {X : C} (m n p m' n' p' : A) (hm : m' + m = 0) (hn : n' + n = 0) (hp : p' + p = 0) (h : m + n = p) :
    theorem CategoryTheory.shiftFunctorCompIsoId_add'_hom_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddGroup A] [HasShift C A] {X : C} (m n p m' n' p' : A) (hm : m' + m = 0) (hn : n' + n = 0) (hp : p' + p = 0) (h : m + n = p) :
    theorem CategoryTheory.shift_zero_eq_zero {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddGroup A] [HasShift C A] [Limits.HasZeroMorphisms C] (X Y : C) (n : A) :
    (shiftFunctor C n).map 0 = 0

    When shifts are indexed by an additive commutative monoid, then shifts commute.

    Equations
    theorem CategoryTheory.shiftFunctorComm_eq (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddCommMonoid A] [HasShift C A] (i j k : A) (h : i + j = k) :
    @[reducible, inline]
    abbrev CategoryTheory.shiftComm {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddCommMonoid A] [HasShift C A] (X : C) (i j : A) :

    When shifts are indexed by an additive commutative monoid, then shifts commute.

    Equations
    @[simp]
    theorem CategoryTheory.shiftComm_symm {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddCommMonoid A] [HasShift C A] (X : C) (i j : A) :
    (shiftComm X i j).symm = shiftComm X j i
    theorem CategoryTheory.shiftComm' {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddCommMonoid A] [HasShift C A] {X Y : C} (f : X Y) (i j : A) :

    When shifts are indexed by an additive commutative monoid, then shifts commute.

    theorem CategoryTheory.shiftComm_hom_comp {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddCommMonoid A] [HasShift C A] {X Y : C} (f : X Y) (i j : A) :
    theorem CategoryTheory.shiftComm_hom_comp_assoc {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddCommMonoid A] [HasShift C A] {X Y : C} (f : X Y) (i j : A) {Z : C} (h : (shiftFunctor C i).obj ((shiftFunctor C j).obj Y) Z) :
    theorem CategoryTheory.shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddCommMonoid A] [HasShift C A] (m₁ m₂ m₃ : A) (X : C) :
    CategoryStruct.comp ((shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X) ((shiftFunctor C m₁).map ((shiftFunctorAdd C m₂ m₃).hom.app X)) = CategoryStruct.comp ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X)) (CategoryStruct.comp ((shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).hom.app X)) ((shiftFunctorComm C m₁ m₃).hom.app ((shiftFunctor C m₂).obj X)))
    theorem CategoryTheory.shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app_assoc {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddCommMonoid A] [HasShift C A] (m₁ m₂ m₃ : A) (X : C) {Z : C} (h : (shiftFunctor C m₁).obj ((shiftFunctor C m₃).obj ((shiftFunctor C m₂).obj X)) Z) :
    CategoryStruct.comp ((shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X) (CategoryStruct.comp ((shiftFunctor C m₁).map ((shiftFunctorAdd C m₂ m₃).hom.app X)) h) = CategoryStruct.comp ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X)) (CategoryStruct.comp ((shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).hom.app X)) (CategoryStruct.comp ((shiftFunctorComm C m₁ m₃).hom.app ((shiftFunctor C m₂).obj X)) h))
    def CategoryTheory.Functor.FullyFaithful.hasShift.zero {C : Type u} {A : Type u_1} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] [AddMonoid A] [HasShift D A] {F : Functor C D} (hF : F.FullyFaithful) (s : AFunctor C C) (i : (i : A) → (s i).comp F F.comp (shiftFunctor D i)) :

    auxiliary definition for FullyFaithful.hasShift

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem CategoryTheory.Functor.FullyFaithful.hasShift.map_zero_hom_app {C : Type u} {A : Type u_1} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] [AddMonoid A] [HasShift D A] {F : Functor C D} (hF : F.FullyFaithful) (s : AFunctor C C) (i : (i : A) → (s i).comp F F.comp (shiftFunctor D i)) (X : C) :
    F.map ((zero hF s i).hom.app X) = CategoryStruct.comp ((i 0).hom.app X) ((shiftFunctorZero D A).hom.app (F.obj X))
    @[simp]
    theorem CategoryTheory.Functor.FullyFaithful.hasShift.map_zero_inv_app {C : Type u} {A : Type u_1} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] [AddMonoid A] [HasShift D A] {F : Functor C D} (hF : F.FullyFaithful) (s : AFunctor C C) (i : (i : A) → (s i).comp F F.comp (shiftFunctor D i)) (X : C) :
    F.map ((zero hF s i).inv.app X) = CategoryStruct.comp ((shiftFunctorZero D A).inv.app (F.obj X)) ((i 0).inv.app X)
    def CategoryTheory.Functor.FullyFaithful.hasShift.add {C : Type u} {A : Type u_1} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] [AddMonoid A] [HasShift D A] {F : Functor C D} (hF : F.FullyFaithful) (s : AFunctor C C) (i : (i : A) → (s i).comp F F.comp (shiftFunctor D i)) (a b : A) :
    s (a + b) (s a).comp (s b)

    auxiliary definition for FullyFaithful.hasShift

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem CategoryTheory.Functor.FullyFaithful.hasShift.map_add_hom_app {C : Type u} {A : Type u_1} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] [AddMonoid A] [HasShift D A] {F : Functor C D} (hF : F.FullyFaithful) (s : AFunctor C C) (i : (i : A) → (s i).comp F F.comp (shiftFunctor D i)) (a b : A) (X : C) :
    F.map ((add hF s i a b).hom.app X) = CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryStruct.comp ((shiftFunctorAdd D a b).hom.app (F.obj X)) (CategoryStruct.comp ((shiftFunctor D b).map ((i a).inv.app X)) ((i b).inv.app ((s a).obj X))))
    @[simp]
    theorem CategoryTheory.Functor.FullyFaithful.hasShift.map_add_inv_app {C : Type u} {A : Type u_1} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] [AddMonoid A] [HasShift D A] {F : Functor C D} (hF : F.FullyFaithful) (s : AFunctor C C) (i : (i : A) → (s i).comp F F.comp (shiftFunctor D i)) (a b : A) (X : C) :
    F.map ((add hF s i a b).inv.app X) = CategoryStruct.comp ((i b).hom.app ((s a).obj X)) (CategoryStruct.comp ((shiftFunctor D b).map ((i a).hom.app X)) (CategoryStruct.comp ((shiftFunctorAdd D a b).inv.app (F.obj X)) ((i (a + b)).inv.app X)))
    def CategoryTheory.Functor.FullyFaithful.hasShift {C : Type u} {A : Type u_1} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] [AddMonoid A] [HasShift D A] {F : Functor C D} (hF : F.FullyFaithful) (s : AFunctor C C) (i : (i : A) → (s i).comp F F.comp (shiftFunctor D i)) :

    Given a family of endomorphisms of C which are intertwined by a fully faithful F : C ⥤ D with shift functors on D, we can promote that family to shift functors on C.

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