Documentation

Mathlib.CategoryTheory.Shift.Basic

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 #

Implementation Notes #

[HasShift C A] is implemented using MonoidalFunctor (Discrete A) (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) [CategoryTheory.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.

Instances
    structure CategoryTheory.ShiftMkCore (C : Type u) (A : Type u_1) [CategoryTheory.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).

    Instances For
      theorem CategoryTheory.ShiftMkCore.assoc_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) (m₁ : A) (m₂ : A) (m₃ : A) (X : C) :
      @[simp]
      theorem CategoryTheory.hasShiftMk_shift_toLaxMonoidalFunctor_ε (C : Type u) (A : Type u_1) [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) :
      CategoryTheory.HasShift.shift = h.zero.inv

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

      Instances For

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

        Instances For

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

          Instances For

            shifting an object X by n is obtained by the notation X⟦n⟧

            Instances For

              shifting a morphism f by n is obtained by the notation f⟦n⟧'

              Instances For
                theorem CategoryTheory.shiftFunctorAdd'_assoc (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (a₃ : A) (a₁₂ : A) (a₂₃ : A) (a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) :
                theorem CategoryTheory.shiftFunctorAdd'_assoc_hom_app_assoc {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (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 : (CategoryTheory.shiftFunctor C a₃).obj ((CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a₁) (CategoryTheory.shiftFunctor C a₂)).obj X) Z) :
                CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (_ : a₁₂ + a₃ = a₁₂₃)).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (_ : a₁ + a₂₃ = a₁₂₃)).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app ((CategoryTheory.shiftFunctor C a₁).obj X)) h)
                theorem CategoryTheory.shiftFunctorAdd'_assoc_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (a₃ : A) (a₁₂ : A) (a₂₃ : A) (a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) :
                CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (_ : a₁₂ + a₃ = a₁₂₃)).hom.app X) ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (_ : a₁ + a₂₃ = a₁₂₃)).hom.app X) ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app ((CategoryTheory.shiftFunctor C a₁).obj X))
                theorem CategoryTheory.shiftFunctorAdd'_assoc_inv_app_assoc {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (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 : (CategoryTheory.shiftFunctor C a₁₂₃).obj X Z) :
                CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (_ : a₁₂ + a₃ = a₁₂₃)).inv.app X) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((CategoryTheory.shiftFunctor C a₁).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (_ : a₁ + a₂₃ = a₁₂₃)).inv.app X) h)
                theorem CategoryTheory.shiftFunctorAdd'_assoc_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (a₃ : A) (a₁₂ : A) (a₂₃ : A) (a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) :
                CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X)) ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (_ : a₁₂ + a₃ = a₁₂₃)).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((CategoryTheory.shiftFunctor C a₁).obj X)) ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (_ : a₁ + a₂₃ = a₁₂₃)).inv.app X)
                theorem CategoryTheory.shiftFunctorAdd_assoc_hom_app_assoc {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (a₃ : A) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C a₃).obj ((CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a₁) (CategoryTheory.shiftFunctor C a₂)).obj X) Z) :
                CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).hom.app X)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃)).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C a₂ a₃).hom.app ((CategoryTheory.shiftFunctor C a₁).obj X)) h)
                theorem CategoryTheory.shiftFunctorAdd_assoc_hom_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (a₃ : A) (X : C) :
                CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X) ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).hom.app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃)).hom.app X) ((CategoryTheory.shiftFunctorAdd C a₂ a₃).hom.app ((CategoryTheory.shiftFunctor C a₁).obj X))
                theorem CategoryTheory.shiftFunctorAdd_assoc_inv_app_assoc {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (a₃ : A) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C (a₁ + a₂ + a₃)).obj X Z) :
                CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).inv.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃).inv.app X) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C a₂ a₃).inv.app ((CategoryTheory.shiftFunctor C a₁).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃)).inv.app X) h)
                theorem CategoryTheory.shiftFunctorAdd_assoc_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a₁ : A) (a₂ : A) (a₃ : A) (X : C) :
                CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).inv.app X)) ((CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C a₂ a₃).inv.app ((CategoryTheory.shiftFunctor C a₁).obj X)) ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃)).inv.app X)
                @[simp]
                theorem CategoryTheory.HasShift.shift_obj_obj {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (n : A) (X : C) :
                (CategoryTheory.HasShift.shift.obj { as := n }).obj X = (CategoryTheory.shiftFunctor C n).obj X
                @[inline, reducible]

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

                Instances For
                  @[inline, reducible]

                  Shifting by zero is the identity functor.

                  Instances For

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

                    Instances For
                      @[simp]
                      theorem CategoryTheory.shiftEquiv'_unitIso (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (i : A) (j : A) (h : i + j = 0) :
                      @[simp]
                      theorem CategoryTheory.shiftEquiv'_counitIso (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (i : A) (j : A) (h : i + j = 0) :
                      def CategoryTheory.shiftEquiv' (C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (i : A) (j : A) (h : i + j = 0) :
                      C C

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

                      Instances For
                        @[inline, reducible]

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

                        Instances For

                          Shifting by n is an essentially surjective functor.

                          @[inline, reducible]

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

                          Instances For
                            @[inline, reducible]

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

                            Instances For
                              @[inline, reducible]

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

                              Instances For

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

                                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.

                                Instances For