# mathlibdocumentation

category_theory.shift

# 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 #

• 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 #

Many of the definitions in this file are marked as an abbreviation so that the simp lemmas in category_theory/monoidal/End can apply.

@[simp]
theorem category_theory.eq_to_hom_μ_app {C : Type u} {A : Type u_1} [add_monoid A] (F : (C C)) {i j i' j' : A} (h₁ : i = i') (h₂ : j = j') (X : C) :
(F.to_lax_monoidal_functor.μ {as := i'} {as := j'}).app X = (F.to_lax_monoidal_functor.μ {as := i} {as := j}).app X
@[simp]
theorem category_theory.eq_to_hom_μ_app_assoc {C : Type u} {A : Type u_1} [add_monoid A] (F : (C C)) {i j i' j' : A} (h₁ : i = i') (h₂ : j = j') (X : C) {X' : C} (f' : (F.to_lax_monoidal_functor.to_functor.obj ({as := i'} {as := j'})).obj X X') :
(F.to_lax_monoidal_functor.μ {as := i'} {as := j'}).app X f' = (F.to_lax_monoidal_functor.μ {as := i} {as := j}).app X
@[simp]
theorem category_theory.μ_inv_app_eq_to_hom {C : Type u} {A : Type u_1} [add_monoid A] (F : (C C)) {i j i' j' : A} (h₁ : i = i') (h₂ : j = j') (X : C) :
@[simp]
theorem category_theory.μ_inv_app_eq_to_hom_assoc {C : Type u} {A : Type u_1} [add_monoid A] (F : (C C)) {i j i' j' : A} (h₁ : i = i') (h₂ : j = j') (X : C) {X' : C} (f' : (F.to_lax_monoidal_functor.to_functor.obj {as := i'} F.to_lax_monoidal_functor.to_functor.obj {as := j'}).obj X X') :
noncomputable def category_theory.add_neg_equiv {C : Type u} {A : Type u_1} [add_group A] (F : (C C)) (n : A) :
C C

A monoidal functor from a group A into C ⥤ C induces a self-equivalence of C for each n : A.

Equations
@[simp]
theorem category_theory.add_neg_equiv_functor {C : Type u} {A : Type u_1} [add_group A] (F : (C C)) (n : A) :
@[simp]
theorem category_theory.add_neg_equiv_unit_iso_hom {C : Type u} {A : Type u_1} [add_group A] (F : (C C)) (n : A) :
= {as := -n} .inv
@[simp]
theorem category_theory.add_neg_equiv_unit_iso_inv {C : Type u} {A : Type u_1} [add_group A] (F : (C C)) (n : A) :
= {as := -n} .hom
@[simp]
theorem category_theory.add_neg_equiv_counit_iso_hom {C : Type u} {A : Type u_1} [add_group A] (F : (C C)) (n : A) :
@[simp]
theorem category_theory.add_neg_equiv_inverse {C : Type u} {A : Type u_1} [add_group A] (F : (C C)) (n : A) :
@[simp]
theorem category_theory.add_neg_equiv_counit_iso_inv {C : Type u} {A : Type u_1} [add_group A] (F : (C C)) (n : A) :
@[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
@[simp]
theorem category_theory.has_shift_mk_shift_to_lax_monoidal_functor_to_functor (C : Type u) (A : Type u_1) [add_monoid A] (h : A) :
@[simp]
theorem category_theory.has_shift_mk_shift_to_lax_monoidal_functor_μ (C : Type u) (A : Type u_1) [add_monoid A] (h : A) (m n : category_theory.discrete A) :
= (h.μ m.as n.as).hom
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
@[simp]
theorem category_theory.has_shift_mk_shift_to_lax_monoidal_functor_ε (C : Type u) (A : Type u_1) [add_monoid A] (h : A) :
def category_theory.shift_monoidal_functor (C : Type u) (A : Type u_1) [add_monoid A]  :

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

Equations
@[reducible]
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'.

@[reducible]
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.

@[reducible]
noncomputable def category_theory.shift_functor_zero (C : Type u) (A : Type u_1) [add_monoid A]  :

Shifting by zero is the identity functor.

@[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_add_hom_comp_eq_to_hom₁_assoc {C : Type u} {A : Type u_1} [add_monoid A] (X : C) (i i' j : A) (h : i = i') {X' : C} (f' : .obj X) X') :
j).hom = j).hom f'
theorem category_theory.shift_add_hom_comp_eq_to_hom₁ {C : Type u} {A : Type u_1} [add_monoid A] (X : C) (i i' j : A) (h : i = i') :
theorem category_theory.shift_add_hom_comp_eq_to_hom₂_assoc {C : Type u} {A : Type u_1} [add_monoid A] (X : C) (i j j' : A) (h : j = j') {X' : C} (f' : .obj .obj X) X') :
j).hom = j').hom f'
theorem category_theory.shift_add_hom_comp_eq_to_hom₂ {C : Type u} {A : Type u_1} [add_monoid A] (X : C) (i j j' : A) (h : j = j') :
theorem category_theory.shift_add_hom_comp_eq_to_hom₁₂_assoc {C : Type u} {A : Type u_1} [add_monoid A] (X : C) (i j i' j' : A) (h₁ : i = i') (h₂ : j = j') {X' : C} (f' : .obj .obj X) X') :
j).hom = j').hom f'
theorem category_theory.shift_add_hom_comp_eq_to_hom₁₂ {C : Type u} {A : Type u_1} [add_monoid A] (X : C) (i j i' j' : A) (h₁ : i = i') (h₂ : j = j') :
=
theorem category_theory.eq_to_hom_comp_shift_add_inv₁_assoc {C : Type u} {A : Type u_1} [add_monoid A] (X : C) (i i' j : A) (h : i = i') {X' : C} (f' : (i' + j)).obj X X') :
j).inv f' = j).inv
theorem category_theory.eq_to_hom_comp_shift_add_inv₁ {C : Type u} {A : Type u_1} [add_monoid A] (X : C) (i i' j : A) (h : i = i') :
theorem category_theory.eq_to_hom_comp_shift_add_inv₂_assoc {C : Type u} {A : Type u_1} [add_monoid A] (X : C) (i j j' : A) (h : j = j') {X' : C} (f' : (i + j')).obj X X') :
j').inv f' = j).inv
theorem category_theory.eq_to_hom_comp_shift_add_inv₂ {C : Type u} {A : Type u_1} [add_monoid A] (X : C) (i j j' : A) (h : j = j') :
theorem category_theory.eq_to_hom_comp_shift_add_inv₁₂ {C : Type u} {A : Type u_1} [add_monoid A] (X : C) (i j i' j' : A) (h₁ : i = i') (h₂ : j = j') :
=
theorem category_theory.eq_to_hom_comp_shift_add_inv₁₂_assoc {C : Type u} {A : Type u_1} [add_monoid A] (X : C) (i j i' j' : A) (h₁ : i = i') (h₂ : j = j') {X' : C} (f' : (i' + j')).obj X X') :
j').inv f' = j).inv
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
@[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) :
@[reducible]
noncomputable def category_theory.shift_functor_comp_shift_functor_neg (C : Type u) {A : Type u_1} [add_group A] (i : A) :

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

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

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

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

Shifting by n is a faithful functor.

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

Shifting by n is a full functor.

Equations
@[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) =
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) =
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_neg_hom_shift {C : Type u} {A : Type u_1} [add_group A] (n : A) (X : C) :
theorem category_theory.shift_shift_neg_inv_shift {C : Type u} {A : Type u_1} [add_group A] (n : A) (X : C) :
@[simp]
theorem category_theory.shift_shift_neg_shift_eq {C : Type u} {A : Type u_1} [add_group A] (n : A) (X : C) :
noncomputable def category_theory.shift_equiv (C : Type u) {A : Type u_1} [add_group A] (n : A) :
C C

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

Equations
@[simp]
theorem category_theory.shift_equiv_inverse (C : Type u) {A : Type u_1} [add_group A] (n : A) :
@[simp]
theorem category_theory.shift_equiv_functor (C : Type u) {A : Type u_1} [add_group A] (n : A) :
@[simp]
theorem category_theory.shift_equiv_counit_iso (C : Type u) {A : Type u_1} [add_group A] (n : A) :
@[simp]
theorem category_theory.shift_equiv_unit_iso (C : Type u) {A : Type u_1} [add_group A] (n : A) :
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_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.

Equations
@[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
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
@[nolint]
def category_theory.has_shift_of_fully_faithful_comm {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 ) (m : A) :
s m F

When we construct shifts on a subcategory from shifts on the ambient category, the inclusion functor intertwines the shifts.

Equations