Documentation

Mathlib.CategoryTheory.Shift.CommShift

Functors which commute with shifts #

Let C and D be two categories equipped with shifts by an additive monoid A. In this file, we define the notion of functor F : C ⥤ D which "commutes" with these shifts. The associated type class is [F.CommShift A]. The data consists of commutation isomorphisms F.commShiftIso a : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a for all a : A which satisfy a compatibility with the addition and the zero. After this was formalised in Lean, it was found that this definition is exactly the definition which appears in Jean-Louis Verdier's thesis (I 1.2.3/1.2.4), although the language is different. (In Verdier's thesis, the shift is not given by a monoidal functor Discrete A ⥤ C ⥤ C, but by a fibred category C ⥤ BA, where BA is the category with one object, the endomorphisms of which identify to A. The choice of a cleavage for this fibered category gives the individual shift functors.)

References #

For any functor F : C ⥤ D, this is the obvious isomorphism shiftFunctor C (0 : A) ⋙ F ≅ F ⋙ shiftFunctor D (0 : A) deduced from the isomorphisms shiftFunctorZero on both categories C and D.

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

    If a functor F : C ⥤ D is equipped with "commutation isomorphisms" with the shifts by a and b, then there is a commutation isomorphism with the shift by c when a + b = c.

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

      If a functor F : C ⥤ D is equipped with "commutation isomorphisms" with the shifts by a and b, then there is a commutation isomorphism with the shift by a + b.

      Equations
      Instances For

        A functor F commutes with the shift by a monoid A if it is equipped with commutation isomorphisms with the shifts by all a : A, and these isomorphisms satisfy coherence properties with respect to 0 : A and the addition in A.

        Instances

          If a functor F commutes with the shift by A (i.e. [F.CommShift A]), then F.commShiftIso a is the given isomorphism shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.Functor.commShiftIso_hom_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] {X : C} {Y : C} (f : X Y) (a : A) {Z : D} (h : (CategoryTheory.shiftFunctor D a).obj (F.obj Y) Z) :
            @[simp]
            theorem CategoryTheory.Functor.commShiftIso_hom_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] {X : C} {Y : C} (f : X Y) (a : A) :
            CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map f)) ((F.commShiftIso a).hom.app Y) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).hom.app X) ((CategoryTheory.shiftFunctor D a).map (F.map f))
            @[simp]
            theorem CategoryTheory.Functor.commShiftIso_inv_naturality_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] {X : C} {Y : C} (f : X Y) (a : A) {Z : D} (h : F.obj ((CategoryTheory.shiftFunctor C a).obj Y) Z) :
            @[simp]
            theorem CategoryTheory.Functor.commShiftIso_inv_naturality {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] {X : C} {Y : C} (f : X Y) (a : A) :
            CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map f)) ((F.commShiftIso a).inv.app Y) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).inv.app X) (F.map ((CategoryTheory.shiftFunctor C a).map f))
            theorem CategoryTheory.Functor.commShiftIso_add {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] (a : A) (b : A) :
            F.commShiftIso (a + b) = CategoryTheory.Functor.CommShift.isoAdd (F.commShiftIso a) (F.commShiftIso b)
            theorem CategoryTheory.Functor.commShiftIso_add' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] {a : A} {b : A} {c : A} (h : a + b = c) :
            F.commShiftIso c = CategoryTheory.Functor.CommShift.isoAdd' h (F.commShiftIso a) (F.commShiftIso b)
            Equations
            • One or more equations did not get rendered due to their size.
            Equations
            • One or more equations did not get rendered due to their size.
            theorem CategoryTheory.Functor.commShiftIso_comp_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] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] [F.CommShift A] [G.CommShift A] (a : A) (X : C) :
            ((F.comp G).commShiftIso a).hom.app X = CategoryTheory.CategoryStruct.comp (G.map ((F.commShiftIso a).hom.app X)) ((G.commShiftIso a).hom.app (F.obj X))
            theorem CategoryTheory.Functor.commShiftIso_comp_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] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] [F.CommShift A] [G.CommShift A] (a : A) (X : C) :
            ((F.comp G).commShiftIso a).inv.app X = CategoryTheory.CategoryStruct.comp ((G.commShiftIso a).inv.app (F.obj X)) (G.map ((F.commShiftIso a).inv.app X))
            theorem CategoryTheory.Functor.map_shiftFunctorComm_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {B : Type u_5} [AddCommMonoid B] [CategoryTheory.HasShift C B] [CategoryTheory.HasShift D B] [F.CommShift B] (X : C) (a : B) (b : B) :
            F.map ((CategoryTheory.shiftFunctorComm C a b).hom.app X) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso b).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((F.commShiftIso a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm D a b).hom.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map ((F.commShiftIso b).inv.app X)) ((F.commShiftIso a).inv.app ((CategoryTheory.shiftFunctor C b).obj X)))))
            theorem CategoryTheory.Functor.map_shiftFunctorCompIsoId_hom_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] (X : C) (a : A) (b : A) (h : a + b = 0) {Z : D} (h : F.obj X Z) :
            @[simp]
            theorem CategoryTheory.Functor.map_shiftFunctorCompIsoId_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] (X : C) (a : A) (b : A) (h : a + b = 0) :
            F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).hom.app X) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso b).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((F.commShiftIso a).hom.app X)) ((CategoryTheory.shiftFunctorCompIsoId D a b h).hom.app (F.obj X)))
            @[simp]
            theorem CategoryTheory.Functor.map_shiftFunctorCompIsoId_inv_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] (X : C) (a : A) (b : A) (h : a + b = 0) :
            F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId D a b h).inv.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((F.commShiftIso a).inv.app X)) ((F.commShiftIso b).inv.app ((CategoryTheory.shiftFunctor C a).obj X)))
            class CategoryTheory.NatTrans.CommShift {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (τ : F₁ F₂) (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] :

            If τ : F₁ ⟶ F₂ is a natural transformation between two functors which commute with a shift by an additive monoid A, this typeclass asserts a compatibility of τ with these shifts.

            Instances
              theorem CategoryTheory.NatTrans.CommShift.comm_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (τ : F₁ F₂) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C) {Z : D} (h : (CategoryTheory.shiftFunctor D a).obj (F₂.obj X) Z) :
              CategoryTheory.CategoryStruct.comp ((F₁.commShiftIso a).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X)) h) = CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((F₂.commShiftIso a).hom.app X) h)
              theorem CategoryTheory.NatTrans.CommShift.comm_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (τ : F₁ F₂) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C) :
              CategoryTheory.CategoryStruct.comp ((F₁.commShiftIso a).hom.app X) ((CategoryTheory.shiftFunctor D a).map (τ.app X)) = CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X)) ((F₂.commShiftIso a).hom.app X)
              theorem CategoryTheory.NatTrans.CommShift.shift_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (τ : F₁ F₂) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C) {Z : D} (h : (CategoryTheory.shiftFunctor D a).obj (F₂.obj X) Z) :
              CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X)) h = CategoryTheory.CategoryStruct.comp ((F₁.commShiftIso a).inv.app X) (CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((F₂.commShiftIso a).hom.app X) h))
              theorem CategoryTheory.NatTrans.CommShift.shift_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (τ : F₁ F₂) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C) :
              (CategoryTheory.shiftFunctor D a).map (τ.app X) = CategoryTheory.CategoryStruct.comp ((F₁.commShiftIso a).inv.app X) (CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X)) ((F₂.commShiftIso a).hom.app X))
              theorem CategoryTheory.NatTrans.CommShift.app_shift_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (τ : F₁ F₂) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C) {Z : D} (h : F₂.obj ((CategoryTheory.shiftFunctor C a).obj X) Z) :
              CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X)) h = CategoryTheory.CategoryStruct.comp ((F₁.commShiftIso a).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X)) (CategoryTheory.CategoryStruct.comp ((F₂.commShiftIso a).inv.app X) h))
              theorem CategoryTheory.NatTrans.CommShift.app_shift {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (τ : F₁ F₂) {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] [F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C) :
              τ.app ((CategoryTheory.shiftFunctor C a).obj X) = CategoryTheory.CategoryStruct.comp ((F₁.commShiftIso a).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X)) ((F₂.commShiftIso a).inv.app X))

              If e : F ≅ G is an isomorphism of functors and if F commutes with the shift, then G also commutes with the shift.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem CategoryTheory.NatTrans.CommShift.verticalComposition {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] {F₁₂ : CategoryTheory.Functor C₁ C₂} {F₂₃ : CategoryTheory.Functor C₂ C₃} {F₁₃ : CategoryTheory.Functor C₁ C₃} (α : F₁₃ F₁₂.comp F₂₃) {G₁₂ : CategoryTheory.Functor D₁ D₂} {G₂₃ : CategoryTheory.Functor D₂ D₃} {G₁₃ : CategoryTheory.Functor D₁ D₃} (β : G₁₂.comp G₂₃ G₁₃) {L₁ : CategoryTheory.Functor C₁ D₁} {L₂ : CategoryTheory.Functor C₂ D₂} {L₃ : CategoryTheory.Functor C₃ D₃} (e₁₂ : F₁₂.comp L₂ L₁.comp G₁₂) (e₂₃ : F₂₃.comp L₃ L₂.comp G₂₃) (e₁₃ : F₁₃.comp L₃ L₁.comp G₁₃) (A : Type u_7) [AddMonoid A] [CategoryTheory.HasShift C₁ A] [CategoryTheory.HasShift C₂ A] [CategoryTheory.HasShift C₃ A] [CategoryTheory.HasShift D₁ A] [CategoryTheory.HasShift D₂ A] [CategoryTheory.HasShift D₃ A] [F₁₂.CommShift A] [F₂₃.CommShift A] [F₁₃.CommShift A] [CategoryTheory.NatTrans.CommShift α A] [G₁₂.CommShift A] [G₂₃.CommShift A] [G₁₃.CommShift A] [CategoryTheory.NatTrans.CommShift β A] [L₁.CommShift A] [L₂.CommShift A] [L₃.CommShift A] [CategoryTheory.NatTrans.CommShift e₁₂ A] [CategoryTheory.NatTrans.CommShift e₂₃ A] (h₁₃ : e₁₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight α L₃) (CategoryTheory.CategoryStruct.comp (F₁₂.associator F₂₃ L₃).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft F₁₂ e₂₃) (CategoryTheory.CategoryStruct.comp (F₁₂.associator L₂ G₂₃).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight e₁₂ G₂₃) (CategoryTheory.CategoryStruct.comp (L₁.associator G₁₂ G₂₃).hom (CategoryTheory.whiskerLeft L₁ β))))))) :

                Assume that we have a diagram of categories

                C₁ ⥤ D₁
                ‖     ‖
                v     v
                C₂ ⥤ D₂
                ‖     ‖
                v     v
                C₃ ⥤ D₃
                

                with functors F₁₂ : C₁ ⥤ C₂, F₂₃ : C₂ ⥤ C₃ and F₁₃ : C₁ ⥤ C₃ on the first column that are related by a natural transformation α : F₁₃ ⟶ F₁₂ ⋙ F₂₃ and similarly β : G₁₂ ⋙ G₂₃ ⟶ G₁₃ on the second column. Assume that we have natural transformations e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂ (top square), e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃ (bottom square), and e₁₃ : F₁₃ ⋙ L₃ ⟶ L₁ ⋙ G₁₃ (outer square), where the horizontal functors are denoted L₁, L₂ and L₃. Assume that e₁₃ is determined by the other natural transformations α, e₂₃, e₁₂ and β. Then, if all these categories are equipped with a shift by an additive monoid A, and all these functors commute with these shifts, then the natural transformation e₁₃ of the outer square commutes with the shift if all α, e₂₃, e₁₂ and β do.