# mathlibdocumentation

category_theory.abelian.left_derived

# 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.left_derived 0 ≅ F.

## Main definitions #

• category_theory.abelian.functor.left_derived_zero_iso_self: the natural isomorphism (F.left_derived 0) ≅ F.

## Main results #

• preserves_exact_of_preserves_finite_colimits_of_epi: if preserves_finite_colimits F and epi g, then exact (F.map f) (F.map g) if exact f g.
theorem category_theory.abelian.functor.preserves_exact_of_preserves_finite_colimits_of_epi {C : Type u} {D : Type u} (F : C D) {X Y Z : C} {f : X Y} {g : Y Z} [F.additive] (ex : g) :

If preserves_finite_colimits F and epi g, then exact (F.map f) (F.map g) if exact f g.

theorem category_theory.abelian.functor.exact_of_map_projective_resolution {C : Type u} {D : Type u} (F : C D) {X : C} [F.additive]  :
(F.map (P.π.f 0))
@[nolint]
noncomputable def category_theory.abelian.functor.left_derived_zero_to_self_app {C : Type u} {D : Type u} (F : C D) [F.additive] {X : C}  :
(F.left_derived 0).obj X F.obj X

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

Equations
noncomputable def category_theory.abelian.functor.left_derived_zero_to_self_app_inv {C : Type u} {D : Type u} (F : C D) [F.additive] {X : C}  :
F.obj X (F.left_derived 0).obj X

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

Equations
theorem category_theory.abelian.functor.left_derived_zero_to_self_app_comp_inv {C : Type u} {D : Type u} (F : C D) [F.additive] {X : C}  :
noncomputable def category_theory.abelian.functor.left_derived_zero_to_self_app_iso {C : Type u} {D : Type u} (F : C D) [F.additive] {X : C}  :
(F.left_derived 0).obj X F.obj X

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

Equations
theorem category_theory.abelian.functor.left_derived_zero_to_self_natural {C : Type u} {D : Type u} (F : C D) [F.additive] {X 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 left_derived_zero_to_self_obj_hom.

noncomputable def category_theory.abelian.functor.left_derived_zero_iso_self {C : Type u} {D : Type u} (F : C D) [F.additive]  :

Given preserves_finite_colimits F, the natural isomorphism (F.left_derived 0) ≅ F`.

Equations