Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-12 07:00 e1c649d5

View on Github →

feat(category_theory/abelian): the five lemma (#8265)

Estimated changes

Modified src/algebra/homology/exact.lean

Modified src/category_theory/abelian/basic.lean

added theorem category_theory.abelian.coimages.comp_coimage_π_eq_zero

added theorem category_theory.abelian.epi_fst_of_factor_thru_epi_mono_factorization

added theorem category_theory.abelian.epi_fst_of_is_limit

added theorem category_theory.abelian.epi_snd_of_is_limit

added theorem category_theory.abelian.mono_inl_of_factor_thru_epi_mono_factorization

added theorem category_theory.abelian.mono_inl_of_is_colimit

added theorem category_theory.abelian.mono_inr_of_is_colimit

Modified src/category_theory/abelian/diagram_lemmas/four.lean

added theorem category_theory.abelian.epi_of_epi_of_epi_of_mono

added theorem category_theory.abelian.is_iso_of_is_iso_of_is_iso_of_is_iso_of_is_iso

Modified src/category_theory/abelian/exact.lean

added def category_theory.abelian.is_colimit_coimage

added def category_theory.abelian.is_colimit_image

Modified src/category_theory/limits/shapes/pullbacks.lean

added def category_theory.limits.pullback_cone.is_limit_of_factors

added def category_theory.limits.pushout_cocone.is_colimit_of_factors

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

added theorem category_theory.limits.comp_factor_thru_image_eq_zero

Modified src/category_theory/subobject/limits.lean

added theorem category_theory.limits.factor_thru_kernel_subobject_comp_kernel_subobject_iso