mathlib documentation

category_theory.shift

Shift #

A shift on a category C indexed by a monoid A is 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-indexing 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 #

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} [category_theory.category C] [add_monoid A] (F : category_theory.monoidal_functor (category_theory.discrete A) (C C)) {i j i' j' : A} (h₁ : i = i') (h₂ : j = j') (X : C) :
@[simp]
theorem category_theory.eq_to_hom_μ_app_assoc {C : Type u} {A : Type u_1} [category_theory.category C] [add_monoid A] (F : category_theory.monoidal_functor (category_theory.discrete A) (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 (i' j')).obj X X') :
@[simp]
theorem category_theory.μ_inv_app_eq_to_hom {C : Type u} {A : Type u_1} [category_theory.category C] [add_monoid A] (F : category_theory.monoidal_functor (category_theory.discrete A) (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} [category_theory.category C] [add_monoid A] (F : category_theory.monoidal_functor (category_theory.discrete A) (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 i' F.to_lax_monoidal_functor.to_functor.obj j').obj X X') :
noncomputable def category_theory.add_neg_equiv {C : Type u} {A : Type u_1} [category_theory.category C] [add_group A] (F : category_theory.monoidal_functor (category_theory.discrete A) (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
@[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

Constructs a has_shift C A instance from shift_mk_core.

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

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

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

Shifting by zero is the identity functor.

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

theorem category_theory.eq_to_hom_comp_shift_add_inv₁₂_assoc {C : Type u} {A : Type u_1} [category_theory.category C] [add_monoid A] [category_theory.has_shift C A] (X : C) (i j i' j' : A) (h₁ : i = i') (h₂ : j = j') {X' : C} (f' : (category_theory.shift_functor C (i' + j')).obj X X') :
noncomputable def category_theory.shift_zero {C : Type u} (A : Type u_1) [category_theory.category C] [add_monoid A] [category_theory.has_shift C A] (X : C) :

Shifting by zero is the identity functor.

def category_theory.opaque_eq_to_iso {ι : Type u_2} {i j : ι} (h : i = j) :
i j

This definition is used instead of eq_to_iso so that the proof of i = j is visible to the simplifier

Equations
@[simp]
theorem category_theory.map_opaque_eq_to_iso_comp_app_assoc {C : Type u} [category_theory.category C] {ι : Type u_2} {i j k : ι} (F : category_theory.discrete ι C C) (h : i = j) (h' : j = k) (X : C) {X' : C} (f' : (F.obj k).obj X X') :
@[simp]
theorem category_theory.map_opaque_eq_to_iso_comp_app {C : Type u} [category_theory.category C] {ι : Type u_2} {i j k : ι} (F : category_theory.discrete ι C C) (h : i = j) (h' : j = k) (X : C) :

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

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

@[protected, instance]

Shifting by n is a faithful functor.

@[protected, instance]

Shifting by n is an essentially surjective functor.

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

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

noncomputable def category_theory.shift_neg_shift {C : Type u} {A : Type u_1} [category_theory.category C] [add_group A] [category_theory.has_shift C A] (X : C) (i : A) :

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

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

@[nolint]

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

Equations