Commit 2023-04-05 03:01 1084b886

View on Github →

feat: port CategoryTheory.Abelian.Basic (#2769)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Abelian/Basic.lean

added def CategoryTheory.Abelian.BiproductToPushoutIsCokernel.isColimitBiproductToPushout

added theorem CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.hasImages

added def CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageFactorisation

added def CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation

added theorem CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e'

added def CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.normalEpiCategory

added def CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.normalMonoCategory

added def CategoryTheory.Abelian.PullbackToBiproductIsKernel.isLimitPullbackToBiproduct

added theorem CategoryTheory.Abelian.coimageIsoImage'_hom

added def CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation

added theorem CategoryTheory.Abelian.comp_coimage_π_eq_zero

added theorem CategoryTheory.Abelian.comp_epiDesc

added def CategoryTheory.Abelian.epiDesc

added def CategoryTheory.Abelian.epiIsCokernelOfKernel

added theorem CategoryTheory.Abelian.epi_fst_of_factor_thru_epi_mono_factorization

added theorem CategoryTheory.Abelian.epi_fst_of_isLimit

added theorem CategoryTheory.Abelian.epi_of_cokernel_π_eq_zero

added theorem CategoryTheory.Abelian.epi_snd_of_isLimit

added theorem CategoryTheory.Abelian.factorThruImage_comp_coimageIsoImage'_inv

added theorem CategoryTheory.Abelian.hasFiniteBiproducts

added theorem CategoryTheory.Abelian.imageIsoImage_hom_comp_image_ι

added theorem CategoryTheory.Abelian.imageIsoImage_inv

added def CategoryTheory.Abelian.imageStrongEpiMonoFactorisation

added theorem CategoryTheory.Abelian.image_ι_comp_eq_zero

added def CategoryTheory.Abelian.monoIsKernelOfCokernel

added def CategoryTheory.Abelian.monoLift

added theorem CategoryTheory.Abelian.monoLift_comp

added theorem CategoryTheory.Abelian.mono_inl_of_factor_thru_epi_mono_factorization

added theorem CategoryTheory.Abelian.mono_inl_of_isColimit

added theorem CategoryTheory.Abelian.mono_inr_of_isColimit

added theorem CategoryTheory.Abelian.mono_of_kernel_ι_eq_zero

added def CategoryTheory.Abelian.nonPreadditiveAbelian

added def CategoryTheory.Abelian.ofCoimageImageComparisonIsIso

added def CategoryTheory.NonPreadditiveAbelian.abelian