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_hom_app_assoc {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] (self : CategoryTheory.ShiftMkCore C A) (m₁ : A) (m₂ : A) (m₃ : A) (X : C) {Z : C} (h : (self.F m₃).obj ((self.F m₂).obj ((self.F m₁).obj X)) Z) :
      CategoryTheory.CategoryStruct.comp ((self.add (m₁ + m₂) m₃).hom.app X) (CategoryTheory.CategoryStruct.comp ((self.F m₃).map ((self.add m₁ m₂).hom.app X)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ) (CategoryTheory.CategoryStruct.comp ((self.add m₁ (m₂ + m₃)).hom.app X) (CategoryTheory.CategoryStruct.comp ((self.add m₂ m₃).hom.app ((self.F m₁).obj X)) h))
      theorem CategoryTheory.ShiftMkCore.assoc_inv_app_assoc {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) {Z : C} (h : (h✝.F (m₁ + m₂ + m₃)).obj X Z) :
      CategoryTheory.CategoryStruct.comp ((h✝.F m₃).map ((h✝.add m₁ m₂).inv.app X)) (CategoryTheory.CategoryStruct.comp ((h✝.add (m₁ + m₂) m₃).inv.app X) h) = CategoryTheory.CategoryStruct.comp ((h✝.add m₂ m₃).inv.app ((h✝.F m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((h✝.add m₁ (m₂ + m₃)).inv.app X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ) h))
      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) :
      CategoryTheory.CategoryStruct.comp ((h.F m₃).map ((h.add m₁ m₂).inv.app X)) ((h.add (m₁ + m₂) m₃).inv.app X) = CategoryTheory.CategoryStruct.comp ((h.add m₂ m₃).inv.app ((h.F m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((h.add m₁ (m₂ + m₃)).inv.app X) (CategoryTheory.eqToHom ))
      theorem CategoryTheory.ShiftMkCore.zero_add_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) (n : A) (X : C) :
      (h.add 0 n).inv.app X = CategoryTheory.CategoryStruct.comp ((h.F n).map (h.zero.hom.app X)) (CategoryTheory.eqToHom )
      theorem CategoryTheory.ShiftMkCore.add_zero_inv_app {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) (n : A) (X : C) :
      (h.add n 0).inv.app X = CategoryTheory.CategoryStruct.comp (h.zero.hom.app ((h.F n).obj X)) (CategoryTheory.eqToHom )
      @[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
      @[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) (m : CategoryTheory.Discrete A) (n : CategoryTheory.Discrete A) :
      CategoryTheory.HasShift.shift m n = (h.add m.as n.as).inv

      Constructs a HasShift C A instance from ShiftMkCore.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

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

        Equations
        Instances For

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

          Equations
          Instances For

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

            Equations
            Instances For

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

              Equations
              Instances For

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  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.shiftFunctor C a₂).obj ((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₂ a₁₂ h₁₂).hom.app X)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C 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₁₂₃ ).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₁₂₃ ).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₁₂₃ ).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₁₂₃ ).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₁₂₃ ).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₁₂₃ ).inv.app X)
                    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₃) ).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) :
                    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₃) ).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.

                    Equations
                    Instances For
                      @[inline, reducible]

                      Shifting by zero is the identity functor.

                      Equations
                      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) :
                        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.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[inline, reducible]

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

                          Equations
                          Instances For

                            Shifting by n is an essentially surjective functor.

                            Equations
                            • =
                            @[inline, reducible]

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

                            Equations
                            Instances For
                              @[inline, reducible]

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

                              Equations
                              Instances For
                                @[inline, reducible]

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

                                Equations
                                Instances For

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

                                  auxiliary definition for hasShiftOfFullyFaithful

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    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.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For