Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-05 15:19 4ecd92a9

View on Github →

feat(category_theory/abelian): faithful functors reflect exact sequences (#12071)

Estimated changes

Modified src/algebra/homology/exact.lean

added theorem category_theory.functor.exact_of_exact_map'

added theorem category_theory.functor.exact_of_exact_map

modified theorem category_theory.mono_iff_exact_zero_left

Modified src/category_theory/abelian/exact.lean

Modified src/category_theory/limits/preserves/shapes/zero.lean

added theorem category_theory.functor.map_eq_zero_iff

added theorem category_theory.functor.zero_of_map_zero