Documentation

Mathlib.CategoryTheory.Abelian.LeftDerived

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.

TODO #

refactor Functor.leftDerived (and Functor.rightDerived) 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 functor F.leftDerivedFunctorMinus : DerivedCategory.Minus C ⥤ DerivedCategory.Minus D, and F.leftDerived shall be redefined using F.leftDerivedFunctorMinus.

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) [F.Additive] :

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

F.leftDerivedToHomotopyCategory = (CategoryTheory.projectiveResolutions C).comp (F.mapHomotopyCategory (ComplexShape.down ℕ))

Instances For

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) [F.Additive] :

F.leftDerivedToHomotopyCategory.obj X ≅ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.down ℕ))).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

P.isoLeftDerivedToHomotopyCategoryObj F = (F.mapHomotopyCategory (ComplexShape.down ℕ)).mapIso P.iso ≪≫ (F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).app P.complex

Instances For

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) [F.Additive] {Z : HomotopyCategory D (ComplexShape.down ℕ)} (h : F.leftDerivedToHomotopyCategory.obj Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).inv (CategoryTheory.CategoryStruct.comp (F.leftDerivedToHomotopyCategory.map f) h) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)) (CategoryTheory.CategoryStruct.comp (Q.isoLeftDerivedToHomotopyCategoryObj 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) [F.Additive] :

CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).inv (F.leftDerivedToHomotopyCategory.map f) = CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.down ℕ))).map φ) (Q.isoLeftDerivedToHomotopyCategoryObj 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) [F.Additive] {Z : HomotopyCategory D (ComplexShape.down ℕ)} (h : (HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.leftDerivedToHomotopyCategory.map f) (CategoryTheory.CategoryStruct.comp (Q.isoLeftDerivedToHomotopyCategoryObj F).hom h) = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).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) [F.Additive] :

CategoryTheory.CategoryStruct.comp (F.leftDerivedToHomotopyCategory.map f) (Q.isoLeftDerivedToHomotopyCategoryObj F).hom = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.down ℕ))).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) [F.Additive] (n : ℕ) :

CategoryTheory.Functor C D

The left derived functors of an additive functor.

Equations

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

Instances For

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) [F.Additive] (n : ℕ) :

(F.leftDerived n).obj X ≅ (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.down ℕ)).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.

Instances For

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) [F.Additive] (n : ℕ) {Z : D} (h : (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((F.leftDerived n).map f) (CategoryTheory.CategoryStruct.comp (Q.isoLeftDerivedObj F n).hom h) = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).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) [F.Additive] (n : ℕ) :

CategoryTheory.CategoryStruct.comp ((F.leftDerived n).map f) (Q.isoLeftDerivedObj F n).hom = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).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) [F.Additive] (n : ℕ) {Z : D} (h : (F.leftDerived n).obj Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).inv (CategoryTheory.CategoryStruct.comp ((F.leftDerived n).map f) h) = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)) (CategoryTheory.CategoryStruct.comp (Q.isoLeftDerivedObj 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) [F.Additive] (n : ℕ) :

CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).inv ((F.leftDerived n).map f) = CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map φ) (Q.isoLeftDerivedObj 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) [F.Additive] (n : ℕ) (X : C) [CategoryTheory.Projective X] :

CategoryTheory.Limits.IsZero ((F.leftDerived (n + 1)).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) [F.Additive] (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).map f)) :

(F.leftDerived n).map f = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map g) (Q.isoLeftDerivedObj 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} [F.Additive] [G.Additive] (α : F ⟶ G) :

F.leftDerivedToHomotopyCategory ⟶ G.leftDerivedToHomotopyCategory

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.

Instances For

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} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : CategoryTheory.ProjectiveResolution X) :

(CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α).app X = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) (P.isoLeftDerivedToHomotopyCategoryObj 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) [F.Additive] :

CategoryTheory.NatTrans.leftDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.leftDerivedToHomotopyCategory

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) [F.Additive] [G.Additive] [H.Additive] {Z : CategoryTheory.Functor C (HomotopyCategory D (ComplexShape.down ℕ))} (h : H.leftDerivedToHomotopyCategory ⟶ 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) [F.Additive] [G.Additive] [H.Additive] :

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} [F.Additive] [G.Additive] (α : F ⟶ G) (n : ℕ) :

F.leftDerived n ⟶ G.leftDerived 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)

Instances For

@[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) [F.Additive] (n : ℕ) :

CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.id F) n = CategoryTheory.CategoryStruct.id (F.leftDerived 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} [F.Additive] [G.Additive] [H.Additive] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) {Z : CategoryTheory.Functor C D} (h : H.leftDerived 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} [F.Additive] [G.Additive] [H.Additive] (α : 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} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : CategoryTheory.ProjectiveResolution X) (n : ℕ) :

(CategoryTheory.NatTrans.leftDerived α n).app X = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) (P.isoLeftDerivedObj 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) [F.Additive] :

((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).opcycles 0 ⟶ F.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

P.fromLeftDerivedZero' F = ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).descOpcycles (F.map (P.π.f 0)) 1 CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'.proof_3 ⋯

Instances For

@[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) [F.Additive] {Z : D} (h : F.obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).pOpcycles 0) (CategoryTheory.CategoryStruct.comp (P.fromLeftDerivedZero' F) h) = CategoryTheory.CategoryStruct.comp (F.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) [F.Additive] :

CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).pOpcycles 0) (P.fromLeftDerivedZero' F) = F.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) [F.Additive] {Z : D} (h : F.obj Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) 0) (CategoryTheory.CategoryStruct.comp (Q.fromLeftDerivedZero' F) h) = CategoryTheory.CategoryStruct.comp (P.fromLeftDerivedZero' F) (CategoryTheory.CategoryStruct.comp (F.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) [F.Additive] :

CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) 0) (Q.fromLeftDerivedZero' F) = CategoryTheory.CategoryStruct.comp (P.fromLeftDerivedZero' F) (F.map f)

instance CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self {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) [F.Additive] (X : C) [CategoryTheory.Projective X] :

CategoryTheory.IsIso ((CategoryTheory.ProjectiveResolution.self X).fromLeftDerivedZero' F)

Equations

⋯ = ⋯

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) [F.Additive] :

F.leftDerived 0 ⟶ F

The natural transformation F.leftDerived 0 ⟶ F.

Equations

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

Instances For

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) [F.Additive] :

F.fromLeftDerivedZero.app X = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F 0).hom (CategoryTheory.CategoryStruct.comp (ChainComplex.isoHomologyι₀ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)).hom (P.fromLeftDerivedZero' F))

instance CategoryTheory.instIsIsoAppFromLeftDerivedZeroOfProjective {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) [F.Additive] (X : C) [CategoryTheory.Projective X] :

CategoryTheory.IsIso (F.fromLeftDerivedZero.app X)

Equations

⋯ = ⋯

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

CategoryTheory.IsIso (P.fromLeftDerivedZero' F)

Equations

⋯ = ⋯

instance CategoryTheory.instIsIsoAppFromLeftDerivedZero {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) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) :

CategoryTheory.IsIso (F.fromLeftDerivedZero.app X)

Equations

⋯ = ⋯

instance CategoryTheory.instIsIsoFunctorFromLeftDerivedZero {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) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] :

CategoryTheory.IsIso F.fromLeftDerivedZero

Equations

⋯ = ⋯

@[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) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] :

F.leftDerivedZeroIsoSelf.hom = F.fromLeftDerivedZero

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) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] :

F.leftDerived 0 ≅ F

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

Equations

F.leftDerivedZeroIsoSelf = CategoryTheory.asIso F.fromLeftDerivedZero

Instances For

@[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) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] {Z : CategoryTheory.Functor C D} (h : F.leftDerived 0 ⟶ Z) :

CategoryTheory.CategoryStruct.comp F.fromLeftDerivedZero (CategoryTheory.CategoryStruct.comp F.leftDerivedZeroIsoSelf.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) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] :

CategoryTheory.CategoryStruct.comp F.fromLeftDerivedZero F.leftDerivedZeroIsoSelf.inv = CategoryTheory.CategoryStruct.id (F.leftDerived 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) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] {Z : CategoryTheory.Functor C D} (h : F ⟶ Z) :

CategoryTheory.CategoryStruct.comp F.leftDerivedZeroIsoSelf.inv (CategoryTheory.CategoryStruct.comp F.fromLeftDerivedZero 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) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] :

CategoryTheory.CategoryStruct.comp F.leftDerivedZeroIsoSelf.inv F.fromLeftDerivedZero = 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) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) {Z : D} (h : (F.leftDerived 0).obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.fromLeftDerivedZero.app X) (CategoryTheory.CategoryStruct.comp (F.leftDerivedZeroIsoSelf.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) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) :

CategoryTheory.CategoryStruct.comp (F.fromLeftDerivedZero.app X) (F.leftDerivedZeroIsoSelf.inv.app X) = CategoryTheory.CategoryStruct.id ((F.leftDerived 0).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) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) {Z : D} (h : F.obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) (CategoryTheory.CategoryStruct.comp (F.fromLeftDerivedZero.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) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) :

CategoryTheory.CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) (F.fromLeftDerivedZero.app X) = CategoryTheory.CategoryStruct.id (F.obj X)