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 #
Functor.isZero_rightDerived_obj_injective_succ: injective objects have no higher right derived functor.NatTrans.rightDerived: the natural transformation between right derived functors induced by a natural transformation.Functor.toRightDerivedZero: the natural transformationF ⟶ F.rightDerived 0, which is an isomorphism whenFis left exact (i.e. preserves finite limits), see alsoFunctor.rightDerivedZeroIsoSelf.
TODO #
- refactor
Functor.rightDerived(andFunctor.leftDerived) when the necessary material enters mathlib: derived categories, injective/projective derivability structures, existence of derived functors from derivability structures. Eventually, we shall get a right derived functorF.rightDerivedFunctorPlus : DerivedCategory.Plus C ⥤ DerivedCategory.Plus D, andF.rightDerivedshall be redefined usingF.rightDerivedFunctorPlus.
noncomputable def
CategoryTheory.Functor.rightDerivedToHomotopyCategory
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
:
Functor C (HomotopyCategory D (ComplexShape.up ℕ))
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.
Instances For
noncomputable def
CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{X : C}
(I : InjectiveResolution X)
(F : Functor C D)
[F.Additive]
:
F.rightDerivedToHomotopyCategory.obj X ≅ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.up ℕ))).obj I.cocomplex
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.
Instances For
theorem
CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(I : InjectiveResolution X)
(J : InjectiveResolution Y)
(φ : I.cocomplex ⟶ J.cocomplex)
(comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0))
(F : Functor C D)
[F.Additive]
:
theorem
CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(I : InjectiveResolution X)
(J : InjectiveResolution Y)
(φ : I.cocomplex ⟶ J.cocomplex)
(comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0))
(F : 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)
:
CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f)
(CategoryStruct.comp (J.isoRightDerivedToHomotopyCategoryObj F).hom h) = CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).hom
(CategoryStruct.comp
((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)) h)
theorem
CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(I : InjectiveResolution X)
(J : InjectiveResolution Y)
(φ : I.cocomplex ⟶ J.cocomplex)
(comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0))
(F : Functor C D)
[F.Additive]
:
theorem
CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(I : InjectiveResolution X)
(J : InjectiveResolution Y)
(φ : I.cocomplex ⟶ J.cocomplex)
(comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0))
(F : Functor C D)
[F.Additive]
{Z : HomotopyCategory D (ComplexShape.up ℕ)}
(h : F.rightDerivedToHomotopyCategory.obj Y ⟶ Z)
:
CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).inv
(CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f) h) = CategoryStruct.comp
((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ))
(CategoryStruct.comp (J.isoRightDerivedToHomotopyCategoryObj F).inv h)
noncomputable def
CategoryTheory.Functor.rightDerived
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
(n : ℕ)
:
Functor C D
The right derived functors of an additive functor.
Instances For
noncomputable def
CategoryTheory.InjectiveResolution.isoRightDerivedObj
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{X : C}
(I : InjectiveResolution X)
(F : Functor C D)
[F.Additive]
(n : ℕ)
:
(F.rightDerived n).obj X ≅ (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).obj
((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)
We can compute a right derived functor using a chosen injective resolution.
Instances For
theorem
CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(I : InjectiveResolution X)
(J : InjectiveResolution Y)
(φ : I.cocomplex ⟶ J.cocomplex)
(comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0))
(F : Functor C D)
[F.Additive]
(n : ℕ)
:
CategoryStruct.comp ((F.rightDerived n).map f) (J.isoRightDerivedObj F n).hom = CategoryStruct.comp (I.isoRightDerivedObj F n).hom
(((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp
(HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map
φ)
theorem
CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(I : InjectiveResolution X)
(J : InjectiveResolution Y)
(φ : I.cocomplex ⟶ J.cocomplex)
(comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0))
(F : Functor C D)
[F.Additive]
(n : ℕ)
{Z : D}
(h :
(HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).obj
((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) ⟶ Z)
:
CategoryStruct.comp ((F.rightDerived n).map f) (CategoryStruct.comp (J.isoRightDerivedObj F n).hom h) = CategoryStruct.comp (I.isoRightDerivedObj F n).hom
(CategoryStruct.comp
((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ))
h)
theorem
CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(I : InjectiveResolution X)
(J : InjectiveResolution Y)
(φ : I.cocomplex ⟶ J.cocomplex)
(comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0))
(F : Functor C D)
[F.Additive]
(n : ℕ)
:
CategoryStruct.comp (I.isoRightDerivedObj F n).inv ((F.rightDerived n).map f) = CategoryStruct.comp
(((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp
(HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map
φ)
(J.isoRightDerivedObj F n).inv
theorem
CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(I : InjectiveResolution X)
(J : InjectiveResolution Y)
(φ : I.cocomplex ⟶ J.cocomplex)
(comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0))
(F : Functor C D)
[F.Additive]
(n : ℕ)
{Z : D}
(h : (F.rightDerived n).obj Y ⟶ Z)
:
CategoryStruct.comp (I.isoRightDerivedObj F n).inv (CategoryStruct.comp ((F.rightDerived n).map f) h) = CategoryStruct.comp
((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ))
(CategoryStruct.comp (J.isoRightDerivedObj F n).inv h)
theorem
CategoryTheory.Functor.isZero_rightDerived_obj_injective_succ
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
(n : ℕ)
(X : C)
[Injective X]
:
Limits.IsZero ((F.rightDerived (n + 1)).obj X)
The higher derived functors vanish on injective objects.
theorem
CategoryTheory.Functor.rightDerived_map_eq
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
(n : ℕ)
{X Y : C}
(f : X ⟶ Y)
{P : InjectiveResolution X}
{Q : InjectiveResolution Y}
(g : P.cocomplex ⟶ Q.cocomplex)
(w : CategoryStruct.comp P.ι g = CategoryStruct.comp ((CochainComplex.single₀ C).map f) Q.ι)
:
(F.rightDerived n).map f = CategoryStruct.comp (P.isoRightDerivedObj F n).hom
(CategoryStruct.comp
(((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp
(HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map
g)
(Q.isoRightDerivedObj F n).inv)
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}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{F G : Functor C D}
[F.Additive]
[G.Additive]
(α : F ⟶ G)
:
The natural transformation
F.rightDerivedToHomotopyCategory ⟶ G.rightDerivedToHomotopyCategory induced by
a natural transformation F ⟶ G between additive functors.
Instances For
theorem
CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{F G : Functor C D}
[F.Additive]
[G.Additive]
(α : F ⟶ G)
{X : C}
(P : InjectiveResolution X)
:
(NatTrans.rightDerivedToHomotopyCategory α).app X = CategoryStruct.comp (P.isoRightDerivedToHomotopyCategoryObj F).hom
(CategoryStruct.comp
((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex))
(P.isoRightDerivedToHomotopyCategoryObj G).inv)
@[simp]
theorem
CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_id
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
:
@[simp]
theorem
CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{F G H : Functor C D}
(α : F ⟶ G)
(β : G ⟶ H)
[F.Additive]
[G.Additive]
[H.Additive]
:
theorem
CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{F G H : Functor C D}
(α : F ⟶ G)
(β : G ⟶ H)
[F.Additive]
[G.Additive]
[H.Additive]
{Z : Functor C (HomotopyCategory D (ComplexShape.up ℕ))}
(h : H.rightDerivedToHomotopyCategory ⟶ Z)
:
noncomputable def
CategoryTheory.NatTrans.rightDerived
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{F G : Functor C D}
[F.Additive]
[G.Additive]
(α : F ⟶ G)
(n : ℕ)
:
The natural transformation between right-derived functors induced by a natural transformation.
Instances For
@[simp]
theorem
CategoryTheory.NatTrans.rightDerived_id
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
(n : ℕ)
:
rightDerived (CategoryStruct.id F) n = CategoryStruct.id (F.rightDerived n)
@[simp]
theorem
CategoryTheory.NatTrans.rightDerived_comp
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{F G H : Functor C D}
[F.Additive]
[G.Additive]
[H.Additive]
(α : F ⟶ G)
(β : G ⟶ H)
(n : ℕ)
:
rightDerived (CategoryStruct.comp α β) n = CategoryStruct.comp (rightDerived α n) (rightDerived β n)
theorem
CategoryTheory.NatTrans.rightDerived_comp_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{F G H : Functor C D}
[F.Additive]
[G.Additive]
[H.Additive]
(α : F ⟶ G)
(β : G ⟶ H)
(n : ℕ)
{Z : Functor C D}
(h : H.rightDerived n ⟶ Z)
:
CategoryStruct.comp (rightDerived (CategoryStruct.comp α β) n) h = CategoryStruct.comp (rightDerived α n) (CategoryStruct.comp (rightDerived β n) h)
theorem
CategoryTheory.InjectiveResolution.rightDerived_app_eq
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{F G : Functor C D}
[F.Additive]
[G.Additive]
(α : F ⟶ G)
{X : C}
(P : InjectiveResolution X)
(n : ℕ)
:
(NatTrans.rightDerived α n).app X = CategoryStruct.comp (P.isoRightDerivedObj F n).hom
(CategoryStruct.comp
((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex))
(P.isoRightDerivedObj G n).inv)
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}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[Abelian D]
{X : C}
(P : InjectiveResolution X)
(F : Functor C D)
[F.Additive]
:
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.
Instances For
@[simp]
theorem
CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian D]
{C : Type u_2}
[Category.{v_2, u_2} C]
[Abelian C]
{X : C}
(P : InjectiveResolution X)
(F : Functor C D)
[F.Additive]
:
CategoryStruct.comp (P.toRightDerivedZero' F)
(((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).iCycles 0) = F.map (P.ι.f 0)
@[simp]
theorem
CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian D]
{C : Type u_2}
[Category.{v_2, u_2} C]
[Abelian C]
{X : C}
(P : InjectiveResolution X)
(F : Functor C D)
[F.Additive]
{Z : D}
(h : ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).X 0 ⟶ Z)
:
CategoryStruct.comp (P.toRightDerivedZero' F)
(CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).iCycles 0) h) = CategoryStruct.comp (F.map (P.ι.f 0)) h
theorem
CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian D]
{C : Type u_2}
[Category.{v_2, u_2} C]
[Abelian C]
{X Y : C}
(f : X ⟶ Y)
(P : InjectiveResolution X)
(Q : InjectiveResolution Y)
(φ : P.cocomplex ⟶ Q.cocomplex)
(comm : CategoryStruct.comp (P.ι.f 0) (φ.f 0) = CategoryStruct.comp f (Q.ι.f 0))
(F : Functor C D)
[F.Additive]
:
CategoryStruct.comp (F.map f) (Q.toRightDerivedZero' F) = CategoryStruct.comp (P.toRightDerivedZero' F)
(HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) 0)
theorem
CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality_assoc
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian D]
{C : Type u_2}
[Category.{v_2, u_2} C]
[Abelian C]
{X Y : C}
(f : X ⟶ Y)
(P : InjectiveResolution X)
(Q : InjectiveResolution Y)
(φ : P.cocomplex ⟶ Q.cocomplex)
(comm : CategoryStruct.comp (P.ι.f 0) (φ.f 0) = CategoryStruct.comp f (Q.ι.f 0))
(F : Functor C D)
[F.Additive]
{Z : D}
(h : ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj Q.cocomplex).cycles 0 ⟶ Z)
:
CategoryStruct.comp (F.map f) (CategoryStruct.comp (Q.toRightDerivedZero' F) h) = CategoryStruct.comp (P.toRightDerivedZero' F)
(CategoryStruct.comp (HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) 0) h)
instance
CategoryTheory.InjectiveResolution.instIsIsoToRightDerivedZero'Self
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[Abelian D]
(F : Functor C D)
[F.Additive]
(X : C)
[Injective X]
:
IsIso ((self X).toRightDerivedZero' F)
noncomputable def
CategoryTheory.Functor.toRightDerivedZero
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
:
The natural transformation F ⟶ F.rightDerived 0.
Instances For
theorem
CategoryTheory.InjectiveResolution.toRightDerivedZero_eq
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
{X : C}
(I : InjectiveResolution X)
(F : Functor C D)
[F.Additive]
:
F.toRightDerivedZero.app X = CategoryStruct.comp (I.toRightDerivedZero' F)
(CategoryStruct.comp
(CochainComplex.isoHomologyπ₀ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)).hom
(I.isoRightDerivedObj F 0).inv)
instance
CategoryTheory.instIsIsoAppToRightDerivedZeroOfInjective
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
(X : C)
[Injective X]
:
IsIso (F.toRightDerivedZero.app X)
instance
CategoryTheory.instIsIsoToRightDerivedZero'
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
{X : C}
(P : InjectiveResolution X)
:
IsIso (P.toRightDerivedZero' F)
instance
CategoryTheory.instIsIsoAppToRightDerivedZero
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
(X : C)
:
IsIso (F.toRightDerivedZero.app X)
instance
CategoryTheory.instIsIsoFunctorToRightDerivedZero
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
:
noncomputable def
CategoryTheory.Functor.rightDerivedZeroIsoSelf
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
:
The canonical isomorphism F.rightDerived 0 ≅ F when F is left exact
(i.e. preserves finite limits).
Instances For
@[simp]
theorem
CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
:
@[simp]
theorem
CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
:
@[simp]
theorem
CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
{Z : Functor C D}
(h : F.rightDerived 0 ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
:
@[simp]
theorem
CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
{Z : Functor C D}
(h : F ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_app
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
(X : C)
:
CategoryStruct.comp (F.rightDerivedZeroIsoSelf.hom.app X) (F.toRightDerivedZero.app X) = CategoryStruct.id ((F.rightDerived 0).obj X)
@[simp]
theorem
CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_app_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
(X : C)
{Z : D}
(h : (F.rightDerived 0).obj X ⟶ Z)
:
CategoryStruct.comp (F.rightDerivedZeroIsoSelf.hom.app X) (CategoryStruct.comp (F.toRightDerivedZero.app X) h) = h
@[simp]
theorem
CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_app
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
(X : C)
:
CategoryStruct.comp (F.toRightDerivedZero.app X) (F.rightDerivedZeroIsoSelf.hom.app X) = CategoryStruct.id (F.obj X)
@[simp]
theorem
CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_app_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{v_1, u_1} D]
[Abelian C]
[HasInjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
(X : C)
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (F.toRightDerivedZero.app X) (CategoryStruct.comp (F.rightDerivedZeroIsoSelf.hom.app X) h) = h