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.

The definition is

injectiveResolutions C ⋙ F.mapHomotopyCategory _ ⋙ HomotopyCategory.homologyFunctor D _ n

that is, we pick an injective resolution (thought of as an object of the homotopy category), we apply F objectwise, and compute n-th homology.

We show that these right-derived functors can be calculated on objects using any choice of injective resolution, and on morphisms by any choice of lift to a cochain map between chosen injective resolutions.

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 #

Now, we assume PreservesFiniteLimits F, then

@[simp]
theorem CategoryTheory.Functor.rightDerivedObjInjectiveZero_hom {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) [CategoryTheory.Functor.Additive F] (X : C) [CategoryTheory.Injective X] :
(CategoryTheory.Functor.rightDerivedObjInjectiveZero F X).hom = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctor D (ComplexShape.up ) 0).map ((HomotopyCategory.quotient D (ComplexShape.up )).map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up )).map (CategoryTheory.InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (CategoryTheory.InjectiveResolution X))) (CategoryTheory.InjectiveResolution.self X)).hom))) (CategoryTheory.CategoryStruct.comp (homology.map (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up )).obj (CategoryTheory.InjectiveResolution.self X).cocomplex) 0) (HomologicalComplex.dFrom ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up )).obj (CategoryTheory.InjectiveResolution.self X).cocomplex) 0) = 0) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo ((CochainComplex.single₀ D).obj (F.obj X)) 0) (HomologicalComplex.dFrom ((CochainComplex.single₀ D).obj (F.obj X)) 0) = 0) (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).hom.app X) 0) (HomologicalComplex.Hom.sqFrom ((CochainComplex.single₀MapHomologicalComplex F).hom.app X) 0) (_ : (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).hom.app X) 0).right = (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).hom.app X) 0).right)) ((CochainComplex.homologyFunctor0Single₀ D).hom.app (F.obj X)))
@[simp]
theorem CategoryTheory.Functor.rightDerivedObjInjectiveZero_inv {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) [CategoryTheory.Functor.Additive F] (X : C) [CategoryTheory.Injective X] :
(CategoryTheory.Functor.rightDerivedObjInjectiveZero F X).inv = CategoryTheory.CategoryStruct.comp ((CochainComplex.homologyFunctor0Single₀ D).inv.app (F.obj X)) (CategoryTheory.CategoryStruct.comp (homology.map (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo ((CochainComplex.single₀ D).obj (F.obj X)) 0) (HomologicalComplex.dFrom ((CochainComplex.single₀ D).obj (F.obj X)) 0) = 0) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up )).obj (CategoryTheory.InjectiveResolution.self X).cocomplex) 0) (HomologicalComplex.dFrom ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up )).obj (CategoryTheory.InjectiveResolution.self X).cocomplex) 0) = 0) (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) 0) (HomologicalComplex.Hom.sqFrom ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) 0) (_ : (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) 0).right = (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) 0).right)) ((HomotopyCategory.homologyFunctor D (ComplexShape.up ) 0).map ((HomotopyCategory.quotient D (ComplexShape.up )).map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up )).map (CategoryTheory.InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (CategoryTheory.InjectiveResolution X))) (CategoryTheory.InjectiveResolution.self X)).inv))))
@[simp]
theorem CategoryTheory.Functor.rightDerivedObjInjectiveSucc_inv {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) [CategoryTheory.Functor.Additive F] (n : ) (X : C) [CategoryTheory.Injective X] :
(CategoryTheory.Functor.rightDerivedObjInjectiveSucc F n X).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsZero.isoZero (_ : CategoryTheory.Limits.IsZero (0.obj (F.obj X)))).inv (CategoryTheory.CategoryStruct.comp ((CochainComplex.homologyFunctorSuccSingle₀ D n).inv.app (F.obj X)) (CategoryTheory.CategoryStruct.comp (homology.map (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo ((CochainComplex.single₀ D).obj (F.obj X)) (n + 1)) (HomologicalComplex.dFrom ((CochainComplex.single₀ D).obj (F.obj X)) (n + 1)) = 0) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up )).obj (CategoryTheory.InjectiveResolution.self X).cocomplex) (n + 1)) (HomologicalComplex.dFrom ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up )).obj (CategoryTheory.InjectiveResolution.self X).cocomplex) (n + 1)) = 0) (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) (n + 1)) (HomologicalComplex.Hom.sqFrom ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) (n + 1)) (_ : (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) (n + 1)).right = (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) (n + 1)).right)) ((HomotopyCategory.homologyFunctor D (ComplexShape.up ) (n + 1)).map ((HomotopyCategory.quotient D (ComplexShape.up )).map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up )).map (CategoryTheory.InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (CategoryTheory.InjectiveResolution X))) (CategoryTheory.InjectiveResolution.self X)).inv)))))