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) ≅ (self.F n).comp (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₃).map ((self.add m₁ m₂).hom.app X)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((self.add m₁ (m₂ + m₃)).hom.app X) ((self.add m₂ m₃).hom.app ((self.F m₁).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 n).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.zero.inv.app ((self.F n).obj X))

  compatibility with the right addition with 0

theorem CategoryTheory.ShiftMkCore.assoc_hom_app {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) : CategoryTheory.CategoryStruct.comp ((self.add (m₁ + m₂) m₃).hom.app X) ((self.F m₃).map ((self.add m₁ m₂).hom.app X)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((self.add m₁ (m₂ + m₃)).hom.app X) ((self.add m₂ m₃).hom.app ((self.F m₁).obj X)))

compatibility with the associativity

theorem CategoryTheory.ShiftMkCore.zero_add_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] (self : CategoryTheory.ShiftMkCore C A) (n : A) (X : C) : (self.add 0 n).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((self.F n).map (self.zero.inv.app X))

compatibility with the left addition with 0

theorem CategoryTheory.ShiftMkCore.add_zero_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] (self : CategoryTheory.ShiftMkCore C A) (n : A) (X : C) : (self.add n 0).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (self.zero.inv.app ((self.F n).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₃).obj ((self.F m₂).obj ((self.F m₁).obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.add (m₁ + m₂) m₃).hom.app X) (CategoryTheory.CategoryStruct.comp ((self.F m₃).map ((self.add m₁ m₂).hom.app X)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((self.add m₁ (m₂ + m₃)).hom.app X) (CategoryTheory.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} [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₃).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₁).obj X)) (CategoryTheory.CategoryStruct.comp ((h.add m₁ (m₂ + m₃)).inv.app X) (CategoryTheory.eqToHom ⋯))

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₃)).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((h✝.F m₃).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₁).obj X)) (CategoryTheory.CategoryStruct.comp ((h✝.add m₁ (m₂ + m₃)).inv.app X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h))

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).map (h.zero.hom.app X)) (CategoryTheory.eqToHom ⋯)

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).obj X)) (CategoryTheory.eqToHom ⋯)

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.

@[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.μ m n = (h.add m.as n.as).inv

@[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

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).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.shiftFunctor C i).comp (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.shiftMonoidalFunctor C A).μIso { 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.shiftFunctor C i).comp (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.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) ⋯ = 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.shiftMonoidalFunctor C A).εIso.symm

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

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

Equations

• CategoryTheory.shiftFunctorZero' C a ha = CategoryTheory.eqToIso ⋯ ≪≫ CategoryTheory.shiftFunctorZero C A

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 ⋯ = (CategoryTheory.shiftFunctor C a).leftUnitor.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 ⋯ = (CategoryTheory.shiftFunctor C a).rightUnitor.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₁₂₃ ⋯ ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂) (CategoryTheory.shiftFunctor C a₃) ≪≫ (CategoryTheory.shiftFunctor C a₁).associator (CategoryTheory.shiftFunctor C a₂) (CategoryTheory.shiftFunctor C a₃) = CategoryTheory.shiftFunctorAdd' C 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.shiftFunctor C a₁).associator (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₃)

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 ⋯).hom.app X = (CategoryTheory.shiftFunctor C a).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 a).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 ⋯).inv.app X = (CategoryTheory.shiftFunctor C a).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).map ((CategoryTheory.shiftFunctorZero C A).hom.app X)) (CategoryTheory.eqToHom ⋯)

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 ⋯).hom.app X = (CategoryTheory.shiftFunctorZero C A).inv.app ((CategoryTheory.shiftFunctor C a).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.shiftFunctorZero C A).inv.app ((CategoryTheory.shiftFunctor C a).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 ⋯).inv.app X = (CategoryTheory.shiftFunctorZero C A).hom.app ((CategoryTheory.shiftFunctor C a).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).obj X)) (CategoryTheory.eqToHom ⋯)

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₁₂₃ ⋯).hom.app X) ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).hom.app X) ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app ((CategoryTheory.shiftFunctor C a₁).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₃).obj ((CategoryTheory.shiftFunctor C a₂).obj ((CategoryTheory.shiftFunctor C a₁).obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app ((CategoryTheory.shiftFunctor C a₁).obj 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₃).map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X)) ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((CategoryTheory.shiftFunctor C a₁).obj X)) ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).inv.app 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₁₂₃).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).inv.app X) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((CategoryTheory.shiftFunctor C a₁).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).inv.app 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₃).map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).hom.app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).hom.app X) ((CategoryTheory.shiftFunctorAdd C a₂ a₃).hom.app ((CategoryTheory.shiftFunctor C a₁).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) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C a₃).obj ((CategoryTheory.shiftFunctor C a₂).obj ((CategoryTheory.shiftFunctor C a₁).obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).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₃).hom.app ((CategoryTheory.shiftFunctor C a₁).obj 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₃).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₁).obj X)) ((CategoryTheory.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} [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₃)).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).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₁).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).inv.app X) h)

@[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.obj { as := n }).obj X = (CategoryTheory.shiftFunctor C n).obj X

@[reducible, inline]

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)).obj X ≅ (CategoryTheory.shiftFunctor C j).obj ((CategoryTheory.shiftFunctor C i).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).map ((CategoryTheory.shiftFunctor C i).map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftAdd X i j).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C (i + j)).map f) (CategoryTheory.shiftAdd Y i j).hom)

@[reducible, inline]

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).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).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.shiftFunctor C i).comp (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

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.

@[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'_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'_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 ⋯

@[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

@[reducible, inline]

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) ⋯

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

Shifting by i is an equivalence.

Equations

• ⋯ = ⋯

@[reducible, inline]

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)).obj ((CategoryTheory.shiftFunctor C i).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

@[reducible, inline]

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).obj ((CategoryTheory.shiftFunctor C (-i)).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)).map ((CategoryTheory.shiftFunctor C i).map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C i (-i) ⋯).hom.app X) (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctorCompIsoId C i (-i) ⋯).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).map ((CategoryTheory.shiftFunctor C (-i)).map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C (-i) i ⋯).hom.app X) (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctorCompIsoId C (-i) i ⋯).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).map (CategoryTheory.shiftShiftNeg X n).inv) (CategoryTheory.shiftNegShift ((CategoryTheory.shiftFunctor C n).obj X) n).hom = CategoryTheory.CategoryStruct.id ((CategoryTheory.shiftFunctor C n).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).map ((CategoryTheory.shiftFunctorCompIsoId C n m h).hom.app X) = (CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app ((CategoryTheory.shiftFunctor C n).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).map ((CategoryTheory.shiftFunctorCompIsoId C n m h).inv.app X) = (CategoryTheory.shiftFunctorCompIsoId C m n ⋯).inv.app ((CategoryTheory.shiftFunctor C n).obj X)

theorem CategoryTheory.shift_shiftFunctorCompIsoId_add_neg_cancel_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).map ((CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).hom.app X) = (CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).hom.app ((CategoryTheory.shiftFunctor C n).obj X)

theorem CategoryTheory.shift_shiftFunctorCompIsoId_add_neg_cancel_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).map ((CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).inv.app X) = (CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).inv.app ((CategoryTheory.shiftFunctor C n).obj X)

theorem CategoryTheory.shift_shiftFunctorCompIsoId_neg_add_cancel_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)).map ((CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).hom.app X) = (CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).hom.app ((CategoryTheory.shiftFunctor C (-n)).obj X)

theorem CategoryTheory.shift_shiftFunctorCompIsoId_neg_add_cancel_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)).map ((CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).inv.app X) = (CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).inv.app ((CategoryTheory.shiftFunctor C (-n)).obj X)

theorem CategoryTheory.shiftFunctorCompIsoId_zero_zero_hom_app {C : Type u} (A : Type u_1) [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (X : C) : (CategoryTheory.shiftFunctorCompIsoId C 0 0 ⋯).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 0).map ((CategoryTheory.shiftFunctorZero C A).hom.app X)) ((CategoryTheory.shiftFunctorZero C A).hom.app X)

theorem CategoryTheory.shiftFunctorCompIsoId_zero_zero_inv_app {C : Type u} (A : Type u_1) [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (X : C) : (CategoryTheory.shiftFunctorCompIsoId C 0 0 ⋯).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C A).inv.app X) ((CategoryTheory.shiftFunctor C 0).map ((CategoryTheory.shiftFunctorZero C A).inv.app X))

theorem CategoryTheory.shiftFunctorCompIsoId_add'_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] {X : C} (m : A) (n : A) (p : A) (m' : A) (n' : A) (p' : A) (hm : m' + m = 0) (hn : n' + n = 0) (hp : p' + p = 0) (h : m + n = p) : (CategoryTheory.shiftFunctorCompIsoId C p' p hp).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C n' n hn).inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C m' m hm).inv.app ((CategoryTheory.shiftFunctor C n').obj X))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C m n p h).inv.app ((CategoryTheory.shiftFunctor C m').obj ((CategoryTheory.shiftFunctor C n').obj X))) ((CategoryTheory.shiftFunctor C p).map ((CategoryTheory.shiftFunctorAdd' C n' m' p' ⋯).inv.app X))))

theorem CategoryTheory.shiftFunctorCompIsoId_add'_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] {X : C} (m : A) (n : A) (p : A) (m' : A) (n' : A) (p' : A) (hm : m' + m = 0) (hn : n' + n = 0) (hp : p' + p = 0) (h : m + n = p) : (CategoryTheory.shiftFunctorCompIsoId C p' p hp).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C p).map ((CategoryTheory.shiftFunctorAdd' C n' m' p' ⋯).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C m n p h).hom.app ((CategoryTheory.shiftFunctor C m').obj ((CategoryTheory.shiftFunctor C n').obj X))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C m' m hm).hom.app ((CategoryTheory.shiftFunctor C n').obj X))) ((CategoryTheory.shiftFunctorCompIsoId C n' n hn).hom.app 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).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.shiftFunctor C i).comp (CategoryTheory.shiftFunctor C j) ≅ (CategoryTheory.shiftFunctor C j).comp (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) ⋯

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 ⋯

@[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.shiftFunctor C i).comp (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

@[reducible, inline]

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).obj ((CategoryTheory.shiftFunctor C i).obj X) ≅ (CategoryTheory.shiftFunctor C i).obj ((CategoryTheory.shiftFunctor C j).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).map ((CategoryTheory.shiftFunctor C i).map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm X i j).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C i).map ((CategoryTheory.shiftFunctor C j).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 {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).map ((CategoryTheory.shiftFunctor C j).map f)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C j).map ((CategoryTheory.shiftFunctor C i).map f)) (CategoryTheory.shiftComm Y i j).hom

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).obj ((CategoryTheory.shiftFunctor C j).obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm X i j).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C i).map ((CategoryTheory.shiftFunctor C j).map f)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C j).map ((CategoryTheory.shiftFunctor C i).map f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm Y i j).hom h)

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).obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C n 0).hom.app X) ((CategoryTheory.shiftFunctor C n).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).obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).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).obj X)) ((CategoryTheory.shiftFunctor C a).map ((CategoryTheory.shiftFunctorZero C A).inv.app X))

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₁).map ((CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app ((CategoryTheory.shiftFunctor C m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C m₃).map ((CategoryTheory.shiftFunctorComm C m₁ m₂).hom.app X)) ((CategoryTheory.shiftFunctorComm C m₁ m₃).hom.app ((CategoryTheory.shiftFunctor C m₂).obj 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₁).obj ((CategoryTheory.shiftFunctor C m₃).obj ((CategoryTheory.shiftFunctor C m₂).obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C m₁).map ((CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app X)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app ((CategoryTheory.shiftFunctor C m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C m₃).map ((CategoryTheory.shiftFunctorComm C m₁ m₂).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C m₁ m₃).hom.app ((CategoryTheory.shiftFunctor C m₂).obj X)) h))

def CategoryTheory.Functor.FullyFaithful.hasShift.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} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) : s 0 ≅ CategoryTheory.Functor.id C

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} [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} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (X : C) : F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.zero hF s i).hom.app X) = CategoryTheory.CategoryStruct.comp ((i 0).hom.app X) ((CategoryTheory.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} [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} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (X : C) : F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.zero hF s i).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.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} [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} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (a : 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} [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} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (a : A) (b : A) (X : C) : F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.add hF 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.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.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} [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} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (a : A) (b : A) (X : C) : F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.add hF s i a b).inv.app X) = CategoryTheory.CategoryStruct.comp ((i b).hom.app ((s a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((i a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.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} [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} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (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.