Commit 2023-05-01 17:47 e14488e7

View on Github →

feat: port CategoryTheory.Abelian.Exact (#3638)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/Exact.lean

added theorem CategoryTheory.Exact.epi_kernel_lift

Created Mathlib/CategoryTheory/Abelian/Exact.lean

added theorem CategoryTheory.Abelian.Exact.op

added theorem CategoryTheory.Abelian.Exact.op_iff

added theorem CategoryTheory.Abelian.Exact.unop

added theorem CategoryTheory.Abelian.Exact.unop_iff

added theorem CategoryTheory.Abelian.cokernel.desc.inv

added theorem CategoryTheory.Abelian.epi_iff_cokernel_π_eq_zero

added theorem CategoryTheory.Abelian.exact_cokernel

added theorem CategoryTheory.Abelian.exact_epi_comp_iff

added theorem CategoryTheory.Abelian.exact_iff'

added theorem CategoryTheory.Abelian.exact_iff

added theorem CategoryTheory.Abelian.exact_iff_exact_coimage_π

added theorem CategoryTheory.Abelian.exact_iff_exact_image_ι

added theorem CategoryTheory.Abelian.exact_iff_image_eq_kernel

added theorem CategoryTheory.Abelian.exact_of_is_cokernel

added theorem CategoryTheory.Abelian.exact_of_is_kernel

added theorem CategoryTheory.Abelian.exact_tfae

added def CategoryTheory.Abelian.isColimitCoimage

added def CategoryTheory.Abelian.isColimitImage

added def CategoryTheory.Abelian.isColimitOfExactOfEpi

added theorem CategoryTheory.Abelian.isIso_cokernel_desc_of_exact_of_epi

added theorem CategoryTheory.Abelian.isIso_kernel_lift_of_exact_of_mono

added def CategoryTheory.Abelian.isLimitImage'

added def CategoryTheory.Abelian.isLimitImage

added def CategoryTheory.Abelian.isLimitOfExactOfMono

added theorem CategoryTheory.Abelian.kernel.lift.inv

added theorem CategoryTheory.Abelian.mono_cokernel_desc_of_exact

added theorem CategoryTheory.Abelian.mono_iff_kernel_ι_eq_zero

added theorem CategoryTheory.Abelian.tfae_epi

added theorem CategoryTheory.Abelian.tfae_mono

added theorem CategoryTheory.Functor.map_exact

added def CategoryTheory.Functor.preservesCokernelsOfMapExact

added theorem CategoryTheory.Functor.preservesEpimorphisms_of_map_exact

added def CategoryTheory.Functor.preservesFiniteColimitsOfMapExact

added def CategoryTheory.Functor.preservesFiniteColimitsOfPreservesEpisAndKernels

added def CategoryTheory.Functor.preservesFiniteLimitsOfMapExact

added def CategoryTheory.Functor.preservesFiniteLimitsOfPreservesMonosAndCokernels

added def CategoryTheory.Functor.preservesKernelsOfMapExact

added theorem CategoryTheory.Functor.preservesMonomorphisms_of_map_exact

added theorem CategoryTheory.Functor.preservesZeroMorphisms_of_map_exact

Modified Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean

added theorem CategoryTheory.Limits.colimit_ι_zero_cokernel_desc