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 #

source
@[simp]
theorem CategoryTheory.Functor.CommShift.isoZero_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] (X : C) :
(CategoryTheory.Functor.CommShift.isoZero F A).hom.app X = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorZero C A).hom.app X)) ((CategoryTheory.shiftFunctorZero D A).inv.app (F.obj X))
source
@[simp]
theorem CategoryTheory.Functor.CommShift.isoZero_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] (X : C) :
(CategoryTheory.Functor.CommShift.isoZero F A).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero D A).hom.app (F.obj X)) (F.map ((CategoryTheory.shiftFunctorZero C A).inv.app X))
source
noncomputable def CategoryTheory.Functor.CommShift.isoZero {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] :
(CategoryTheory.shiftFunctor C 0).comp F ≅ F.comp (CategoryTheory.shiftFunctor D 0)

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
    source
    @[simp]
    theorem CategoryTheory.Functor.CommShift.isoAdd'_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] {a : A} {b : A} {c : A} (h : a + b = c) (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) (X : C) :
    (CategoryTheory.Functor.CommShift.isoAdd' h e₁ e₂).hom.app X = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd' C a b c h).hom.app X)) (CategoryTheory.CategoryStruct.comp (e₂.hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.hom.app X)) ((CategoryTheory.shiftFunctorAdd' D a b c h).inv.app (F.obj X))))
    source
    @[simp]
    theorem CategoryTheory.Functor.CommShift.isoAdd'_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] {a : A} {b : A} {c : A} (h : a + b = c) (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) (X : C) :
    (CategoryTheory.Functor.CommShift.isoAdd' h e₁ e₂).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' D a b c h).hom.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.inv.app X)) (CategoryTheory.CategoryStruct.comp (e₂.inv.app ((CategoryTheory.shiftFunctor C a).obj X)) (F.map ((CategoryTheory.shiftFunctorAdd' C a b c h).inv.app X))))
    source
    noncomputable def CategoryTheory.Functor.CommShift.isoAdd' {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] {a : A} {b : A} {c : A} (h : a + b = c) (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) :
    (CategoryTheory.shiftFunctor C c).comp F ≅ F.comp (CategoryTheory.shiftFunctor D c)

    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
      source
      noncomputable def CategoryTheory.Functor.CommShift.isoAdd {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] {a : A} {b : A} (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) :
      (CategoryTheory.shiftFunctor C (a + b)).comp F ≅ F.comp (CategoryTheory.shiftFunctor D (a + b))

      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
        source
        @[simp]
        theorem CategoryTheory.Functor.CommShift.isoAdd_hom_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} {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {a : A} {b : A} (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) (X : C) :
        (CategoryTheory.Functor.CommShift.isoAdd e₁ e₂).hom.app X = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X)) (CategoryTheory.CategoryStruct.comp (e₂.hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.hom.app X)) ((CategoryTheory.shiftFunctorAdd D a b).inv.app (F.obj X))))
        source
        @[simp]
        theorem CategoryTheory.Functor.CommShift.isoAdd_inv_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} {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {a : A} {b : A} (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) (X : C) :
        (CategoryTheory.Functor.CommShift.isoAdd e₁ e₂).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).hom.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.inv.app X)) (CategoryTheory.CategoryStruct.comp (e₂.inv.app ((CategoryTheory.shiftFunctor C a).obj X)) (F.map ((CategoryTheory.shiftFunctorAdd C a b).inv.app X))))
        source
        class CategoryTheory.Functor.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) (A : Type u_4) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] :
        Type (max (max u_1 u_4) u_7)

        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
          source
          theorem CategoryTheory.Functor.CommShift.zero {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] [self : F.CommShift A] :
          CategoryTheory.Functor.CommShift.iso 0 = CategoryTheory.Functor.CommShift.isoZero F A
          source
          theorem CategoryTheory.Functor.CommShift.add {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] [self : F.CommShift A] (a : A) (b : A) :
          CategoryTheory.Functor.CommShift.iso (a + b) = CategoryTheory.Functor.CommShift.isoAdd (CategoryTheory.Functor.CommShift.iso a) (CategoryTheory.Functor.CommShift.iso b)
          source
          def CategoryTheory.Functor.commShiftIso {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] (a : A) :
          (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)

          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
            source
            @[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) :
            CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map f)) (CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).hom.app Y) h) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map f)) h)
            source
            @[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))
            source
            @[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) :
            CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map f)) (CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).inv.app Y) h) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).inv.app X) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map f)) h)
            source
            @[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))
            source
            theorem CategoryTheory.Functor.commShiftIso_zero {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] :
            F.commShiftIso 0 = CategoryTheory.Functor.CommShift.isoZero F A
            source
            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)
            source
            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)
            source
            instance CategoryTheory.Functor.CommShift.id (C : Type u_1) [CategoryTheory.Category.{u_6, u_1} C] {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] :
            (CategoryTheory.Functor.id C).CommShift A
            Equations
            • One or more equations did not get rendered due to their size.
            source
            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] {B : Type u_5} [AddCommMonoid B] [CategoryTheory.HasShift C B] [CategoryTheory.HasShift D B] (F : CategoryTheory.Functor C D) [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)))))