Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-19 09:56 2b6b9ffc

View on Github →

feat(category_theory/abelian/derived): add left_derived_zero_iso_self (#12403) We add left_derived_zero_iso_self: the natural isomorphism (F.left_derived 0) ≅ F if preserves_finite_colimits F. From lean-liquid

Estimated changes

Modified src/algebra/homology/exact.lean

added theorem category_theory.preadditive.exact_of_iso_of_exact'

Created src/category_theory/abelian/derived.lean

added theorem category_theory.abelian.functor.exact_of_map_projective_resolution

added def category_theory.abelian.functor.left_derived_zero_iso_self

added def category_theory.abelian.functor.left_derived_zero_to_self_app

added theorem category_theory.abelian.functor.left_derived_zero_to_self_app_comp_inv

added def category_theory.abelian.functor.left_derived_zero_to_self_app_inv

added theorem category_theory.abelian.functor.left_derived_zero_to_self_app_inv_comp

added def category_theory.abelian.functor.left_derived_zero_to_self_app_iso

added theorem category_theory.abelian.functor.left_derived_zero_to_self_natural

added theorem category_theory.abelian.functor.preserves_exact_of_preserves_finite_colimits_of_epi

Modified src/category_theory/abelian/exact.lean

added theorem category_theory.abelian.cokernel.desc.inv