mathlib3 documentation

category_theory.shift.basic

Shift #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

Implementation Notes #

[has_shift C A] is implemented using monoidal_functor (discrete A) (C ⥤ C). However, the API of monodial functors is used only internally: one should use the API of shifts functors which includes shift_functor C a : C ⥤ C for a : A, shift_functor_zero C A : shift_functor C (0 : A) ≅ 𝟭 C and shift_functor_add C i j : shift_functor C (i + j) ≅ shift_functor C i ⋙ shift_functor C j (and its variant shift_functor_add'). These isomorphisms satisfy some coherence properties which are stated in lemmas like shift_functor_add'_assoc, shift_functor_add'_zero_add and shift_functor_add'_add_zero.

@[class]
structure category_theory.has_shift (C : Type u) (A : Type u_2) [category_theory.category C] [add_monoid A] :
Type (max u u_2 v)

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

Instances of this typeclass
Instances of other typeclasses for category_theory.has_shift
  • category_theory.has_shift.has_sizeof_inst
@[nolint]
structure category_theory.shift_mk_core (C : Type u) (A : Type u_1) [category_theory.category C] [add_monoid A] :
Type (max u u_1 v)

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

Instances for category_theory.shift_mk_core
  • category_theory.shift_mk_core.has_sizeof_inst
theorem category_theory.shift_mk_core.assoc_hom_app_assoc {C : Type u} {A : Type u_1} [category_theory.category C] [add_monoid A] (self : category_theory.shift_mk_core C A) (m₁ m₂ m₃ : A) (X : C) {X' : C} (f' : (self.F m₃).obj ((self.F m₁ self.F m₂).obj X) X') :
(self.add (m₁ + m₂) m₃).hom.app X (self.F m₃).map ((self.add m₁ m₂).hom.app X) f' = category_theory.eq_to_hom _ (self.add m₁ (m₂ + m₃)).hom.app X (self.add m₂ m₃).hom.app ((self.F m₁).obj X) f'
theorem category_theory.shift_mk_core.assoc_inv_app {C : Type u} {A : Type u_1} [category_theory.category C] [add_monoid A] (h : category_theory.shift_mk_core C A) (m₁ m₂ m₃ : A) (X : C) :
(h.F m₃).map ((h.add m₁ m₂).inv.app X) (h.add (m₁ + m₂) m₃).inv.app X = (h.add m₂ m₃).inv.app ((h.F m₁).obj X) (h.add m₁ (m₂ + m₃)).inv.app X category_theory.eq_to_hom _
theorem category_theory.shift_mk_core.assoc_inv_app_assoc {C : Type u} {A : Type u_1} [category_theory.category C] [add_monoid A] (h : category_theory.shift_mk_core C A) (m₁ m₂ m₃ : A) (X : C) {X' : C} (f' : (h.F (m₁ + m₂ + m₃)).obj X X') :
(h.F m₃).map ((h.add m₁ m₂).inv.app X) (h.add (m₁ + m₂) m₃).inv.app X f' = (h.add m₂ m₃).inv.app ((h.F m₁).obj X) (h.add m₁ (m₂ + m₃)).inv.app X category_theory.eq_to_hom _ f'

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

Equations
Instances for category_theory.shift_functor

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

Equations

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

Equations
theorem category_theory.shift_functor_add'_assoc (C : Type u) {A : Type u_1} [category_theory.category C] [add_monoid A] [category_theory.has_shift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) :
theorem category_theory.shift_functor_add'_assoc_hom_app_assoc {C : Type u} {A : Type u_1} [category_theory.category C] [add_monoid A] [category_theory.has_shift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) {X' : C} (f' : (category_theory.shift_functor C a₃).obj ((category_theory.shift_functor C a₁ category_theory.shift_functor C a₂).obj X) X') :
(category_theory.shift_functor_add' C a₁₂ a₃ a₁₂₃ _).hom.app X (category_theory.shift_functor C a₃).map ((category_theory.shift_functor_add' C a₁ a₂ a₁₂ h₁₂).hom.app X) f' = (category_theory.shift_functor_add' C a₁ a₂₃ a₁₂₃ _).hom.app X (category_theory.shift_functor_add' C a₂ a₃ a₂₃ h₂₃).hom.app ((category_theory.shift_functor C a₁).obj X) f'
theorem category_theory.shift_functor_add'_assoc_hom_app {C : Type u} {A : Type u_1} [category_theory.category C] [add_monoid A] [category_theory.has_shift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) :
(category_theory.shift_functor_add' C a₁₂ a₃ a₁₂₃ _).hom.app X (category_theory.shift_functor C a₃).map ((category_theory.shift_functor_add' C a₁ a₂ a₁₂ h₁₂).hom.app X) = (category_theory.shift_functor_add' C a₁ a₂₃ a₁₂₃ _).hom.app X (category_theory.shift_functor_add' C a₂ a₃ a₂₃ h₂₃).hom.app ((category_theory.shift_functor C a₁).obj X)
theorem category_theory.shift_functor_add'_assoc_inv_app {C : Type u} {A : Type u_1} [category_theory.category C] [add_monoid A] [category_theory.has_shift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) :
(category_theory.shift_functor C a₃).map ((category_theory.shift_functor_add' C a₁ a₂ a₁₂ h₁₂).inv.app X) (category_theory.shift_functor_add' C a₁₂ a₃ a₁₂₃ _).inv.app X = (category_theory.shift_functor_add' C a₂ a₃ a₂₃ h₂₃).inv.app ((category_theory.shift_functor C a₁).obj X) (category_theory.shift_functor_add' C a₁ a₂₃ a₁₂₃ _).inv.app X
theorem category_theory.shift_functor_add'_assoc_inv_app_assoc {C : Type u} {A : Type u_1} [category_theory.category C] [add_monoid A] [category_theory.has_shift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) {X' : C} (f' : (category_theory.shift_functor C a₁₂₃).obj X X') :
(category_theory.shift_functor C a₃).map ((category_theory.shift_functor_add' C a₁ a₂ a₁₂ h₁₂).inv.app X) (category_theory.shift_functor_add' C a₁₂ a₃ a₁₂₃ _).inv.app X f' = (category_theory.shift_functor_add' C a₂ a₃ a₂₃ h₂₃).inv.app ((category_theory.shift_functor C a₁).obj X) (category_theory.shift_functor_add' C a₁ a₂₃ a₁₂₃ _).inv.app X f'
theorem category_theory.shift_functor_add_assoc_inv_app_assoc {C : Type u} {A : Type u_1} [category_theory.category C] [add_monoid A] [category_theory.has_shift C A] (a₁ a₂ a₃ : A) (X : C) {X' : C} (f' : (category_theory.shift_functor C (a₁ + a₂ + a₃)).obj X X') :
@[reducible]

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

@[reducible]

Shifting by zero is the identity functor.

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

Equations
noncomputable def category_theory.shift_equiv' (C : Type u) {A : Type u_1} [category_theory.category C] [add_group A] [category_theory.has_shift 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
@[reducible]
noncomputable def category_theory.shift_equiv (C : Type u) {A : Type u_1} [category_theory.category C] [add_group A] [category_theory.has_shift C A] (i : A) :
C C

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

@[protected, instance]

Shifting by n is an essentially surjective functor.

@[reducible]

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

@[reducible]

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

@[reducible]

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

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

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

Equations