mathlib3 documentation


Zeroth left derived functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Main results #

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

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


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.