Commit 2023-05-10 06:12 8ac1301c

View on Github →

feat: port CategoryTheory.Abelian.Pseudoelements (#3843)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Abelian/Pseudoelements.lean

added def CategoryTheory.Abelian.PseudoEqual

added theorem CategoryTheory.Abelian.Pseudoelement.ModuleCat.eq_range_of_pseudoequal

added theorem CategoryTheory.Abelian.Pseudoelement.apply_eq_zero_of_comp_eq_zero

added theorem CategoryTheory.Abelian.Pseudoelement.apply_zero

added theorem CategoryTheory.Abelian.Pseudoelement.comp_apply

added theorem CategoryTheory.Abelian.Pseudoelement.comp_comp

added theorem CategoryTheory.Abelian.Pseudoelement.epi_of_pseudo_surjective

added theorem CategoryTheory.Abelian.Pseudoelement.eq_zero_iff

added theorem CategoryTheory.Abelian.Pseudoelement.exact_of_pseudo_exact

added def CategoryTheory.Abelian.Pseudoelement.homToFun

added theorem CategoryTheory.Abelian.Pseudoelement.mono_of_zero_of_map_zero

added def CategoryTheory.Abelian.Pseudoelement.objectToSort

added def CategoryTheory.Abelian.Pseudoelement.overToSort

added theorem CategoryTheory.Abelian.Pseudoelement.over_coe_def

added def CategoryTheory.Abelian.Pseudoelement.pseudoApply

added theorem CategoryTheory.Abelian.Pseudoelement.pseudoApply_aux

added theorem CategoryTheory.Abelian.Pseudoelement.pseudoApply_mk'

added def CategoryTheory.Abelian.Pseudoelement.pseudoZero

added theorem CategoryTheory.Abelian.Pseudoelement.pseudoZero_aux

added theorem CategoryTheory.Abelian.Pseudoelement.pseudoZero_def

added theorem CategoryTheory.Abelian.Pseudoelement.pseudoZero_iff

added theorem CategoryTheory.Abelian.Pseudoelement.pseudo_exact_of_exact

added theorem CategoryTheory.Abelian.Pseudoelement.pseudo_injective_of_mono

added theorem CategoryTheory.Abelian.Pseudoelement.pseudo_pullback

added theorem CategoryTheory.Abelian.Pseudoelement.pseudo_surjective_of_epi

added def CategoryTheory.Abelian.Pseudoelement.setoid

added theorem CategoryTheory.Abelian.Pseudoelement.sub_of_eq_image

added theorem CategoryTheory.Abelian.Pseudoelement.zero_apply

added theorem CategoryTheory.Abelian.Pseudoelement.zero_eq_zero'

added theorem CategoryTheory.Abelian.Pseudoelement.zero_eq_zero

added theorem CategoryTheory.Abelian.Pseudoelement.zero_morphism_ext'

added theorem CategoryTheory.Abelian.Pseudoelement.zero_morphism_ext

added theorem CategoryTheory.Abelian.Pseudoelement.zero_of_map_zero

added def CategoryTheory.Abelian.Pseudoelement

added def CategoryTheory.Abelian.app

added theorem CategoryTheory.Abelian.app_hom

added theorem CategoryTheory.Abelian.pseudoEqual_refl

added theorem CategoryTheory.Abelian.pseudoEqual_symm

added theorem CategoryTheory.Abelian.pseudoEqual_trans