Commit 2022-03-23 20:36 cd942870

View on Github →

feat(category_theory/abelian): right derived functor in abelian category with enough injectives (#12810) This pr shows that in an abelian category with enough injectives, if a functor preserves finite limits, then the zeroth right derived functor is naturally isomorphic to itself. Dual to #12403 ↔️

Estimated changes

Modified src/category_theory/abelian/right_derived.lean

added theorem category_theory.abelian.functor.exact_of_map_injective_resolution

added theorem category_theory.abelian.functor.preserves_exact_of_preserves_finite_limits_of_mono

added def category_theory.abelian.functor.right_derived_zero_iso_self

added def category_theory.abelian.functor.right_derived_zero_to_self_app

added theorem category_theory.abelian.functor.right_derived_zero_to_self_app_comp_inv

added def category_theory.abelian.functor.right_derived_zero_to_self_app_inv

added theorem category_theory.abelian.functor.right_derived_zero_to_self_app_inv_comp

added def category_theory.abelian.functor.right_derived_zero_to_self_app_iso

added theorem category_theory.abelian.functor.right_derived_zero_to_self_natural