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

• HasShift: A typeclass asserting the existence of a shift functor.
• shiftEquiv: When the indexing monoid is a group, then the functor indexed by n and -n forms a self-equivalence of C.
• shiftComm: When the indexing monoid is commutative, then shifts commute as well.

Implementation Notes

[HasShift C A] is implemented using MonoidalFunctor (Discrete A) (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) [CategoryTheory.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.

• shift : CategoryTheory.MonoidalFunctor (CategoryTheory.Discrete A) (CategoryTheory.Functor C C)

  a shift is a monoidal functor from A to C ⥤ C

structure CategoryTheory.ShiftMkCore (C : Type u) (A : Type u_1) [CategoryTheory.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).

• F : A → CategoryTheory.Functor C C

  the family of shift functors

• zero : self.F 0 ≅ CategoryTheory.Functor.id C

  the shift by 0 identifies to the identity functor

• add : (n m : A) → self.F (n + m) ≅ CategoryTheory.Functor.comp (self.F n) (self.F m)

  the composition of shift functors identifies to the shift by the sum

• assoc_hom_app : ∀ (m₁ m₂ m₃ : A) (X : C), CategoryTheory.CategoryStruct.comp ((self.add (m₁ + m₂) m₃).hom.app X) ((self.F m₃).toPrefunctor.map ((self.add m₁ m₂).hom.app X)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (self.F (m₁ + m₂ + m₃)).toPrefunctor.obj X = (self.F (m₁ + (m₂ + m₃))).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((self.add m₁ (m₂ + m₃)).hom.app X) ((self.add m₂ m₃).hom.app ((self.F m₁).toPrefunctor.obj X)))

  compatibility with the associativity

• zero_add_hom_app : ∀ (n : A) (X : C), (self.add 0 n).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (self.F (0 + n)).toPrefunctor.obj X = (self.F n).toPrefunctor.obj ((CategoryTheory.Functor.id C).toPrefunctor.obj X))) ((self.F n).toPrefunctor.map (self.zero.inv.app X))

  compatibility with the left addition with 0

• add_zero_hom_app : ∀ (n : A) (X : C), (self.add n 0).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (self.F (n + 0)).toPrefunctor.obj X = (CategoryTheory.Functor.id C).toPrefunctor.obj ((self.F n).toPrefunctor.obj X))) (self.zero.inv.app ((self.F n).toPrefunctor.obj X))

  compatibility with the right addition with 0

theorem CategoryTheory.ShiftMkCore.assoc_hom_app_assoc {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] (self : CategoryTheory.ShiftMkCore C A) (m₁ : A) (m₂ : A) (m₃ : A) (X : C) {Z : C} (h : (self.F m₃).toPrefunctor.obj ((self.F m₂).toPrefunctor.obj ((self.F m₁).toPrefunctor.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.add (m₁ + m₂) m₃).hom.app X) (CategoryTheory.CategoryStruct.comp ((self.F m₃).toPrefunctor.map ((self.add m₁ m₂).hom.app X)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (self.F (m₁ + m₂ + m₃)).toPrefunctor.obj X = (self.F (m₁ + (m₂ + m₃))).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((self.add m₁ (m₂ + m₃)).hom.app X) (CategoryTheory.CategoryStruct.comp ((self.add m₂ m₃).hom.app ((self.F m₁).toPrefunctor.obj X)) h))

theorem CategoryTheory.ShiftMkCore.assoc_inv_app_assoc {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) (m₁ : A) (m₂ : A) (m₃ : A) (X : C) {Z : C} (h : (h✝.F (m₁ + m₂ + m₃)).toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((h✝.F m₃).toPrefunctor.map ((h✝.add m₁ m₂).inv.app X)) (CategoryTheory.CategoryStruct.comp ((h✝.add (m₁ + m₂) m₃).inv.app X) h) = CategoryTheory.CategoryStruct.comp ((h✝.add m₂ m₃).inv.app ((h✝.F m₁).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((h✝.add m₁ (m₂ + m₃)).inv.app X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (h✝.F (m₁ + (m₂ + m₃))).toPrefunctor.obj X = (h✝.F (m₁ + m₂ + m₃)).toPrefunctor.obj X)) h))

theorem CategoryTheory.ShiftMkCore.assoc_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) (m₁ : A) (m₂ : A) (m₃ : A) (X : C) : CategoryTheory.CategoryStruct.comp ((h.F m₃).toPrefunctor.map ((h.add m₁ m₂).inv.app X)) ((h.add (m₁ + m₂) m₃).inv.app X) = CategoryTheory.CategoryStruct.comp ((h.add m₂ m₃).inv.app ((h.F m₁).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((h.add m₁ (m₂ + m₃)).inv.app X) (CategoryTheory.eqToHom (_ : (h.F (m₁ + (m₂ + m₃))).toPrefunctor.obj X = (h.F (m₁ + m₂ + m₃)).toPrefunctor.obj X)))

theorem CategoryTheory.ShiftMkCore.zero_add_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) (n : A) (X : C) : (h.add 0 n).inv.app X = CategoryTheory.CategoryStruct.comp ((h.F n).toPrefunctor.map (h.zero.hom.app X)) (CategoryTheory.eqToHom (_ : (h.F n).toPrefunctor.obj ((CategoryTheory.Functor.id C).toPrefunctor.obj X) = (h.F (0 + n)).toPrefunctor.obj X))

theorem CategoryTheory.ShiftMkCore.add_zero_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) (n : A) (X : C) : (h.add n 0).inv.app X = CategoryTheory.CategoryStruct.comp (h.zero.hom.app ((h.F n).toPrefunctor.obj X)) (CategoryTheory.eqToHom (_ : (CategoryTheory.Functor.id C).toPrefunctor.obj ((h.F n).toPrefunctor.obj X) = (h.F (n + 0)).toPrefunctor.obj X))

@[simp]

theorem CategoryTheory.hasShiftMk_shift_toLaxMonoidalFunctor_toFunctor (C : Type u) (A : Type u_1) [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) : CategoryTheory.HasShift.shift.toFunctor = CategoryTheory.Discrete.functor h.F

@[simp]

theorem CategoryTheory.hasShiftMk_shift_toLaxMonoidalFunctor_ε (C : Type u) (A : Type u_1) [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) : CategoryTheory.HasShift.shift.ε = h.zero.inv

@[simp]

theorem CategoryTheory.hasShiftMk_shift_toLaxMonoidalFunctor_μ (C : Type u) (A : Type u_1) [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) (m : CategoryTheory.Discrete A) (n : CategoryTheory.Discrete A) : CategoryTheory.HasShift.shift.toLaxMonoidalFunctor.μ m n = (h.add m.as n.as).inv

def CategoryTheory.hasShiftMk (C : Type u) (A : Type u_1) [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) : CategoryTheory.HasShift C A

Constructs a HasShift C A instance from ShiftMkCore.

Equations

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

def CategoryTheory.shiftMonoidalFunctor (C : Type u) (A : Type u_1) [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] : CategoryTheory.MonoidalFunctor (CategoryTheory.Discrete A) (CategoryTheory.Functor C C)

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

Equations

• CategoryTheory.shiftMonoidalFunctor C A = CategoryTheory.HasShift.shift

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

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

Equations

• CategoryTheory.shiftFunctor C i = (CategoryTheory.shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj { as := i }

def CategoryTheory.shiftFunctorAdd (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (i : A) (j : A) : CategoryTheory.shiftFunctor C (i + j) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C i) (CategoryTheory.shiftFunctor C j)

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

Equations

• CategoryTheory.shiftFunctorAdd C i j = (CategoryTheory.MonoidalFunctor.μIso (CategoryTheory.shiftMonoidalFunctor C A) { as := i } { as := j }).symm

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

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

Equations

• CategoryTheory.shiftFunctorAdd' C i j k h = CategoryTheory.eqToIso (_ : CategoryTheory.shiftFunctor C k = CategoryTheory.shiftFunctor C (i + j)) ≪≫ CategoryTheory.shiftFunctorAdd C i j

theorem CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (i : A) (j : A) : CategoryTheory.shiftFunctorAdd' C i j (i + j) (_ : i + j = i + j) = CategoryTheory.shiftFunctorAdd C i j

def CategoryTheory.shiftFunctorZero (C : Type u) (A : Type u_1) [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] : CategoryTheory.shiftFunctor C 0 ≅ CategoryTheory.Functor.id C

Shifting by zero is the identity functor.

Equations

• CategoryTheory.shiftFunctorZero C A = (CategoryTheory.MonoidalFunctor.εIso (CategoryTheory.shiftMonoidalFunctor C A)).symm

theorem CategoryTheory.ShiftMkCore.shiftFunctor_eq {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) (a : A) : CategoryTheory.shiftFunctor C a = h.F a

theorem CategoryTheory.ShiftMkCore.shiftFunctorZero_eq {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) : CategoryTheory.shiftFunctorZero C A = h.zero

theorem CategoryTheory.ShiftMkCore.shiftFunctorAdd_eq {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) (a : A) (b : A) : CategoryTheory.shiftFunctorAdd C a b = h.add a b

def CategoryTheory.«term_⟦_⟧» : Lean.TrailingParserDescr

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.

def CategoryTheory.«term_⟦_⟧'» : Lean.TrailingParserDescr

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'_zero_add (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) : CategoryTheory.shiftFunctorAdd' C 0 a a (_ : 0 + a = a) = (CategoryTheory.Functor.leftUnitor (CategoryTheory.shiftFunctor C a)).symm ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorZero C A).symm (CategoryTheory.shiftFunctor C a)

theorem CategoryTheory.shiftFunctorAdd'_add_zero (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) : CategoryTheory.shiftFunctorAdd' C a 0 a (_ : a + 0 = a) = (CategoryTheory.Functor.rightUnitor (CategoryTheory.shiftFunctor C a)).symm ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C a) (CategoryTheory.shiftFunctorZero C A).symm

theorem CategoryTheory.shiftFunctorAdd'_assoc (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (a₃ : A) (a₁₂ : A) (a₂₃ : A) (a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) : CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (_ : a₁₂ + a₃ = a₁₂₃) ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂) (CategoryTheory.shiftFunctor C a₃) ≪≫ CategoryTheory.Functor.associator (CategoryTheory.shiftFunctor C a₁) (CategoryTheory.shiftFunctor C a₂) (CategoryTheory.shiftFunctor C a₃) = CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (_ : a₁ + a₂₃ = a₁₂₃) ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C a₁) (CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃)

theorem CategoryTheory.shiftFunctorAdd_assoc (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (a₃ : A) : CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C a₁ a₂) (CategoryTheory.shiftFunctor C a₃) ≪≫ CategoryTheory.Functor.associator (CategoryTheory.shiftFunctor C a₁) (CategoryTheory.shiftFunctor C a₂) (CategoryTheory.shiftFunctor C a₃) = CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃) ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C a₁) (CategoryTheory.shiftFunctorAdd C a₂ a₃)

theorem CategoryTheory.shiftFunctorAdd'_zero_add_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) (X : C) : (CategoryTheory.shiftFunctorAdd' C 0 a a (_ : 0 + a = a)).hom.app X = (CategoryTheory.shiftFunctor C a).toPrefunctor.map ((CategoryTheory.shiftFunctorZero C A).inv.app X)

theorem CategoryTheory.shiftFunctorAdd_zero_add_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) (X : C) : (CategoryTheory.shiftFunctorAdd C 0 a).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (CategoryTheory.shiftFunctor C (0 + a)).toPrefunctor.obj X = (CategoryTheory.shiftFunctor C a).toPrefunctor.obj ((CategoryTheory.Functor.id C).toPrefunctor.obj X))) ((CategoryTheory.shiftFunctor C a).toPrefunctor.map ((CategoryTheory.shiftFunctorZero C A).inv.app X))

theorem CategoryTheory.shiftFunctorAdd'_zero_add_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) (X : C) : (CategoryTheory.shiftFunctorAdd' C 0 a a (_ : 0 + a = a)).inv.app X = (CategoryTheory.shiftFunctor C a).toPrefunctor.map ((CategoryTheory.shiftFunctorZero C A).hom.app X)

theorem CategoryTheory.shiftFunctorAdd_zero_add_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) (X : C) : (CategoryTheory.shiftFunctorAdd C 0 a).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).toPrefunctor.map ((CategoryTheory.shiftFunctorZero C A).hom.app X)) (CategoryTheory.eqToHom (_ : (CategoryTheory.shiftFunctor C a).toPrefunctor.obj ((CategoryTheory.Functor.id C).toPrefunctor.obj X) = (CategoryTheory.shiftFunctor C (0 + a)).toPrefunctor.obj X))

theorem CategoryTheory.shiftFunctorAdd'_add_zero_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) (X : C) : (CategoryTheory.shiftFunctorAdd' C a 0 a (_ : a + 0 = a)).hom.app X = (CategoryTheory.shiftFunctorZero C A).inv.app ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X)

theorem CategoryTheory.shiftFunctorAdd_add_zero_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) (X : C) : (CategoryTheory.shiftFunctorAdd C a 0).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (CategoryTheory.shiftFunctor C (a + 0)).toPrefunctor.obj X = (CategoryTheory.Functor.id C).toPrefunctor.obj ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X))) ((CategoryTheory.shiftFunctorZero C A).inv.app ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X))

theorem CategoryTheory.shiftFunctorAdd'_add_zero_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) (X : C) : (CategoryTheory.shiftFunctorAdd' C a 0 a (_ : a + 0 = a)).inv.app X = (CategoryTheory.shiftFunctorZero C A).hom.app ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X)

theorem CategoryTheory.shiftFunctorAdd_add_zero_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) (X : C) : (CategoryTheory.shiftFunctorAdd C a 0).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C A).hom.app ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X)) (CategoryTheory.eqToHom (_ : (CategoryTheory.Functor.id C).toPrefunctor.obj ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X) = (CategoryTheory.shiftFunctor C (a + 0)).toPrefunctor.obj X))

theorem CategoryTheory.shiftFunctorAdd'_assoc_hom_app_assoc {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (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 : (CategoryTheory.shiftFunctor C a₃).toPrefunctor.obj ((CategoryTheory.shiftFunctor C a₂).toPrefunctor.obj ((CategoryTheory.shiftFunctor C a₁).toPrefunctor.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (_ : a₁₂ + a₃ = a₁₂₃)).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).toPrefunctor.map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (_ : a₁ + a₂₃ = a₁₂₃)).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app ((CategoryTheory.shiftFunctor C a₁).toPrefunctor.obj X)) h)

theorem CategoryTheory.shiftFunctorAdd'_assoc_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (a₃ : A) (a₁₂ : A) (a₂₃ : A) (a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (_ : a₁₂ + a₃ = a₁₂₃)).hom.app X) ((CategoryTheory.shiftFunctor C a₃).toPrefunctor.map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (_ : a₁ + a₂₃ = a₁₂₃)).hom.app X) ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app ((CategoryTheory.shiftFunctor C a₁).toPrefunctor.obj X))

theorem CategoryTheory.shiftFunctorAdd'_assoc_inv_app_assoc {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (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 : (CategoryTheory.shiftFunctor C a₁₂₃).toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).toPrefunctor.map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (_ : a₁₂ + a₃ = a₁₂₃)).inv.app X) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((CategoryTheory.shiftFunctor C a₁).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (_ : a₁ + a₂₃ = a₁₂₃)).inv.app X) h)

theorem CategoryTheory.shiftFunctorAdd'_assoc_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (a₃ : A) (a₁₂ : A) (a₂₃ : A) (a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).toPrefunctor.map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X)) ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (_ : a₁₂ + a₃ = a₁₂₃)).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((CategoryTheory.shiftFunctor C a₁).toPrefunctor.obj X)) ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (_ : a₁ + a₂₃ = a₁₂₃)).inv.app X)

theorem CategoryTheory.shiftFunctorAdd_assoc_hom_app_assoc {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (a₃ : A) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C a₃).toPrefunctor.obj ((CategoryTheory.shiftFunctor C a₂).toPrefunctor.obj ((CategoryTheory.shiftFunctor C a₁).toPrefunctor.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).toPrefunctor.map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).hom.app X)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃)).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C a₂ a₃).hom.app ((CategoryTheory.shiftFunctor C a₁).toPrefunctor.obj X)) h)

theorem CategoryTheory.shiftFunctorAdd_assoc_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (a₃ : A) (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X) ((CategoryTheory.shiftFunctor C a₃).toPrefunctor.map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).hom.app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃)).hom.app X) ((CategoryTheory.shiftFunctorAdd C a₂ a₃).hom.app ((CategoryTheory.shiftFunctor C a₁).toPrefunctor.obj X))

theorem CategoryTheory.shiftFunctorAdd_assoc_inv_app_assoc {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (a₃ : A) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C (a₁ + a₂ + a₃)).toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).toPrefunctor.map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).inv.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃).inv.app X) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C a₂ a₃).inv.app ((CategoryTheory.shiftFunctor C a₁).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃)).inv.app X) h)

theorem CategoryTheory.shiftFunctorAdd_assoc_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (a₃ : A) (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).toPrefunctor.map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).inv.app X)) ((CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C a₂ a₃).inv.app ((CategoryTheory.shiftFunctor C a₁).toPrefunctor.obj X)) ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃)).inv.app X)

@[simp]

theorem CategoryTheory.HasShift.shift_obj_obj {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (n : A) (X : C) : (CategoryTheory.HasShift.shift.toPrefunctor.obj { as := n }).toPrefunctor.obj X = (CategoryTheory.shiftFunctor C n).toPrefunctor.obj X

@[inline, reducible]

abbrev CategoryTheory.shiftAdd {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (X : C) (i : A) (j : A) : (CategoryTheory.shiftFunctor C (i + j)).toPrefunctor.obj X ≅ (CategoryTheory.shiftFunctor C j).toPrefunctor.obj ((CategoryTheory.shiftFunctor C i).toPrefunctor.obj X)

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

Equations

• CategoryTheory.shiftAdd X i j = (CategoryTheory.shiftFunctorAdd C i j).app X

theorem CategoryTheory.shift_shift' {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (X : C) (Y : C) (f : X ⟶ Y) (i : A) (j : A) : (CategoryTheory.shiftFunctor C j).toPrefunctor.map ((CategoryTheory.shiftFunctor C i).toPrefunctor.map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftAdd X i j).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C (i + j)).toPrefunctor.map f) (CategoryTheory.shiftAdd Y i j).hom)

@[inline, reducible]

abbrev CategoryTheory.shiftZero {C : Type u} (A : Type u_1) [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (X : C) : (CategoryTheory.shiftFunctor C 0).toPrefunctor.obj X ≅ X

Shifting by zero is the identity functor.

Equations

• CategoryTheory.shiftZero A X = (CategoryTheory.shiftFunctorZero C A).app X

theorem CategoryTheory.shiftZero' {C : Type u} (A : Type u_1) [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (X : C) (Y : C) (f : X ⟶ Y) : (CategoryTheory.shiftFunctor C 0).toPrefunctor.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftZero A X).hom (CategoryTheory.CategoryStruct.comp f (CategoryTheory.shiftZero A Y).inv)

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

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

Equations

• CategoryTheory.shiftFunctorCompIsoId C i j h = (CategoryTheory.shiftFunctorAdd' C i j 0 h).symm ≪≫ CategoryTheory.shiftFunctorZero C A

@[simp]

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

@[simp]

theorem CategoryTheory.shiftEquiv'_unitIso (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (i : A) (j : A) (h : i + j = 0) : (CategoryTheory.shiftEquiv' C i j h).unitIso = (CategoryTheory.shiftFunctorCompIsoId C i j h).symm

@[simp]

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

@[simp]

theorem CategoryTheory.shiftEquiv'_counitIso (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (i : A) (j : A) (h : i + j = 0) : (CategoryTheory.shiftEquiv' C i j h).counitIso = CategoryTheory.shiftFunctorCompIsoId C j i (_ : j + i = 0)

def CategoryTheory.shiftEquiv' (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (i : A) (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.

@[inline, reducible]

abbrev CategoryTheory.shiftEquiv (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (n : A) : C ≌ C

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

Equations

• CategoryTheory.shiftEquiv C n = CategoryTheory.shiftEquiv' C n (-n) (_ : n + -n = 0)

instance CategoryTheory.instIsEquivalenceShiftFunctorToAddMonoidToSubNegMonoid (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (i : A) : CategoryTheory.IsEquivalence (CategoryTheory.shiftFunctor C i)

Shifting by i is an equivalence.

Equations

• CategoryTheory.instIsEquivalenceShiftFunctorToAddMonoidToSubNegMonoid C i = let_fun this := inferInstance; this

@[simp]

theorem CategoryTheory.shiftFunctor_inv (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (i : A) : CategoryTheory.Functor.inv (CategoryTheory.shiftFunctor C i) = CategoryTheory.shiftFunctor C (-i)

instance CategoryTheory.shiftFunctor_essSurj (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (i : A) : CategoryTheory.EssSurj (CategoryTheory.shiftFunctor C i)

Shifting by n is an essentially surjective functor.

Equations

• (_ : CategoryTheory.EssSurj (CategoryTheory.shiftFunctor C i)) = (_ : CategoryTheory.EssSurj (CategoryTheory.shiftFunctor C i))

@[inline, reducible]

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

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

Equations

• CategoryTheory.shiftShiftNeg X i = (CategoryTheory.shiftEquiv C i).unitIso.symm.app X

@[inline, reducible]

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

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

Equations

• CategoryTheory.shiftNegShift X i = (CategoryTheory.shiftEquiv C i).counitIso.app X

theorem CategoryTheory.shift_shift_neg' {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] {X : C} {Y : C} (f : X ⟶ Y) (i : A) : (CategoryTheory.shiftFunctor C (-i)).toPrefunctor.map ((CategoryTheory.shiftFunctor C i).toPrefunctor.map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C i (-i) (_ : i + -i = 0)).hom.app X) (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctorCompIsoId C i (-i) (_ : i + -i = 0)).inv.app Y))

theorem CategoryTheory.shift_neg_shift' {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] {X : C} {Y : C} (f : X ⟶ Y) (i : A) : (CategoryTheory.shiftFunctor C i).toPrefunctor.map ((CategoryTheory.shiftFunctor C (-i)).toPrefunctor.map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C (-i) i (_ : -i + i = 0)).hom.app X) (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctorCompIsoId C (-i) i (_ : -i + i = 0)).inv.app Y))

theorem CategoryTheory.shift_equiv_triangle {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (n : A) (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).toPrefunctor.map (CategoryTheory.shiftShiftNeg X n).inv) (CategoryTheory.shiftNegShift ((CategoryTheory.shiftFunctor C n).toPrefunctor.obj X) n).hom = CategoryTheory.CategoryStruct.id ((CategoryTheory.shiftFunctor C n).toPrefunctor.obj X)

theorem CategoryTheory.shift_shiftFunctorCompIsoId_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (n : A) (m : A) (h : n + m = 0) (X : C) : (CategoryTheory.shiftFunctor C n).toPrefunctor.map ((CategoryTheory.shiftFunctorCompIsoId C n m h).hom.app X) = (CategoryTheory.shiftFunctorCompIsoId C m n (_ : m + n = 0)).hom.app ((CategoryTheory.shiftFunctor C n).toPrefunctor.obj X)

theorem CategoryTheory.shift_shiftFunctorCompIsoId_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (n : A) (m : A) (h : n + m = 0) (X : C) : (CategoryTheory.shiftFunctor C n).toPrefunctor.map ((CategoryTheory.shiftFunctorCompIsoId C n m h).inv.app X) = (CategoryTheory.shiftFunctorCompIsoId C m n (_ : m + n = 0)).inv.app ((CategoryTheory.shiftFunctor C n).toPrefunctor.obj X)

theorem CategoryTheory.shift_shiftFunctorCompIsoId_add_neg_self_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (n : A) (X : C) : (CategoryTheory.shiftFunctor C n).toPrefunctor.map ((CategoryTheory.shiftFunctorCompIsoId C n (-n) (_ : n + -n = 0)).hom.app X) = (CategoryTheory.shiftFunctorCompIsoId C (-n) n (_ : -n + n = 0)).hom.app ((CategoryTheory.shiftFunctor C n).toPrefunctor.obj X)

theorem CategoryTheory.shift_shiftFunctorCompIsoId_add_neg_self_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (n : A) (X : C) : (CategoryTheory.shiftFunctor C n).toPrefunctor.map ((CategoryTheory.shiftFunctorCompIsoId C n (-n) (_ : n + -n = 0)).inv.app X) = (CategoryTheory.shiftFunctorCompIsoId C (-n) n (_ : -n + n = 0)).inv.app ((CategoryTheory.shiftFunctor C n).toPrefunctor.obj X)

theorem CategoryTheory.shift_shiftFunctorCompIsoId_neg_add_self_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (n : A) (X : C) : (CategoryTheory.shiftFunctor C (-n)).toPrefunctor.map ((CategoryTheory.shiftFunctorCompIsoId C (-n) n (_ : -n + n = 0)).hom.app X) = (CategoryTheory.shiftFunctorCompIsoId C n (-n) (_ : n + -n = 0)).hom.app ((CategoryTheory.shiftFunctor C (-n)).toPrefunctor.obj X)

theorem CategoryTheory.shift_shiftFunctorCompIsoId_neg_add_self_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (n : A) (X : C) : (CategoryTheory.shiftFunctor C (-n)).toPrefunctor.map ((CategoryTheory.shiftFunctorCompIsoId C (-n) n (_ : -n + n = 0)).inv.app X) = (CategoryTheory.shiftFunctorCompIsoId C n (-n) (_ : n + -n = 0)).inv.app ((CategoryTheory.shiftFunctor C (-n)).toPrefunctor.obj X)

theorem CategoryTheory.shift_zero_eq_zero {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (Y : C) (n : A) : (CategoryTheory.shiftFunctor C n).toPrefunctor.map 0 = 0

def CategoryTheory.shiftFunctorComm (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] (i : A) (j : A) : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C i) (CategoryTheory.shiftFunctor C j) ≅ CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C j) (CategoryTheory.shiftFunctor C i)

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

Equations

• CategoryTheory.shiftFunctorComm C i j = (CategoryTheory.shiftFunctorAdd C i j).symm ≪≫ CategoryTheory.shiftFunctorAdd' C j i (i + j) (_ : j + i = i + j)

theorem CategoryTheory.shiftFunctorComm_eq (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] (i : A) (j : A) (k : A) (h : i + j = k) : CategoryTheory.shiftFunctorComm C i j = (CategoryTheory.shiftFunctorAdd' C i j k h).symm ≪≫ CategoryTheory.shiftFunctorAdd' C j i k (_ : j + i = k)

@[simp]

theorem CategoryTheory.shiftFunctorComm_eq_refl (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] (i : A) : CategoryTheory.shiftFunctorComm C i i = CategoryTheory.Iso.refl (CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C i) (CategoryTheory.shiftFunctor C i))

theorem CategoryTheory.shiftFunctorComm_symm (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] (i : A) (j : A) : (CategoryTheory.shiftFunctorComm C i j).symm = CategoryTheory.shiftFunctorComm C j i

@[inline, reducible]

abbrev CategoryTheory.shiftComm {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] (X : C) (i : A) (j : A) : (CategoryTheory.shiftFunctor C j).toPrefunctor.obj ((CategoryTheory.shiftFunctor C i).toPrefunctor.obj X) ≅ (CategoryTheory.shiftFunctor C i).toPrefunctor.obj ((CategoryTheory.shiftFunctor C j).toPrefunctor.obj X)

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

Equations

• CategoryTheory.shiftComm X i j = (CategoryTheory.shiftFunctorComm C i j).app X

@[simp]

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

theorem CategoryTheory.shiftComm' {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] {X : C} {Y : C} (f : X ⟶ Y) (i : A) (j : A) : (CategoryTheory.shiftFunctor C j).toPrefunctor.map ((CategoryTheory.shiftFunctor C i).toPrefunctor.map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm X i j).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C i).toPrefunctor.map ((CategoryTheory.shiftFunctor C j).toPrefunctor.map f)) (CategoryTheory.shiftComm Y j i).hom)

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

theorem CategoryTheory.shiftComm_hom_comp_assoc {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] {X : C} {Y : C} (f : X ⟶ Y) (i : A) (j : A) {Z : C} (h : (CategoryTheory.shiftFunctor C i).toPrefunctor.obj ((CategoryTheory.shiftFunctor C j).toPrefunctor.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm X i j).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C i).toPrefunctor.map ((CategoryTheory.shiftFunctor C j).toPrefunctor.map f)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C j).toPrefunctor.map ((CategoryTheory.shiftFunctor C i).toPrefunctor.map f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm Y i j).hom h)

theorem CategoryTheory.shiftComm_hom_comp {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] {X : C} {Y : C} (f : X ⟶ Y) (i : A) (j : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm X i j).hom ((CategoryTheory.shiftFunctor C i).toPrefunctor.map ((CategoryTheory.shiftFunctor C j).toPrefunctor.map f)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C j).toPrefunctor.map ((CategoryTheory.shiftFunctor C i).toPrefunctor.map f)) (CategoryTheory.shiftComm Y i j).hom

theorem CategoryTheory.shiftFunctorZero_hom_app_shift {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] {X : C} (n : A) : (CategoryTheory.shiftFunctorZero C A).hom.app ((CategoryTheory.shiftFunctor C n).toPrefunctor.obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C n 0).hom.app X) ((CategoryTheory.shiftFunctor C n).toPrefunctor.map ((CategoryTheory.shiftFunctorZero C A).hom.app X))

theorem CategoryTheory.shiftFunctorZero_inv_app_shift {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] {X : C} (n : A) : (CategoryTheory.shiftFunctorZero C A).inv.app ((CategoryTheory.shiftFunctor C n).toPrefunctor.obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).toPrefunctor.map ((CategoryTheory.shiftFunctorZero C A).inv.app X)) ((CategoryTheory.shiftFunctorComm C n 0).inv.app X)

theorem CategoryTheory.shiftFunctorComm_zero_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] {X : C} (a : A) : (CategoryTheory.shiftFunctorComm C a 0).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C A).hom.app ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X)) ((CategoryTheory.shiftFunctor C a).toPrefunctor.map ((CategoryTheory.shiftFunctorZero C A).inv.app X))

theorem CategoryTheory.shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app_assoc {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] (m₁ : A) (m₂ : A) (m₃ : A) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C m₁).toPrefunctor.obj ((CategoryTheory.shiftFunctor C m₃).toPrefunctor.obj ((CategoryTheory.shiftFunctor C m₂).toPrefunctor.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C m₁).toPrefunctor.map ((CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app X)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app ((CategoryTheory.shiftFunctor C m₁).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C m₃).toPrefunctor.map ((CategoryTheory.shiftFunctorComm C m₁ m₂).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C m₁ m₃).hom.app ((CategoryTheory.shiftFunctor C m₂).toPrefunctor.obj X)) h))

theorem CategoryTheory.shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] (m₁ : A) (m₂ : A) (m₃ : A) (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X) ((CategoryTheory.shiftFunctor C m₁).toPrefunctor.map ((CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app ((CategoryTheory.shiftFunctor C m₁).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C m₃).toPrefunctor.map ((CategoryTheory.shiftFunctorComm C m₁ m₂).hom.app X)) ((CategoryTheory.shiftFunctorComm C m₁ m₃).hom.app ((CategoryTheory.shiftFunctor C m₂).toPrefunctor.obj X)))

def CategoryTheory.hasShiftOfFullyFaithful_zero {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] (s : A → CategoryTheory.Functor C C) (i : (i : A) → CategoryTheory.Functor.comp (s i) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D i)) : s 0 ≅ CategoryTheory.Functor.id C

auxiliary definition for hasShiftOfFullyFaithful

Equations

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

@[simp]

theorem CategoryTheory.map_hasShiftOfFullyFaithful_zero_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] (s : A → CategoryTheory.Functor C C) (i : (i : A) → CategoryTheory.Functor.comp (s i) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D i)) (X : C) : F.toPrefunctor.map ((CategoryTheory.hasShiftOfFullyFaithful_zero F s i).hom.app X) = CategoryTheory.CategoryStruct.comp ((i 0).hom.app X) ((CategoryTheory.shiftFunctorZero D A).hom.app (F.toPrefunctor.obj X))

@[simp]

theorem CategoryTheory.map_hasShiftOfFullyFaithful_zero_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] (s : A → CategoryTheory.Functor C C) (i : (i : A) → CategoryTheory.Functor.comp (s i) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D i)) (X : C) : F.toPrefunctor.map ((CategoryTheory.hasShiftOfFullyFaithful_zero F s i).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero D A).inv.app (F.toPrefunctor.obj X)) ((i 0).inv.app X)

def CategoryTheory.hasShiftOfFullyFaithful_add {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] (s : A → CategoryTheory.Functor C C) (i : (i : A) → CategoryTheory.Functor.comp (s i) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D i)) (a : A) (b : A) : s (a + b) ≅ CategoryTheory.Functor.comp (s a) (s b)

auxiliary definition for hasShiftOfFullyFaithful

Equations

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

@[simp]

theorem CategoryTheory.map_hasShiftOfFullyFaithful_add_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] (s : A → CategoryTheory.Functor C C) (i : (i : A) → CategoryTheory.Functor.comp (s i) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D i)) (a : A) (b : A) (X : C) : F.toPrefunctor.map ((CategoryTheory.hasShiftOfFullyFaithful_add F s i a b).hom.app X) = CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).hom.app (F.toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).toPrefunctor.map ((i a).inv.app X)) ((i b).inv.app ((s a).toPrefunctor.obj X))))

@[simp]

theorem CategoryTheory.map_hasShiftOfFullyFaithful_add_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] (s : A → CategoryTheory.Functor C C) (i : (i : A) → CategoryTheory.Functor.comp (s i) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D i)) (a : A) (b : A) (X : C) : F.toPrefunctor.map ((CategoryTheory.hasShiftOfFullyFaithful_add F s i a b).inv.app X) = CategoryTheory.CategoryStruct.comp ((i b).hom.app ((s a).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).toPrefunctor.map ((i a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).inv.app (F.toPrefunctor.obj X)) ((i (a + b)).inv.app X)))

def CategoryTheory.hasShiftOfFullyFaithful {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] (s : A → CategoryTheory.Functor C C) (i : (i : A) → CategoryTheory.Functor.comp (s i) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D i)) : CategoryTheory.HasShift C A

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.