Commit 2022-03-21 19:25 8001ea54

View on Github →

feat(category_theory/abelian): right derived functor (#12841) This pr dualises derived.lean. Right derived functor and natural transformation between right derived functors and related lemmas are formalised. The docs string currently contains more than what is in this file, but everything else will come shortly after.

Estimated changes

Modified src/category_theory/abelian/ext.lean

Renamed src/category_theory/abelian/derived.lean to src/category_theory/abelian/left_derived.lean

Created src/category_theory/abelian/right_derived.lean

added def category_theory.functor.right_derived

added theorem category_theory.functor.right_derived_map_eq

added def category_theory.functor.right_derived_obj_injective_succ

added def category_theory.functor.right_derived_obj_injective_zero

added def category_theory.functor.right_derived_obj_iso

added def category_theory.nat_trans.right_derived

added theorem category_theory.nat_trans.right_derived_comp

added theorem category_theory.nat_trans.right_derived_eq

added theorem category_theory.nat_trans.right_derived_id

Renamed src/category_theory/functor/derived.lean to src/category_theory/functor/left_derived.lean

Modified src/category_theory/monoidal/tor.lean