Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-06 07:44 d61ebab1

View on Github →

feat(category_theory/abelian): (co)kernels in terms of exact sequences (#12460)

Estimated changes

Modified src/category_theory/abelian/basic.lean

added theorem category_theory.abelian.comp_epi_desc

added def category_theory.abelian.epi_desc

added def category_theory.abelian.mono_lift

added theorem category_theory.abelian.mono_lift_comp

Modified src/category_theory/abelian/exact.lean

added theorem category_theory.abelian.exact_of_is_cokernel

added theorem category_theory.abelian.exact_of_is_kernel

added def category_theory.abelian.is_colimit_of_exact_of_epi

added def category_theory.abelian.is_limit_of_exact_of_mono