Zeroth left derived functors

If F : C ⥤ D is an additive right exact functor between abelian categories, where C has enough projectives, we provide the natural isomorphism F.leftDerived 0 ≅ F.

Main definitions

• CategoryTheory.Abelian.Functor.leftDerivedZeroIsoSelf: the natural isomorphism (F.leftDerived 0) ≅ F.

Main results

• preserves_exact_of_PreservesFiniteColimits_of_epi: if PreservesFiniteColimits F and Epi g, then Exact (F.map f) (F.map g) if exact f g.

theorem CategoryTheory.Abelian.Functor.preserves_exact_of_PreservesFiniteColimits_of_epi {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.Epi g] (ex : CategoryTheory.Exact f g) : CategoryTheory.Exact (F.map f) (F.map g)

If PreservesFiniteColimits F and Epi g, then Exact (F.map f) (F.map g) if Exact f g.

theorem CategoryTheory.Abelian.Functor.exact_of_map_projectiveResolution {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) {X : C} [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] (P : CategoryTheory.ProjectiveResolution X) [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Exact (HomologicalComplex.dTo ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) (F.map (HomologicalComplex.Hom.f P.π 0))

def CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfApp {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.EnoughProjectives C] {X : C} (P : CategoryTheory.ProjectiveResolution X) : (CategoryTheory.Functor.leftDerived F 0).obj X ⟶ F.obj X

Given P : ProjectiveResolution X, a morphism (F.leftDerived 0).obj X ⟶ F.obj X.

def CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfAppInv {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.EnoughProjectives C] [CategoryTheory.Limits.PreservesFiniteColimits F] {X : C} (P : CategoryTheory.ProjectiveResolution X) : F.obj X ⟶ (CategoryTheory.Functor.leftDerived F 0).obj X

Given P : ProjectiveResolution X, a morphism F.obj X ⟶ (F.leftDerived 0).obj X given PreservesFiniteColimits F.

theorem CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfApp_comp_inv {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.EnoughProjectives C] [CategoryTheory.Limits.PreservesFiniteColimits F] {X : C} (P : CategoryTheory.ProjectiveResolution X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfApp F P) (CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfAppInv F P) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.leftDerived F 0).obj X)

theorem CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfAppInv_comp {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.EnoughProjectives C] [CategoryTheory.Limits.PreservesFiniteColimits F] {X : C} (P : CategoryTheory.ProjectiveResolution X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfAppInv F P) (CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfApp F P) = CategoryTheory.CategoryStruct.id (F.obj X)

def CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfAppIso {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.EnoughProjectives C] [CategoryTheory.Limits.PreservesFiniteColimits F] {X : C} (P : CategoryTheory.ProjectiveResolution X) : (CategoryTheory.Functor.leftDerived F 0).obj X ≅ F.obj X

Given P : ProjectiveResolution X, the isomorphism (F.leftDerived 0).obj X ≅ F.obj X if PreservesFiniteColimits F.

theorem CategoryTheory.Abelian.Functor.leftDerived_zero_to_self_natural {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.EnoughProjectives C] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.leftDerived F 0).map f) (CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfApp F Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfApp F P) (F.map f)

Given P : ProjectiveResolution X and Q : ProjectiveResolution Y and a morphism f : X ⟶ Y, naturality of the square given by leftDerived_zero_to_self_obj_hom.

def CategoryTheory.Abelian.Functor.leftDerivedZeroIsoSelf {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.EnoughProjectives C] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Functor.leftDerived F 0 ≅ F

Given PreservesFiniteColimits F, the natural isomorphism (F.leftDerived 0) ≅ F.