Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-18 08:44 c3561489

View on Github →

feat(category_theory/abelian): pseudoelements and a four lemma (#3803)

Estimated changes

Modified src/category_theory/abelian/basic.lean

added theorem category_theory.abelian.image_ι_eq_image_ι

added theorem category_theory.abelian.kernel_cokernel_eq_image_ι

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

added theorem category_theory.abelian.mono_of_epi_of_mono_of_mono

Modified src/category_theory/abelian/exact.lean

added def category_theory.abelian.is_limit_image

Created src/category_theory/abelian/pseudoelements.lean

added def category_theory.abelian.app

added theorem category_theory.abelian.app_hom

added def category_theory.abelian.pseudo_equal

added theorem category_theory.abelian.pseudo_equal_refl

added theorem category_theory.abelian.pseudo_equal_symm

added theorem category_theory.abelian.pseudo_equal_trans

added theorem category_theory.abelian.pseudoelement.apply_eq_zero_of_comp_eq_zero

added theorem category_theory.abelian.pseudoelement.apply_zero

added theorem category_theory.abelian.pseudoelement.comp_apply

added theorem category_theory.abelian.pseudoelement.comp_comp

added theorem category_theory.abelian.pseudoelement.epi_of_pseudo_surjective

added theorem category_theory.abelian.pseudoelement.eq_zero_iff

added theorem category_theory.abelian.pseudoelement.exact_of_pseudo_exact

added def category_theory.abelian.pseudoelement.hom_to_fun

added theorem category_theory.abelian.pseudoelement.mono_of_zero_of_map_zero

added def category_theory.abelian.pseudoelement.object_to_sort

added theorem category_theory.abelian.pseudoelement.over_coe_def

added def category_theory.abelian.pseudoelement.over_to_sort

added def category_theory.abelian.pseudoelement.pseudo_apply

added theorem category_theory.abelian.pseudoelement.pseudo_apply_aux

added theorem category_theory.abelian.pseudoelement.pseudo_apply_mk

added theorem category_theory.abelian.pseudoelement.pseudo_exact_of_exact

added theorem category_theory.abelian.pseudoelement.pseudo_injective_of_mono

added theorem category_theory.abelian.pseudoelement.pseudo_pullback

added theorem category_theory.abelian.pseudoelement.pseudo_surjective_of_epi

added def category_theory.abelian.pseudoelement.pseudo_zero

added theorem category_theory.abelian.pseudoelement.pseudo_zero_aux

added theorem category_theory.abelian.pseudoelement.pseudo_zero_def

added theorem category_theory.abelian.pseudoelement.pseudo_zero_iff

added def category_theory.abelian.pseudoelement.setoid

added theorem category_theory.abelian.pseudoelement.sub_of_eq_image

added theorem category_theory.abelian.pseudoelement.zero_apply

added theorem category_theory.abelian.pseudoelement.zero_eq_zero'

added theorem category_theory.abelian.pseudoelement.zero_eq_zero

added theorem category_theory.abelian.pseudoelement.zero_morphism_ext'

added theorem category_theory.abelian.pseudoelement.zero_morphism_ext

added theorem category_theory.abelian.pseudoelement.zero_of_map_zero

added def category_theory.abelian.pseudoelement

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

added theorem category_theory.limits.image_ι_comp_eq_zero

Modified src/category_theory/over.lean

added def category_theory.over.coe_from_hom

added theorem category_theory.over.coe_hom