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

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

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

• shift : Functor (Discrete A) (Functor C C)

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

• shiftMonoidal : shift.Monoidal

  shift is monoidal

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

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

• F : A → Functor C C

  the family of shift functors

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

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

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

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

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

instance CategoryTheory.instMonoidalDiscreteFunctorFunctorF (C : Type u) (A : Type u_1) [Category.{v, u} C] [AddMonoid A] (h : ShiftMkCore C A) : (Discrete.functor h.F).Monoidal

Equations

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

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

Constructs a HasShift C A instance from ShiftMkCore.

Equations

• CategoryTheory.hasShiftMk C A h = { shift := CategoryTheory.Discrete.functor h.F, shiftMonoidal := inferInstance }

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

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

Equations

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

instance CategoryTheory.instMonoidalDiscreteFunctorShiftMonoidalFunctor (C : Type u) (A : Type u_1) [Category.{v, u} C] [AddMonoid A] [HasShift C A] : (shiftMonoidalFunctor C A).Monoidal

Equations

• CategoryTheory.instMonoidalDiscreteFunctorShiftMonoidalFunctor C A = CategoryTheory.HasShift.shiftMonoidal

def CategoryTheory.shiftFunctor (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (i : A) : 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} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (i j : A) : shiftFunctor C (i + j) ≅ (shiftFunctor C i).comp (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.Functor.Monoidal.μIso (CategoryTheory.shiftMonoidalFunctor C A) { as := i } { as := j }).symm

def CategoryTheory.shiftFunctorAdd' (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (i j k : A) (h : i + j = k) : shiftFunctor C k ≅ (shiftFunctor C i).comp (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} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (i j : A) : shiftFunctorAdd' C i j (i + j) ⋯ = shiftFunctorAdd C i j

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

Shifting by zero is the identity functor.

Equations

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

def CategoryTheory.shiftFunctorZero' (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a : A) (ha : a = 0) : shiftFunctor C a ≅ 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} [Category.{v, u} C] [AddMonoid A] (h : ShiftMkCore C A) (a : A) : shiftFunctor C a = h.F a

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

theorem CategoryTheory.ShiftMkCore.shiftFunctorAdd_eq {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddMonoid A] (h : ShiftMkCore C A) (a b : A) : 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} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (a : A) : shiftFunctorAdd' C 0 a a ⋯ = (shiftFunctor C a).leftUnitor.symm ≪≫ isoWhiskerRight (shiftFunctorZero C A).symm (shiftFunctor C a)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[reducible, inline]

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

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

Equations

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

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

@[reducible, inline]

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

Shifting by zero is the identity functor.

Equations

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

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

def CategoryTheory.shiftFunctorCompIsoId (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddMonoid A] [HasShift C A] (i j : A) (h : i + j = 0) : (shiftFunctor C i).comp (shiftFunctor C j) ≅ 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} [Category.{v, u} C] [AddGroup A] [HasShift C A] (i j : A) (h : i + j = 0) : C ≌ C

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[reducible, inline]

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

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

Equations

• CategoryTheory.shiftEquiv C n = CategoryTheory.shiftEquiv' C n (-n) ⋯

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

Shifting by i is an equivalence.

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

def CategoryTheory.shiftFunctorComm (C : Type u) {A : Type u_1} [Category.{v, u} C] [AddCommMonoid A] [HasShift C A] (i j : A) : (shiftFunctor C i).comp (shiftFunctor C j) ≅ (shiftFunctor C j).comp (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} [Category.{v, u} C] [AddCommMonoid A] [HasShift C A] (i j k : A) (h : i + j = k) : shiftFunctorComm C i j = (shiftFunctorAdd' C i j k h).symm ≪≫ shiftFunctorAdd' C j i k ⋯

@[simp]

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

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

@[reducible, inline]

abbrev CategoryTheory.shiftComm {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddCommMonoid A] [HasShift C A] (X : C) (i j : A) : (shiftFunctor C j).obj ((shiftFunctor C i).obj X) ≅ (shiftFunctor C i).obj ((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} [Category.{v, u} C] [AddCommMonoid A] [HasShift C A] (X : C) (i j : A) : (shiftComm X i j).symm = shiftComm X j i

theorem CategoryTheory.shiftComm' {C : Type u} {A : Type u_1} [Category.{v, u} C] [AddCommMonoid A] [HasShift C A] {X Y : C} (f : X ⟶ Y) (i j : A) : (shiftFunctor C j).map ((shiftFunctor C i).map f) = CategoryStruct.comp (shiftComm X i j).hom (CategoryStruct.comp ((shiftFunctor C i).map ((shiftFunctor C j).map f)) (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} [Category.{v, u} C] [AddCommMonoid A] [HasShift C A] {X Y : C} (f : X ⟶ Y) (i j : A) : CategoryStruct.comp (shiftComm X i j).hom ((shiftFunctor C i).map ((shiftFunctor C j).map f)) = CategoryStruct.comp ((shiftFunctor C j).map ((shiftFunctor C i).map f)) (shiftComm Y i j).hom

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

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

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

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

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

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

def CategoryTheory.Functor.FullyFaithful.hasShift.zero {C : Type u} {A : Type u_1} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] [AddMonoid A] [HasShift D A] {F : Functor C D} (hF : F.FullyFaithful) (s : A → Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (shiftFunctor D i)) : s 0 ≅ 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} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] [AddMonoid A] [HasShift D A] {F : Functor C D} (hF : F.FullyFaithful) (s : A → Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (shiftFunctor D i)) (X : C) : F.map ((zero hF s i).hom.app X) = CategoryStruct.comp ((i 0).hom.app X) ((shiftFunctorZero D A).hom.app (F.obj X))

@[simp]

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

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

auxiliary definition for FullyFaithful.hasShift

Equations

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

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.FullyFaithful.hasShift {C : Type u} {A : Type u_1} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] [AddMonoid A] [HasShift D A] {F : Functor C D} (hF : F.FullyFaithful) (s : A → Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (shiftFunctor D i)) : 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.