# mathlibdocumentation

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 #

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

## 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) [add_monoid A] :
Type (max u u_2 v)
• shift :

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) [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} [add_monoid A] (self : 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' = (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} [add_monoid A] (h : 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
theorem category_theory.shift_mk_core.assoc_inv_app_assoc {C : Type u} {A : Type u_1} [add_monoid A] (h : 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
theorem category_theory.shift_mk_core.zero_add_inv_app {C : Type u} {A : Type u_1} [add_monoid A] (h : A) (n : A) (X : C) :
(h.add 0 n).inv.app X = (h.F n).map (h.zero.hom.app X)
theorem category_theory.shift_mk_core.add_zero_inv_app {C : Type u} {A : Type u_1} [add_monoid A] (h : A) (n : A) (X : C) :
(h.add n 0).inv.app X = h.zero.hom.app ((h.F n).obj X)
def category_theory.has_shift_mk (C : Type u) (A : Type u_1) [add_monoid A] (h : A) :

Constructs a `has_shift C A` instance from `shift_mk_core`.

Equations

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

Equations
def category_theory.shift_functor (C : Type u) {A : Type u_1} [add_monoid A] (i : A) :
C C

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

Equations
Instances for `category_theory.shift_functor`
noncomputable def category_theory.shift_functor_add (C : Type u) {A : Type u_1} [add_monoid A] (i j : A) :

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

Equations
noncomputable def category_theory.shift_functor_add' (C : Type u) {A : Type u_1} [add_monoid A] (i j k : A) (h : i + j = k) :

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

Equations
theorem category_theory.shift_functor_add'_eq_shift_functor_add (C : Type u) {A : Type u_1} [add_monoid A] (i j : A) :
(i + j) rfl =
noncomputable def category_theory.shift_functor_zero (C : Type u) (A : Type u_1) [add_monoid A]  :

Shifting by zero is the identity functor.

Equations
theorem category_theory.shift_mk_core.shift_functor_eq {C : Type u} {A : Type u_1} [add_monoid A] (h : A) (a : A) :
= h.F a
theorem category_theory.shift_mk_core.shift_functor_add_eq {C : Type u} {A : Type u_1} [add_monoid A] (h : A) (a b : A) :
theorem category_theory.shift_functor_add'_assoc (C : Type u) {A : Type u_1} [add_monoid A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) :
a₁₂₃ _ ≪≫ category_theory.iso_whisker_right a₁₂ h₁₂) ≪≫ = a₁₂₃ _ ≪≫ a₂₃ h₂₃)
theorem category_theory.shift_functor_add_assoc (C : Type u) {A : Type u_1} [add_monoid A] (a₁ a₂ a₃ : A) :
(a₁ + a₂) a₃ ≪≫ = (a₂ + a₃) (a₁ + a₂ + a₃) _ ≪≫
theorem category_theory.shift_functor_add'_zero_add_hom_app {C : Type u} {A : Type u_1} [add_monoid A] (a : A) (X : C) :
_).hom.app X = X)
theorem category_theory.shift_functor_add_zero_add_hom_app {C : Type u} {A : Type u_1} [add_monoid A] (a : A) (X : C) :
.hom.app X =
theorem category_theory.shift_functor_add'_zero_add_inv_app {C : Type u} {A : Type u_1} [add_monoid A] (a : A) (X : C) :
_).inv.app X = X)
theorem category_theory.shift_functor_add_zero_add_inv_app {C : Type u} {A : Type u_1} [add_monoid A] (a : A) (X : C) :
.inv.app X =
theorem category_theory.shift_functor_add'_add_zero_hom_app {C : Type u} {A : Type u_1} [add_monoid A] (a : A) (X : C) :
_).hom.app X = .obj X)
theorem category_theory.shift_functor_add_add_zero_hom_app {C : Type u} {A : Type u_1} [add_monoid A] (a : A) (X : C) :
.hom.app X =
theorem category_theory.shift_functor_add'_add_zero_inv_app {C : Type u} {A : Type u_1} [add_monoid A] (a : A) (X : C) :
_).inv.app X = .obj X)
theorem category_theory.shift_functor_add_add_zero_inv_app {C : Type u} {A : Type u_1} [add_monoid A] (a : A) (X : C) :
.inv.app X =
theorem category_theory.shift_functor_add'_assoc_hom_app_assoc {C : Type u} {A : Type u_1} [add_monoid 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' : .obj .obj X) X') :
a₃ a₁₂₃ _).hom.app X .map a₂ a₁₂ h₁₂).hom.app X) f' = a₂₃ a₁₂₃ _).hom.app X a₂₃ h₂₃).hom.app .obj X) f'
theorem category_theory.shift_functor_add'_assoc_hom_app {C : Type u} {A : Type u_1} [add_monoid A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) :
a₃ a₁₂₃ _).hom.app X .map a₂ a₁₂ h₁₂).hom.app X) = a₂₃ a₁₂₃ _).hom.app X a₂₃ h₂₃).hom.app .obj X)
theorem category_theory.shift_functor_add'_assoc_inv_app {C : Type u} {A : Type u_1} [add_monoid A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) :
.map a₂ a₁₂ h₁₂).inv.app X) a₃ a₁₂₃ _).inv.app X = a₂₃ h₂₃).inv.app .obj X) a₂₃ a₁₂₃ _).inv.app X
theorem category_theory.shift_functor_add'_assoc_inv_app_assoc {C : Type u} {A : Type u_1} [add_monoid 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' : a₁₂₃).obj X X') :
.map a₂ a₁₂ h₁₂).inv.app X) a₃ a₁₂₃ _).inv.app X f' = a₂₃ h₂₃).inv.app .obj X) a₂₃ a₁₂₃ _).inv.app X f'
theorem category_theory.shift_functor_add_assoc_hom_app {C : Type u} {A : Type u_1} [add_monoid A] (a₁ a₂ a₃ : A) (X : C) :
(a₁ + a₂) a₃).hom.app X .map a₂).hom.app X) = (a₂ + a₃) (a₁ + a₂ + a₃) _).hom.app X a₃).hom.app .obj X)
theorem category_theory.shift_functor_add_assoc_hom_app_assoc {C : Type u} {A : Type u_1} [add_monoid A] (a₁ a₂ a₃ : A) (X : C) {X' : C} (f' : .obj .obj X) X') :
(a₁ + a₂) a₃).hom.app X .map a₂).hom.app X) f' = (a₂ + a₃) (a₁ + a₂ + a₃) _).hom.app X a₃).hom.app .obj X) f'
theorem category_theory.shift_functor_add_assoc_inv_app {C : Type u} {A : Type u_1} [add_monoid A] (a₁ a₂ a₃ : A) (X : C) :
.map a₂).inv.app X) (a₁ + a₂) a₃).inv.app X = a₃).inv.app .obj X) (a₂ + a₃) (a₁ + a₂ + a₃) _).inv.app X
theorem category_theory.shift_functor_add_assoc_inv_app_assoc {C : Type u} {A : Type u_1} [add_monoid A] (a₁ a₂ a₃ : A) (X : C) {X' : C} (f' : (a₁ + a₂ + a₃)).obj X X') :
.map a₂).inv.app X) (a₁ + a₂) a₃).inv.app X f' = a₃).inv.app .obj X) (a₂ + a₃) (a₁ + a₂ + a₃) _).inv.app X f'
@[simp]
theorem category_theory.has_shift.shift_obj_obj {C : Type u} {A : Type u_1} [add_monoid A] (n : A) (X : C) :
@[reducible]
noncomputable def category_theory.shift_add {C : Type u} {A : Type u_1} [add_monoid A] (X : C) (i j : A) :
(i + j)).obj X .obj X)

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

theorem category_theory.shift_shift' {C : Type u} {A : Type u_1} [add_monoid A] (X Y : C) (f : X Y) (i j : A) :
.map f) = j).inv (i + j)).map f j).hom
@[reducible]
noncomputable def category_theory.shift_zero {C : Type u} (A : Type u_1) [add_monoid A] (X : C) :
X X

Shifting by zero is the identity functor.

theorem category_theory.shift_zero' {C : Type u} (A : Type u_1) [add_monoid A] (X Y : C) (f : X Y) :
f = f
noncomputable def category_theory.shift_functor_comp_iso_id (C : Type u) {A : Type u_1} [add_monoid A] (i j : A) (h : i + j = 0) :

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

Equations
@[simp]
theorem category_theory.shift_equiv'_inverse (C : Type u) {A : Type u_1} [add_group A] (i j : A) (h : i + j = 0) :
@[simp]
theorem category_theory.shift_equiv'_unit_iso (C : Type u) {A : Type u_1} [add_group A] (i j : A) (h : i + j = 0) :
h).unit_iso =
@[simp]
theorem category_theory.shift_equiv'_counit_iso (C : Type u) {A : Type u_1} [add_group A] (i j : A) (h : i + j = 0) :
noncomputable def category_theory.shift_equiv' (C : Type u) {A : Type u_1} [add_group 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
• h =
@[simp]
theorem category_theory.shift_equiv'_functor (C : Type u) {A : Type u_1} [add_group A] (i j : A) (h : i + j = 0) :
@[reducible]
noncomputable def category_theory.shift_equiv (C : Type u) {A : Type u_1} [add_group A] (i : A) :
C C

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

@[protected, instance]
noncomputable def category_theory.shift_functor.is_equivalence (C : Type u) {A : Type u_1} [add_group A] (i : A) :

Shifting by `i` is an equivalence.

Equations
@[simp]
theorem category_theory.shift_functor_inv (C : Type u) {A : Type u_1} [add_group A] (i : A) :
@[protected, instance]
def category_theory.shift_functor_ess_surj (C : Type u) {A : Type u_1} [add_group A] (i : A) :

Shifting by `n` is an essentially surjective functor.

@[reducible]
noncomputable def category_theory.shift_shift_neg {C : Type u} {A : Type u_1} [add_group A] (X : C) (i : A) :
.obj .obj X) X

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

@[reducible]
noncomputable def category_theory.shift_neg_shift {C : Type u} {A : Type u_1} [add_group A] (X : C) (i : A) :
(-i)).obj X) X

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

theorem category_theory.shift_shift_neg' {C : Type u} {A : Type u_1} [add_group A] {X Y : C} (f : X Y) (i : A) :
.map .map f) = _).hom.app X f _).inv.app Y
theorem category_theory.shift_neg_shift' {C : Type u} {A : Type u_1} [add_group A] {X Y : C} (f : X Y) (i : A) :
(-i)).map f) = _).hom.app X f _).inv.app Y
theorem category_theory.shift_equiv_triangle {C : Type u} {A : Type u_1} [add_group A] (n : A) (X : C) :
= 𝟙 .obj X)
theorem category_theory.shift_shift_functor_comp_iso_id_hom_app {C : Type u} {A : Type u_1} [add_group A] (n m : A) (h : n + m = 0) (X : C) :
.hom.app X) = .hom.app .obj X)
theorem category_theory.shift_shift_functor_comp_iso_id_inv_app {C : Type u} {A : Type u_1} [add_group A] (n m : A) (h : n + m = 0) (X : C) :
.inv.app X) = .inv.app .obj X)
theorem category_theory.shift_shift_functor_comp_iso_id_add_neg_self_hom_app {C : Type u} {A : Type u_1} [add_group A] (n : A) (X : C) :
_).hom.app X) = _).hom.app .obj X)
theorem category_theory.shift_shift_functor_comp_iso_id_add_neg_self_inv_app {C : Type u} {A : Type u_1} [add_group A] (n : A) (X : C) :
_).inv.app X) = _).inv.app .obj X)
theorem category_theory.shift_shift_functor_comp_iso_id_neg_add_self_hom_app {C : Type u} {A : Type u_1} [add_group A] (n : A) (X : C) :
.map _).hom.app X) = _).hom.app (-n)).obj X)
theorem category_theory.shift_shift_functor_comp_iso_id_neg_add_self_inv_app {C : Type u} {A : Type u_1} [add_group A] (n : A) (X : C) :
.map _).inv.app X) = _).inv.app (-n)).obj X)
theorem category_theory.shift_zero_eq_zero {C : Type u} {A : Type u_1} [add_group A] (X Y : C) (n : A) :
0 = 0
noncomputable def category_theory.shift_functor_comm (C : Type u) {A : Type u_1} (i j : A) :

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

Equations
theorem category_theory.shift_functor_comm_eq (C : Type u) {A : Type u_1} (i j k : A) (h : i + j = k) :
= h).symm ≪≫ _
theorem category_theory.shift_functor_comm_symm (C : Type u) {A : Type u_1} (i j : A) :
@[reducible]
noncomputable def category_theory.shift_comm {C : Type u} {A : Type u_1} (X : C) (i j : A) :
.obj X) .obj X)

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

@[simp]
theorem category_theory.shift_comm_symm {C : Type u} {A : Type u_1} (X : C) (i j : A) :
j).symm =
theorem category_theory.shift_comm' {C : Type u} {A : Type u_1} {X Y : C} (f : X Y) (i j : A) :
.map f) = j).hom .map f) i).hom

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

theorem category_theory.shift_comm_hom_comp_assoc {C : Type u} {A : Type u_1} {X Y : C} (f : X Y) (i j : A) {X' : C} (f' : .obj Y) X') :
j).hom .map f) f' = .map f) j).hom f'
theorem category_theory.shift_comm_hom_comp {C : Type u} {A : Type u_1} {X Y : C} (f : X Y) (i j : A) :
j).hom .map f) = .map f) j).hom
theorem category_theory.shift_functor_zero_hom_app_shift {C : Type u} {A : Type u_1} {X : C} (n : A) :
.obj X) = .app X X)
theorem category_theory.shift_functor_zero_inv_app_shift {C : Type u} {A : Type u_1} {X : C} (n : A) :
.obj X) = X) .app X
theorem category_theory.shift_functor_comm_hom_app_comp_shift_shift_functor_add_hom_app_assoc {C : Type u} {A : Type u_1} (m₁ m₂ m₃ : A) (X : C) {X' : C} (f' : .obj .obj X) X') :
(m₂ + m₃)).hom.app X .map m₃).hom.app X) f' = m₃).hom.app .obj X) .map m₂).hom.app X) m₃).hom.app .obj X) f'
theorem category_theory.shift_functor_comm_hom_app_comp_shift_shift_functor_add_hom_app {C : Type u} {A : Type u_1} (m₁ m₂ m₃ : A) (X : C) :
(m₂ + m₃)).hom.app X .map m₃).hom.app X) = m₃).hom.app .obj X) .map m₂).hom.app X) m₃).hom.app .obj X)
noncomputable def category_theory.has_shift_of_fully_faithful_zero {C : Type u} {A : Type u_1} {D : Type u_2} [add_monoid A] (F : C D) (s : A C C) (i : Π (i : A), s i F ) :
s 0 𝟭 C

auxiliary definition for `has_shift_of_fully_faithful`

Equations
@[simp]
theorem category_theory.map_has_shift_of_fully_faithful_zero_hom_app {C : Type u} {A : Type u_1} {D : Type u_2} [add_monoid A] (F : C D) (s : A C C) (i : Π (i : A), s i F ) (X : C) :
F.map = (i 0).hom.app X (F.obj X)
@[simp]
theorem category_theory.map_has_shift_of_fully_faithful_zero_inv_app {C : Type u} {A : Type u_1} {D : Type u_2} [add_monoid A] (F : C D) (s : A C C) (i : Π (i : A), s i F ) (X : C) :
F.map = (F.obj X) (i 0).inv.app X
noncomputable def category_theory.has_shift_of_fully_faithful_add {C : Type u} {A : Type u_1} {D : Type u_2} [add_monoid A] (F : C D) (s : A C C) (i : Π (i : A), s i F ) (a b : A) :
s (a + b) s a s b

auxiliary definition for `has_shift_of_fully_faithful`

Equations
@[simp]
theorem category_theory.map_has_shift_of_fully_faithful_add_hom_app {C : Type u} {A : Type u_1} {D : Type u_2} [add_monoid A] (F : C D) (s : A C C) (i : Π (i : A), s i F ) (a b : A) (X : C) :
F.map b).hom.app X) = (i (a + b)).hom.app X .hom.app (F.obj X) ((i a).inv.app X) (i b).inv.app ((s a).obj X)
@[simp]
theorem category_theory.map_has_shift_of_fully_faithful_add_inv_app {C : Type u} {A : Type u_1} {D : Type u_2} [add_monoid A] (F : C D) (s : A C C) (i : Π (i : A), s i F ) (a b : A) (X : C) :
F.map b).inv.app X) = (i b).hom.app ((s a).obj X) ((i a).hom.app X) .inv.app (F.obj X) (i (a + b)).inv.app X
noncomputable def category_theory.has_shift_of_fully_faithful {C : Type u} {A : Type u_1} {D : Type u_2} [add_monoid A] (F : C D) (s : A C C) (i : Π (i : A), s i F ) :

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