Documentation

Mathlib.CategoryTheory.Shift.SingleFunctors

Functors from a category to a category with a shift #

Given a category C, and a category D equipped with a shift by a monoid A, we define a structure SingleFunctors C D A which contains the data of functors functor a : C ⥤ D for all a : A and isomorphisms shiftIso n a a' h : functor a' ⋙ shiftFunctor D n ≅ functor a whenever n + a = a'. These isomorphisms should satisfy certain compatibilities with respect to the shift on D.

This notion is similar to Functor.ShiftSequence which can be used in order to attach shifted versions of a homological functor D ⥤ C with D a triangulated category and C an abelian category. However, the definition SingleFunctors is for functors in the other direction: it is meant to ease the formalization of the compatibilities with shifts of the functors C ⥤ CochainComplex C ℤ (or C ⥤ DerivedCategory C (TODO)) which sends an object X : C to a complex where X sits in a single degree.

structure CategoryTheory.SingleFunctors (C : Type u_1) (D : Type u_2) [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift D A] :
Type (max (max (max (max u_1 u_2) u_5) u_6) u_7)

The type of families of functors A → C ⥤ D which are compatible with the shift by A on the category D.

Instances For
    theorem CategoryTheory.SingleFunctors.shiftIso_add {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (self : CategoryTheory.SingleFunctors C D A) (n : A) (m : A) (a : A) (a' : A) (a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') :
    self.shiftIso (m + n) a a'' = CategoryTheory.isoWhiskerLeft (self.functor a'') (CategoryTheory.shiftFunctorAdd D m n) ≪≫ ((self.functor a'').associator (CategoryTheory.shiftFunctor D m) (CategoryTheory.shiftFunctor D n)).symm ≪≫ CategoryTheory.isoWhiskerRight (self.shiftIso m a' a'' ha'') (CategoryTheory.shiftFunctor D n) ≪≫ self.shiftIso n a a' ha'

    shiftIso (m + n) is determined by shiftIso m and shiftIso n.

    theorem CategoryTheory.SingleFunctors.shiftIso_add_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n : A) (m : A) (a : A) (a' : A) (a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
    (F.shiftIso (m + n) a a'' ).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D m n).hom.app ((F.functor a'').obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X)) ((F.shiftIso n a a' ha').hom.app X))
    theorem CategoryTheory.SingleFunctors.shiftIso_add_inv_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n : A) (m : A) (a : A) (a' : A) (a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
    (F.shiftIso (m + n) a a'' ).inv.app X = CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').inv.app X)) ((CategoryTheory.shiftFunctorAdd D m n).inv.app ((F.functor a'').obj X)))
    theorem CategoryTheory.SingleFunctors.shiftIso_add' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n : A) (m : A) (mn : A) (hnm : m + n = mn) (a : A) (a' : A) (a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') :
    F.shiftIso mn a a'' = CategoryTheory.isoWhiskerLeft (F.functor a'') (CategoryTheory.shiftFunctorAdd' D m n mn hnm) ≪≫ ((F.functor a'').associator (CategoryTheory.shiftFunctor D m) (CategoryTheory.shiftFunctor D n)).symm ≪≫ CategoryTheory.isoWhiskerRight (F.shiftIso m a' a'' ha'') (CategoryTheory.shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'
    theorem CategoryTheory.SingleFunctors.shiftIso_add'_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n : A) (m : A) (mn : A) (hnm : m + n = mn) (a : A) (a' : A) (a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
    (F.shiftIso mn a a'' ).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' D m n mn hnm).hom.app ((F.functor a'').obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X)) ((F.shiftIso n a a' ha').hom.app X))
    theorem CategoryTheory.SingleFunctors.shiftIso_add'_inv_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n : A) (m : A) (mn : A) (hnm : m + n = mn) (a : A) (a' : A) (a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
    (F.shiftIso mn a a'' ).inv.app X = CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').inv.app X)) ((CategoryTheory.shiftFunctorAdd' D m n mn hnm).inv.app ((F.functor a'').obj X)))
    @[simp]
    theorem CategoryTheory.SingleFunctors.shiftIso_zero_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (a : A) (X : C) :
    (F.shiftIso 0 a a ).hom.app X = (CategoryTheory.shiftFunctorZero D A).hom.app ((F.functor a).obj X)
    @[simp]
    theorem CategoryTheory.SingleFunctors.shiftIso_zero_inv_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (a : A) (X : C) :
    (F.shiftIso 0 a a ).inv.app X = (CategoryTheory.shiftFunctorZero D A).inv.app ((F.functor a).toPrefunctor.1 X)
    theorem CategoryTheory.SingleFunctors.Hom.ext {C : Type u_1} {D : Type u_2} :
    ∀ {inst : CategoryTheory.Category.{u_6, u_1} C} {inst_1 : CategoryTheory.Category.{u_7, u_2} D} {A : Type u_5} {inst_2 : AddMonoid A} {inst_3 : CategoryTheory.HasShift D A} {F G : CategoryTheory.SingleFunctors C D A} {x y : F.Hom G}, x.hom = y.homx = y
    theorem CategoryTheory.SingleFunctors.Hom.ext_iff {C : Type u_1} {D : Type u_2} :
    ∀ {inst : CategoryTheory.Category.{u_6, u_1} C} {inst_1 : CategoryTheory.Category.{u_7, u_2} D} {A : Type u_5} {inst_2 : AddMonoid A} {inst_3 : CategoryTheory.HasShift D A} {F G : CategoryTheory.SingleFunctors C D A} {x y : F.Hom G}, x = y x.hom = y.hom

    The morphisms in the category SingleFunctors C D A

    Instances For
      theorem CategoryTheory.SingleFunctors.Hom.comm {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.SingleFunctors C D A} {G : CategoryTheory.SingleFunctors C D A} (self : F.Hom G) (n : A) (a : A) (a' : A) (ha' : n + a = a') :
      CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (self.hom a) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (self.hom a') (CategoryTheory.shiftFunctor D n)) (G.shiftIso n a a' ha').hom

      The identity morphism in SingleFunctors C D A.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.SingleFunctors.Hom.comp_hom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.SingleFunctors C D A} {G : CategoryTheory.SingleFunctors C D A} {H : CategoryTheory.SingleFunctors C D A} (α : F.Hom G) (β : G.Hom H) (a : A) :
        (α.comp β).hom a = CategoryTheory.CategoryStruct.comp (α.hom a) (β.hom a)

        The composition of morphisms in SingleFunctors C D A.

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.SingleFunctors.isoMk_inv_hom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.SingleFunctors C D A} {G : CategoryTheory.SingleFunctors C D A} (iso : (a : A) → F.functor a G.functor a) (comm : ∀ (n a a' : A) (ha' : n + a = a'), CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (iso a).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (iso a').hom (CategoryTheory.shiftFunctor D n)) (G.shiftIso n a a' ha').hom) (a : A) :
          (CategoryTheory.SingleFunctors.isoMk iso comm).inv.hom a = (iso a).inv
          @[simp]
          theorem CategoryTheory.SingleFunctors.isoMk_hom_hom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.SingleFunctors C D A} {G : CategoryTheory.SingleFunctors C D A} (iso : (a : A) → F.functor a G.functor a) (comm : ∀ (n a a' : A) (ha' : n + a = a'), CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (iso a).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (iso a').hom (CategoryTheory.shiftFunctor D n)) (G.shiftIso n a a' ha').hom) (a : A) :
          (CategoryTheory.SingleFunctors.isoMk iso comm).hom.hom a = (iso a).hom
          def CategoryTheory.SingleFunctors.isoMk {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.SingleFunctors C D A} {G : CategoryTheory.SingleFunctors C D A} (iso : (a : A) → F.functor a G.functor a) (comm : ∀ (n a a' : A) (ha' : n + a = a'), CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (iso a).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (iso a').hom (CategoryTheory.shiftFunctor D n)) (G.shiftIso n a a' ha').hom) :
          F G

          Construct an isomorphism in SingleFunctors C D A by giving level-wise isomorphisms and checking compatibility only in the forward direction.

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

            The evaluation SingleFunctors C D A ⥤ C ⥤ D for some a : A.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem CategoryTheory.SingleFunctors.hom_inv_id_hom_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.SingleFunctors C D A} {G : CategoryTheory.SingleFunctors C D A} (e : F G) (n : A) (X : C) {Z : D} (h : (F.functor n).obj X Z) :
              CategoryTheory.CategoryStruct.comp ((e.hom.hom n).app X) (CategoryTheory.CategoryStruct.comp ((e.inv.hom n).app X) h) = h
              @[simp]
              theorem CategoryTheory.SingleFunctors.inv_hom_id_hom_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.SingleFunctors C D A} {G : CategoryTheory.SingleFunctors C D A} (e : F G) (n : A) (X : C) {Z : D} (h : (G.functor n).obj X Z) :
              CategoryTheory.CategoryStruct.comp ((e.inv.hom n).app X) (CategoryTheory.CategoryStruct.comp ((e.hom.hom n).app X) h) = h
              @[simp]
              theorem CategoryTheory.SingleFunctors.postcomp_functor {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) [G.CommShift A] (a : A) :
              (F.postcomp G).functor a = (F.functor a).comp G
              @[simp]
              theorem CategoryTheory.SingleFunctors.postcomp_shiftIso_inv_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) [G.CommShift A] (n : A) (a : A) (a' : A) (ha' : n + a = a') (X : C) :
              ((F.postcomp G).shiftIso n a a' ha').inv.app X = CategoryTheory.CategoryStruct.comp (G.map ((F.shiftIso n a a' ha').inv.app X)) ((G.commShiftIso n).hom.app ((F.functor a').obj X))
              @[simp]
              theorem CategoryTheory.SingleFunctors.postcomp_shiftIso_hom_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) [G.CommShift A] (n : A) (a : A) (a' : A) (ha' : n + a = a') (X : C) :
              ((F.postcomp G).shiftIso n a a' ha').hom.app X = CategoryTheory.CategoryStruct.comp ((G.commShiftIso n).inv.app ((F.functor a').obj X)) (G.map ((F.shiftIso n a a' ha').hom.app X))

              Given F : SingleFunctors C D A, and a functor G : D ⥤ E which commutes with the shift by A, this is the "composition" of F and G in SingleFunctors C E A.

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

                The functor SingleFunctors C D A ⥤ SingleFunctors C E A given by the postcomposition by a functor G : D ⥤ E which commutes with the shift.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CategoryTheory.SingleFunctors.postcompPostcompIso_hom_hom_app {C : Type u_1} {D : Type u_2} {E : Type u_3} {E' : Type u_4} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] [CategoryTheory.Category.{u_9, u_4} E'] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] [CategoryTheory.HasShift E' A] (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) (G' : CategoryTheory.Functor E E') [G.CommShift A] [G'.CommShift A] (a : A) :
                  ∀ (x : C), ((F.postcompPostcompIso G G').hom.hom a).app x = CategoryTheory.CategoryStruct.id (G'.obj (G.obj ((F.functor a).obj x)))
                  @[simp]
                  theorem CategoryTheory.SingleFunctors.postcompPostcompIso_inv_hom_app {C : Type u_1} {D : Type u_2} {E : Type u_3} {E' : Type u_4} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] [CategoryTheory.Category.{u_9, u_4} E'] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] [CategoryTheory.HasShift E' A] (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) (G' : CategoryTheory.Functor E E') [G.CommShift A] [G'.CommShift A] (a : A) :
                  ∀ (x : C), ((F.postcompPostcompIso G G').inv.hom a).app x = CategoryTheory.CategoryStruct.id (G'.obj (G.obj ((F.functor a).obj x)))

                  The canonical isomorphism (F.postcomp G).postcomp G' ≅ F.postcomp (G ⋙ G').

                  Equations
                  Instances For
                    @[simp]
                    theorem CategoryTheory.SingleFunctors.postcompIsoOfIso_inv_hom_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] (F : CategoryTheory.SingleFunctors C D A) {G : CategoryTheory.Functor D E} {G' : CategoryTheory.Functor D E} (e : G G') [G.CommShift A] [G'.CommShift A] [CategoryTheory.NatTrans.CommShift e.hom A] (a : A) (X : C) :
                    ((F.postcompIsoOfIso e).inv.hom a).app X = e.inv.app ((F.functor a).obj X)
                    @[simp]
                    theorem CategoryTheory.SingleFunctors.postcompIsoOfIso_hom_hom_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] (F : CategoryTheory.SingleFunctors C D A) {G : CategoryTheory.Functor D E} {G' : CategoryTheory.Functor D E} (e : G G') [G.CommShift A] [G'.CommShift A] [CategoryTheory.NatTrans.CommShift e.hom A] (a : A) (X : C) :
                    ((F.postcompIsoOfIso e).hom.hom a).app X = e.hom.app ((F.functor a).obj X)

                    The isomorphism F.postcomp G ≅ F.postcomp G' induced by an isomorphism e : G ≅ G' which commutes with the shift.

                    Equations
                    Instances For