Documentation

Mathlib.CategoryTheory.Functor.Derived.RightDerivedCommShift

The right derived functor commutes with the shift #

Let L : C ⥤ H be a localization functor with respect to W : MorphismProperty C. Let F : C ⥤ D, RF : H ⥤ D and α : F ⟶ L ⋙ RF be a natural transformation which makes RF the right derived functor of F. We assume that C, D and H are equipped with shifts by an additive group A, that L and F commute with these shifts, and that W is compatible with the shift. Under these assumptions, we show that RF commutes with shifts, and that for this structure, the natural transformation α is compatible with the shifts.

source
def CategoryTheory.Functor.IsRightDerivedFunctor.precomposeShiftNatTrans {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H] (RF : Functor H D) {F : Functor C D} {L : Functor C H} (α : F ⟶ L.comp RF) {A : Type u_4} [AddGroup A] [HasShift C A] [HasShift H A] [L.CommShift A] (a : A) :
(shiftFunctor C a).comp F ⟶ L.comp ((shiftFunctor H a).comp RF)

The natural transformation shiftFunctor C a ⋙ F ⟶ L ⋙ shiftFunctor H a ⋙ RF deduced from α : F ⟶ L ⋙ RF when L commutes with the shift.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Functor.IsRightDerivedFunctor.precomposeShiftNatTrans_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H] (RF : Functor H D) {F : Functor C D} {L : Functor C H} (α : F ⟶ L.comp RF) {A : Type u_4} [AddGroup A] [HasShift C A] [HasShift H A] [L.CommShift A] (a : A) (X : C) :
    (precomposeShiftNatTrans RF α a).app X = CategoryStruct.comp (α.app ((shiftFunctor C a).obj X)) (RF.map ((commShiftIso L a).hom.app X))
    source
    def CategoryTheory.Functor.IsRightDerivedFunctor.postcomposeShiftNatTrans {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H] (RF : Functor H D) {F : Functor C D} {L : Functor C H} (α : F ⟶ L.comp RF) {A : Type u_4} [AddGroup A] [HasShift D A] (a : A) :
    F.comp (shiftFunctor D a) ⟶ L.comp (RF.comp (shiftFunctor D a))

    The natural transformation F ⋙ shiftFunctor D a ⟶ L ⋙ RF ⋙ shiftFunctor D a deduced from α : F ⟶ L ⋙ RF when L commutes with the shift.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Functor.IsRightDerivedFunctor.postcomposeShiftNatTrans_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H] (RF : Functor H D) {F : Functor C D} {L : Functor C H} (α : F ⟶ L.comp RF) {A : Type u_4} [AddGroup A] [HasShift D A] (a : A) (X : C) :
      (postcomposeShiftNatTrans RF α a).app X = (shiftFunctor D a).map (α.app X)
      source
      instance CategoryTheory.Functor.IsRightDerivedFunctor.instCompShiftFunctorPrecomposeShiftNatTrans {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H] (RF : Functor H D) {F : Functor C D} {L : Functor C H} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] {A : Type u_4} [AddGroup A] [HasShift C A] [HasShift H A] [W.IsCompatibleWithShift A] [L.CommShift A] (a : A) :
      ((shiftFunctor H a).comp RF).IsRightDerivedFunctor (precomposeShiftNatTrans RF α a) W
      source
      instance CategoryTheory.Functor.IsRightDerivedFunctor.instCompShiftFunctorPostcomposeShiftNatTrans {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H] (RF : Functor H D) {F : Functor C D} {L : Functor C H} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] {A : Type u_4} [AddGroup A] [HasShift D A] (a : A) :
      (RF.comp (shiftFunctor D a)).IsRightDerivedFunctor (postcomposeShiftNatTrans RF α a) W
      source
      @[implicit_reducible]
      noncomputable def CategoryTheory.Functor.IsRightDerivedFunctor.commShift {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H] (RF : Functor H D) {F : Functor C D} {L : Functor C H} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (A : Type u_4) [AddGroup A] [HasShift C A] [HasShift D A] [HasShift H A] [W.IsCompatibleWithShift A] [F.CommShift A] [L.CommShift A] :
      RF.CommShift A

      The right derived functor commutes with the shift.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Functor.IsRightDerivedFunctor.comp_map_commShiftIso_hom_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H] (RF : Functor H D) {F : Functor C D} {L : Functor C H} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (A : Type u_4) [AddGroup A] [HasShift C A] [HasShift D A] [HasShift H A] [W.IsCompatibleWithShift A] [F.CommShift A] [L.CommShift A] (a : A) (X : C) :
        CategoryStruct.comp (α.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp (RF.map ((commShiftIso L a).hom.app X)) ((commShiftIso RF a).hom.app (L.obj X))) = CategoryStruct.comp ((commShiftIso F a).hom.app X) ((shiftFunctor D a).map (α.app X))
        source
        @[simp]
        theorem CategoryTheory.Functor.IsRightDerivedFunctor.comp_map_commShiftIso_hom_app_assoc {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H] (RF : Functor H D) {F : Functor C D} {L : Functor C H} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (A : Type u_4) [AddGroup A] [HasShift C A] [HasShift D A] [HasShift H A] [W.IsCompatibleWithShift A] [F.CommShift A] [L.CommShift A] (a : A) (X : C) {Z : D} (h : (shiftFunctor D a).obj (RF.obj (L.obj X)) ⟶ Z) :
        CategoryStruct.comp (α.app ((shiftFunctor C a).obj X)) (CategoryStruct.comp (RF.map ((commShiftIso L a).hom.app X)) (CategoryStruct.comp ((commShiftIso RF a).hom.app (L.obj X)) h)) = CategoryStruct.comp ((commShiftIso F a).hom.app X) (CategoryStruct.comp ((shiftFunctor D a).map (α.app X)) h)
        source
        instance CategoryTheory.Functor.IsRightDerivedFunctor.natTrans_commShift {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H] (RF : Functor H D) {F : Functor C D} {L : Functor C H} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (A : Type u_4) [AddGroup A] [HasShift C A] [HasShift D A] [HasShift H A] [W.IsCompatibleWithShift A] [F.CommShift A] [L.CommShift A] :
        NatTrans.CommShift α A
        source
        @[instance_reducible]
        noncomputable instance CategoryTheory.Functor.IsRightDerivedFunctor.instCommShiftTotalRightDerived {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H] {F : Functor C D} {L : Functor C H} (W : MorphismProperty C) [L.IsLocalization W] (A : Type u_4) [AddGroup A] [HasShift C A] [HasShift D A] [HasShift H A] [W.IsCompatibleWithShift A] [F.CommShift A] [L.CommShift A] [F.HasRightDerivedFunctor W] :
        (F.totalRightDerived L W).CommShift A
        Equations