From eae0510503794feb937b042e756f2f98f75a8222 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 22 May 2022 14:41:20 +0000 Subject: [PATCH] feat(category_theory/natural_isomorphism): a simp lemma cancelling inverses (#14299) I am not super happy to be adding lemmas like this, because it feels like better designed simp normal forms (or something else) could just avoid the need. However my efforts to think about this keep getting stuck on the shift functor hole we're in, and this lemma is useful in the meantime to dig my way out of it. :-) Co-authored-by: Scott Morrison --- src/category_theory/natural_isomorphism.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/category_theory/natural_isomorphism.lean b/src/category_theory/natural_isomorphism.lean index d66413d606f11..db6947c5a6bcb 100644 --- a/src/category_theory/natural_isomorphism.lean +++ b/src/category_theory/natural_isomorphism.lean @@ -155,6 +155,10 @@ instance is_iso_app_of_is_iso (α : F ⟶ G) [is_iso α] (X) : is_iso (α.app X) @[simp] lemma is_iso_inv_app (α : F ⟶ G) [is_iso α] (X) : (inv α).app X = inv (α.app X) := by { ext, rw ←nat_trans.comp_app, simp, } +@[simp] lemma inv_map_inv_app (F : C ⥤ D ⥤ E) {X Y : C} (e : X ≅ Y) (Z : D) : + inv ((F.map e.inv).app Z) = (F.map e.hom).app Z := +by { ext, simp, } + /-- Construct a natural isomorphism between functors by giving object level isomorphisms, and checking naturality only in the forward direction.