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 #

Main results #