Left-derived functors

We define the left-derived functors F.leftDerived n : C ⥤ D for any additive functor F out of a category with projective resolutions.

We first define a functor F.leftDerivedToHomotopyCategory : C ⥤ HomotopyCategory D (ComplexShape.down ℕ) which is projectiveResolutions C ⋙ F.mapHomotopyCategory _. We show that if X : C and P : ProjectiveResolution X, then F.leftDerivedToHomotopyCategory.obj X identifies to the image in the homotopy category of the functor F applied objectwise to P.complex (this isomorphism is P.isoLeftDerivedToHomotopyCategoryObj F).

Then, the left-derived functors F.leftDerived n : C ⥤ D are obtained by composing F.leftDerivedToHomotopyCategory with the homology functors on the homotopy category.

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

Main results

• Functor.isZero_leftDerived_obj_projective_succ: projective objects have no higher left derived functor.
• NatTrans.leftDerived: the natural isomorphism between left derived functors induced by natural transformation.
• Functor.fromLeftDerivedZero: the natural transformation F.leftDerived 0 ⟶ F, which is an isomorphism when F is right exact (i.e. preserves finite colimits), see also Functor.leftDerivedZeroIsoSelf.

noncomputable def CategoryTheory.Functor.leftDerivedToHomotopyCategory {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.Functor C (HomotopyCategory D (ComplexShape.down ℕ))

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

Equations

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

noncomputable def CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} (P : CategoryTheory.ProjectiveResolution X) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : (CategoryTheory.Functor.leftDerivedToHomotopyCategory F).toPrefunctor.obj X ≅ (CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)) (HomotopyCategory.quotient D (ComplexShape.down ℕ))).toPrefunctor.obj P.complex

If P : ProjectiveResolution Z and F : C ⥤ D is an additive functor, this is an isomorphism between F.leftDerivedToHomotopyCategory.obj X and the complex obtained by applying F to P.complex.

Equations

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

theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_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.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] {Z : HomotopyCategory D (ComplexShape.down ℕ)} (h : (CategoryTheory.Functor.leftDerivedToHomotopyCategory F).toPrefunctor.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj P F).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.leftDerivedToHomotopyCategory F).toPrefunctor.map f) h) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).toPrefunctor.map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).toPrefunctor.map φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj Q F).inv h)

theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_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.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj P F).inv ((CategoryTheory.Functor.leftDerivedToHomotopyCategory F).toPrefunctor.map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)) (HomotopyCategory.quotient D (ComplexShape.down ℕ))).toPrefunctor.map φ) (CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj Q F).inv

theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_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.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] {Z : HomotopyCategory D (ComplexShape.down ℕ)} (h : (HomotopyCategory.quotient D (ComplexShape.down ℕ)).toPrefunctor.obj ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).toPrefunctor.obj Q.complex) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.leftDerivedToHomotopyCategory F).toPrefunctor.map f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj Q F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj P F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).toPrefunctor.map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).toPrefunctor.map φ)) h)

theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_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.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.leftDerivedToHomotopyCategory F).toPrefunctor.map f) (CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj Q F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj P F).hom ((CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)) (HomotopyCategory.quotient D (ComplexShape.down ℕ))).toPrefunctor.map φ)

noncomputable def CategoryTheory.Functor.leftDerived {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) : CategoryTheory.Functor C D

The left derived functors of an additive functor.

Equations

• CategoryTheory.Functor.leftDerived F n = CategoryTheory.Functor.comp (CategoryTheory.Functor.leftDerivedToHomotopyCategory F) (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)

noncomputable def CategoryTheory.ProjectiveResolution.isoLeftDerivedObj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} (P : CategoryTheory.ProjectiveResolution X) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) : (CategoryTheory.Functor.leftDerived F n).toPrefunctor.obj X ≅ (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).toPrefunctor.obj ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).toPrefunctor.obj P.complex)

We can compute a left derived functor using a chosen projective resolution.

Equations

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

theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_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.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) {Z : D} (h : (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).toPrefunctor.obj ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).toPrefunctor.obj Q.complex) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.leftDerived F n).toPrefunctor.map f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedObj Q F n).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedObj P F n).hom (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).toPrefunctor.map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).toPrefunctor.map φ)) h)

theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_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.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.leftDerived F n).toPrefunctor.map f) (CategoryTheory.ProjectiveResolution.isoLeftDerivedObj Q F n).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedObj P F n).hom ((CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).toPrefunctor.map φ)

theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_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.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) {Z : D} (h : (CategoryTheory.Functor.leftDerived F n).toPrefunctor.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedObj P F n).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.leftDerived F n).toPrefunctor.map f) h) = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).toPrefunctor.map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).toPrefunctor.map φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedObj Q F n).inv h)

theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_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.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedObj P F n).inv ((CategoryTheory.Functor.leftDerived F n).toPrefunctor.map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).toPrefunctor.map φ) (CategoryTheory.ProjectiveResolution.isoLeftDerivedObj Q F n).inv

theorem CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) (X : C) [CategoryTheory.Projective X] : CategoryTheory.Limits.IsZero ((CategoryTheory.Functor.leftDerived F (n + 1)).toPrefunctor.obj X)

The higher derived functors vanish on projective objects.

theorem CategoryTheory.Functor.leftDerived_map_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) {X : C} {Y : C} (f : X ⟶ Y) {P : CategoryTheory.ProjectiveResolution X} {Q : CategoryTheory.ProjectiveResolution Y} (g : P.complex ⟶ Q.complex) (w : CategoryTheory.CategoryStruct.comp g Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).toPrefunctor.map f)) : (CategoryTheory.Functor.leftDerived F n).toPrefunctor.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedObj P F n).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).toPrefunctor.map g) (CategoryTheory.ProjectiveResolution.isoLeftDerivedObj Q F n).inv)

We can compute a left derived functor on a morphism using a descent of that morphism to a chain map between chosen projective resolutions.

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

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

Equations

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

theorem CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] (α : F ⟶ G) {X : C} (P : CategoryTheory.ProjectiveResolution X) : (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α).app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj P F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).toPrefunctor.map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) (CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj P G).inv)

@[simp]

theorem CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.NatTrans.leftDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.leftDerivedToHomotopyCategory F)

theorem CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] [CategoryTheory.Functor.Additive H] {Z : CategoryTheory.Functor C (HomotopyCategory D (ComplexShape.down ℕ))} (h : CategoryTheory.Functor.leftDerivedToHomotopyCategory H ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α) (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory β) h)

@[simp]

theorem CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] [CategoryTheory.Functor.Additive H] : CategoryTheory.NatTrans.leftDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α) (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory β)

noncomputable def CategoryTheory.NatTrans.leftDerived {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] (α : F ⟶ G) (n : ℕ) : CategoryTheory.Functor.leftDerived F n ⟶ CategoryTheory.Functor.leftDerived G n

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

Equations

• CategoryTheory.NatTrans.leftDerived α n = CategoryTheory.whiskerRight (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α) (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)

@[simp]

theorem CategoryTheory.NatTrans.leftDerived_id {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) : CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.id F) n = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.leftDerived F n)

theorem CategoryTheory.NatTrans.leftDerived_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] [CategoryTheory.Functor.Additive H] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) {Z : CategoryTheory.Functor C D} (h : CategoryTheory.Functor.leftDerived H n ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.comp α β) n) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived α n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived β n) h)

@[simp]

theorem CategoryTheory.NatTrans.leftDerived_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] [CategoryTheory.Functor.Additive H] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) : CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.comp α β) n = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived α n) (CategoryTheory.NatTrans.leftDerived β n)

theorem CategoryTheory.ProjectiveResolution.leftDerived_app_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] (α : F ⟶ G) {X : C} (P : CategoryTheory.ProjectiveResolution X) (n : ℕ) : (CategoryTheory.NatTrans.leftDerived α n).app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedObj P F n).hom (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).toPrefunctor.map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) (CategoryTheory.ProjectiveResolution.isoLeftDerivedObj P G n).inv)

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

noncomputable def CategoryTheory.ProjectiveResolution.fromLeftDerivedZero' {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.ProjectiveResolution X) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : HomologicalComplex.opcycles ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).toPrefunctor.obj P.complex) 0 ⟶ F.toPrefunctor.obj X

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

Equations

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

@[simp]

theorem CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_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.ProjectiveResolution X) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] {Z : D} (h : F.toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).toPrefunctor.obj P.complex) 0) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.fromLeftDerivedZero' P F) h) = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (P.π.f 0)) h

@[simp]

theorem CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero' {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.ProjectiveResolution X) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).toPrefunctor.obj P.complex) 0) (CategoryTheory.ProjectiveResolution.fromLeftDerivedZero' P F) = F.toPrefunctor.map (P.π.f 0)

theorem CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_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.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] {Z : D} (h : F.toPrefunctor.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).toPrefunctor.map φ) 0) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.fromLeftDerivedZero' Q F) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.fromLeftDerivedZero' P F) (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) h)

theorem CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality {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.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).toPrefunctor.map φ) 0) (CategoryTheory.ProjectiveResolution.fromLeftDerivedZero' Q F) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.fromLeftDerivedZero' P F) (F.toPrefunctor.map f)

instance CategoryTheory.ProjectiveResolution.instIsIsoOpcyclesPreadditiveHasZeroMorphismsToPreadditiveNatDownToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringObjHomologicalComplexPreadditiveHasZeroMorphismsToPreadditiveToQuiverToCategoryStructInstCategoryHomologicalComplexHomologicalComplexToQuiverToCategoryStructInstCategoryHomologicalComplexToPrefunctorMapHomologicalComplexComplexHasZeroObjectSelfOfNatInstOfNatNatHasHomologyCategoryWithHomology_of_abelianScObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorFromLeftDerivedZero' {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] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (X : C) [CategoryTheory.Projective X] : CategoryTheory.IsIso (CategoryTheory.ProjectiveResolution.fromLeftDerivedZero' (CategoryTheory.ProjectiveResolution.self X) F)

Equations

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

noncomputable def CategoryTheory.Functor.fromLeftDerivedZero {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.Functor.leftDerived F 0 ⟶ F

The natural transformation F.leftDerived 0 ⟶ F.

Equations

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

theorem CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} (P : CategoryTheory.ProjectiveResolution X) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : (CategoryTheory.Functor.fromLeftDerivedZero F).app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.isoLeftDerivedObj P F 0).hom (CategoryTheory.CategoryStruct.comp (ChainComplex.isoHomologyι₀ ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).toPrefunctor.obj P.complex)).hom (CategoryTheory.ProjectiveResolution.fromLeftDerivedZero' P F))

instance CategoryTheory.instIsIsoObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorLeftDerivedOfNatNatInstOfNatNatAppFromLeftDerivedZero {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (X : C) [CategoryTheory.Projective X] : CategoryTheory.IsIso ((CategoryTheory.Functor.fromLeftDerivedZero F).app X)

Equations

• (_ : CategoryTheory.IsIso ((CategoryTheory.Functor.fromLeftDerivedZero F).app X)) = (_ : CategoryTheory.IsIso ((CategoryTheory.Functor.fromLeftDerivedZero F).app X))

instance CategoryTheory.instIsIsoOpcyclesPreadditiveHasZeroMorphismsToPreadditiveNatDownToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringObjHomologicalComplexPreadditiveHasZeroMorphismsToPreadditiveToQuiverToCategoryStructInstCategoryHomologicalComplexHomologicalComplexToQuiverToCategoryStructInstCategoryHomologicalComplexToPrefunctorMapHomologicalComplexComplexHasZeroObjectOfNatInstOfNatNatHasHomologyCategoryWithHomology_of_abelianScObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorFromLeftDerivedZero' {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] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteColimits F] {X : C} (P : CategoryTheory.ProjectiveResolution X) : CategoryTheory.IsIso (CategoryTheory.ProjectiveResolution.fromLeftDerivedZero' P F)

Equations

• (_ : CategoryTheory.IsIso (CategoryTheory.ProjectiveResolution.fromLeftDerivedZero' P F)) = (_ : CategoryTheory.IsIso (CategoryTheory.ProjectiveResolution.fromLeftDerivedZero' P F))

instance CategoryTheory.instIsIsoObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorLeftDerivedOfNatNatInstOfNatNatAppFromLeftDerivedZero_1 {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) : CategoryTheory.IsIso ((CategoryTheory.Functor.fromLeftDerivedZero F).app X)

Equations

• (_ : CategoryTheory.IsIso ((CategoryTheory.Functor.fromLeftDerivedZero F).app X)) = (_ : CategoryTheory.IsIso ((CategoryTheory.Functor.fromLeftDerivedZero F).app X))

instance CategoryTheory.instIsIsoFunctorCategoryLeftDerivedOfNatNatInstOfNatNatFromLeftDerivedZero {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.IsIso (CategoryTheory.Functor.fromLeftDerivedZero F)

Equations

• (_ : CategoryTheory.IsIso (CategoryTheory.Functor.fromLeftDerivedZero F)) = (_ : CategoryTheory.IsIso (CategoryTheory.Functor.fromLeftDerivedZero F))

@[simp]

theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteColimits F] : (CategoryTheory.Functor.leftDerivedZeroIsoSelf F).hom = CategoryTheory.Functor.fromLeftDerivedZero F

noncomputable def CategoryTheory.Functor.leftDerivedZeroIsoSelf {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Functor.leftDerived F 0 ≅ F

The canonical isomorphism F.leftDerived 0 ≅ F when F is right exact (i.e. preserves finite colimits).

Equations

• CategoryTheory.Functor.leftDerivedZeroIsoSelf F = CategoryTheory.asIso (CategoryTheory.Functor.fromLeftDerivedZero F)

@[simp]

theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteColimits F] {Z : CategoryTheory.Functor C D} (h : CategoryTheory.Functor.leftDerived F 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.fromLeftDerivedZero F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.leftDerivedZeroIsoSelf F).inv h) = h

@[simp]

theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.fromLeftDerivedZero F) (CategoryTheory.Functor.leftDerivedZeroIsoSelf F).inv = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.leftDerived F 0)

@[simp]

theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteColimits F] {Z : CategoryTheory.Functor C D} (h : F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.leftDerivedZeroIsoSelf F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.fromLeftDerivedZero F) h) = h

@[simp]

theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.leftDerivedZeroIsoSelf F).inv (CategoryTheory.Functor.fromLeftDerivedZero F) = CategoryTheory.CategoryStruct.id F

@[simp]

theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_app_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) {Z : D} (h : (CategoryTheory.Functor.leftDerived F 0).toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.fromLeftDerivedZero F).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.leftDerivedZeroIsoSelf F).inv.app X) h) = h

@[simp]

theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.fromLeftDerivedZero F).app X) ((CategoryTheory.Functor.leftDerivedZeroIsoSelf F).inv.app X) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.leftDerived F 0).toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_app_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) {Z : D} (h : F.toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.leftDerivedZeroIsoSelf F).inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.fromLeftDerivedZero F).app X) h) = h

@[simp]

theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.leftDerivedZeroIsoSelf F).inv.app X) ((CategoryTheory.Functor.fromLeftDerivedZero F).app X) = CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)