Commit 2022-04-12 12:36 4b45a714

View on Github →

feat(counterexamples/pseudoelement): add counterexample to uniqueness in category_theory.abelian.pseudoelement.pseudo_pullback (#13387) Borceux claims that the pseudoelement constructed in category_theory.abelian.pseudoelement.pseudo_pullback is unique. We show here that this claim is false.

Estimated changes

Created counterexamples/pseudoelement.lean

added theorem category_theory.abelian.pseudoelement.exist_ne_and_fst_eq_fst_and_snd_eq_snd

added theorem category_theory.abelian.pseudoelement.fst_mk_x_eq_fst_mk_y

added theorem category_theory.abelian.pseudoelement.fst_x_pseudo_eq_fst_y

added theorem category_theory.abelian.pseudoelement.mk_x_ne_mk_y

added theorem category_theory.abelian.pseudoelement.snd_mk_x_eq_snd_mk_y

added theorem category_theory.abelian.pseudoelement.snd_x_pseudo_eq_snd_y

added def category_theory.abelian.pseudoelement.x

added theorem category_theory.abelian.pseudoelement.x_not_pseudo_eq

added def category_theory.abelian.pseudoelement.y

Modified src/category_theory/abelian/pseudoelements.lean

added theorem category_theory.abelian.pseudoelement.Module.eq_range_of_pseudoequal