From eca55c9a248c741d819fb75ec2dcf37f23fc3f29 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 19 Jul 2020 04:53:42 +0000 Subject: [PATCH] feat(category_theory/equivalence): injectivity simp lemmas for equivalences (#3437) Co-authored-by: Scott Morrison --- src/category_theory/equivalence.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/category_theory/equivalence.lean b/src/category_theory/equivalence.lean index f1d6e05698d15..388619c0200a6 100644 --- a/src/category_theory/equivalence.lean +++ b/src/category_theory/equivalence.lean @@ -388,6 +388,20 @@ is_equivalence.mk (equivalence_inverse F) (λ Y, F.fun_obj_preimage_iso Y) (by obviously)) +@[simp] lemma functor_map_inj_iff (e : C ≌ D) {X Y : C} (f g : X ⟶ Y) : e.functor.map f = e.functor.map g ↔ f = g := +begin + split, + { intro w, apply e.functor.map_injective, exact w, }, + { rintro ⟨rfl⟩, refl, } +end + +@[simp] lemma inverse_map_inj_iff (e : C ≌ D) {X Y : D} (f g : X ⟶ Y) : e.inverse.map f = e.inverse.map g ↔ f = g := +begin + split, + { intro w, apply e.inverse.map_injective, exact w, }, + { rintro ⟨rfl⟩, refl, } +end + end equivalence end category_theory