# Documentation

Mathlib.CategoryTheory.Abelian.LeftDerived

# 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} {D : Type u} (F : ) {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} (ex : ) :
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.

def CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfApp {C : Type u} {D : Type u} (F : ) {X : C} :
().obj X F.obj X

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

Instances For
def CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfAppInv {C : Type u} {D : Type u} (F : ) {X : C} :
F.obj X ().obj X

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

Instances For
def CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfAppIso {C : Type u} {D : Type u} (F : ) {X : C} :
().obj X F.obj X

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

Instances For
theorem CategoryTheory.Abelian.Functor.leftDerived_zero_to_self_natural {C : Type u} {D : Type u} (F : ) {X : C} {Y : C} (f : X Y) :

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.

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

Instances For