Documentation

Mathlib.CategoryTheory.Abelian.RightDerived

Right-derived functors #

We define the right-derived functors F.rightDerived n : C ⥤ D for any additive functor F out of a category with injective resolutions.

We first define a functor F.rightDerivedToHomotopyCategory : C ⥤ HomotopyCategory D (ComplexShape.up ℕ) which is injectiveResolutions C ⋙ F.mapHomotopyCategory _. We show that if X : C and I : InjectiveResolution X, then F.rightDerivedToHomotopyCategory.obj X identifies to the image in the homotopy category of the functor F applied objectwise to I.cocomplex (this isomorphism is I.isoRightDerivedToHomotopyCategoryObj F).

Then, the right-derived functors F.rightDerived n : C ⥤ D are obtained by composing F.rightDerivedToHomotopyCategory with the homology functors on the homotopy category.

Similarly we define natural transformations between right-derived functors coming from natural transformations between the original additive functors, and show how to compute the components.

Main results #

TODO #

When F : C ⥤ D is an additive functor, this is the functor C ⥤ HomotopyCategory D (ComplexShape.up ℕ) which sends X : C to F applied to an injective resolution of X.

Equations
Instances For

    If I : InjectiveResolution Z and F : C ⥤ D is an additive functor, this is an isomorphism between F.rightDerivedToHomotopyCategory.obj X and the complex obtained by applying F to I.cocomplex.

    Equations
    Instances For
      theorem CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.f 0)) (F : CategoryTheory.Functor C D) [F.Additive] {Z : HomotopyCategory D (ComplexShape.up )} (h : (HomotopyCategory.quotient D (ComplexShape.up )).obj ((F.mapHomologicalComplex (ComplexShape.up )).obj J.cocomplex) Z) :
      CategoryTheory.CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f) (CategoryTheory.CategoryStruct.comp (J.isoRightDerivedToHomotopyCategoryObj F).hom h) = CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.up )).map ((F.mapHomologicalComplex (ComplexShape.up )).map φ)) h)
      theorem CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.f 0)) (F : CategoryTheory.Functor C D) [F.Additive] :
      CategoryTheory.CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f) (J.isoRightDerivedToHomotopyCategoryObj F).hom = CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).hom (((F.mapHomologicalComplex (ComplexShape.up )).comp (HomotopyCategory.quotient D (ComplexShape.up ))).map φ)
      theorem CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.f 0)) (F : CategoryTheory.Functor C D) [F.Additive] {Z : HomotopyCategory D (ComplexShape.up )} (h : F.rightDerivedToHomotopyCategory.obj Y Z) :
      CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).inv (CategoryTheory.CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f) h) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.up )).map ((F.mapHomologicalComplex (ComplexShape.up )).map φ)) (CategoryTheory.CategoryStruct.comp (J.isoRightDerivedToHomotopyCategoryObj F).inv h)
      theorem CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.f 0)) (F : CategoryTheory.Functor C D) [F.Additive] :
      CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).inv (F.rightDerivedToHomotopyCategory.map f) = CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up )).comp (HomotopyCategory.quotient D (ComplexShape.up ))).map φ) (J.isoRightDerivedToHomotopyCategoryObj F).inv

      The right derived functors of an additive functor.

      Equations
      Instances For

        We can compute a right derived functor using a chosen injective resolution.

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

          We can compute a right derived functor on a morphism using a descent of that morphism to a cochain map between chosen injective resolutions.

          noncomputable def CategoryTheory.NatTrans.rightDerivedToHomotopyCategory {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (α : F G) :
          F.rightDerivedToHomotopyCategory G.rightDerivedToHomotopyCategory

          The natural transformation F.rightDerivedToHomotopyCategory ⟶ G.rightDerivedToHomotopyCategory induced by a natural transformation F ⟶ G between additive functors.

          Equations
          Instances For
            noncomputable def CategoryTheory.NatTrans.rightDerived {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (α : F G) (n : ) :
            F.rightDerived n G.rightDerived n

            The natural transformation between right-derived functors induced by a natural transformation.

            Equations
            Instances For

              A component of the natural transformation between right-derived functors can be computed using a chosen injective resolution.

              noncomputable def CategoryTheory.InjectiveResolution.toRightDerivedZero' {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] {X : C} (P : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [F.Additive] :
              F.obj X ((F.mapHomologicalComplex (ComplexShape.up )).obj P.cocomplex).cycles 0

              If P : InjectiveResolution X and F is an additive functor, this is the canonical morphism from F.obj X to the cycles in degree 0 of (F.mapHomologicalComplex _).obj P.cocomplex.

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] {X : C} (P : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [F.Additive] {Z : D} (h : ((F.mapHomologicalComplex (ComplexShape.up )).obj P.cocomplex).X 0 Z) :
                CategoryTheory.CategoryStruct.comp (P.toRightDerivedZero' F) (CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up )).obj P.cocomplex).iCycles 0) h) = CategoryTheory.CategoryStruct.comp (F.map (P.f 0)) h
                @[simp]
                theorem CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] {X : C} (P : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [F.Additive] :
                CategoryTheory.CategoryStruct.comp (P.toRightDerivedZero' F) (((F.mapHomologicalComplex (ComplexShape.up )).obj P.cocomplex).iCycles 0) = F.map (P.f 0)
                theorem CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X Y) (P : CategoryTheory.InjectiveResolution X) (Q : CategoryTheory.InjectiveResolution Y) (φ : P.cocomplex Q.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (P.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (Q.f 0)) (F : CategoryTheory.Functor C D) [F.Additive] {Z : D} (h : ((F.mapHomologicalComplex (ComplexShape.up )).obj Q.cocomplex).cycles 0 Z) :

                The natural transformation F ⟶ F.rightDerived 0.

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

                  The canonical isomorphism F.rightDerived 0 ≅ F when F is left exact (i.e. preserves finite limits).

                  Equations
                  Instances For