feat(CategoryTheory): variants of Functor.flipCompEvaluation (#17407)

Co-authored-by: Markus Himmel <[email protected]>
leanprover-community · Oct 7, 2024 · e260f25 · e260f25
1 parent 3ee779f
commit e260f25
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 2 deletions.
diff --git a/Mathlib/CategoryTheory/Functor/Currying.lean b/Mathlib/CategoryTheory/Functor/Currying.lean
@@ -3,6 +3,7 @@ Copyright (c) 2017 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+import Mathlib.CategoryTheory.EqToHom
 import Mathlib.CategoryTheory.Products.Basic
 
 /-!

diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean
@@ -3,6 +3,7 @@ Copyright (c) 2018 Michael Jendrusch. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Jendrusch, Kim Morrison, Bhavik Mehta, Jakob von Raumer
 -/
+import Mathlib.CategoryTheory.EqToHom
 import Mathlib.CategoryTheory.Functor.Trifunctor
 import Mathlib.CategoryTheory.Products.Basic
 

diff --git a/Mathlib/CategoryTheory/Products/Basic.lean b/Mathlib/CategoryTheory/Products/Basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2017 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stephen Morgan, Kim Morrison
 -/
-import Mathlib.CategoryTheory.EqToHom
 import Mathlib.CategoryTheory.Functor.Const
 import Mathlib.CategoryTheory.Opposites
 import Mathlib.Data.Prod.Basic
@@ -296,7 +295,18 @@ end Equivalence
 /-- `F.flip` composed with evaluation is the same as evaluating `F`. -/
 @[simps!]
 def flipCompEvaluation (F : A ⥤ B ⥤ C) (a) : F.flip ⋙ (evaluation _ _).obj a ≅ F.obj a :=
-  NatIso.ofComponents fun b => eqToIso rfl
+  NatIso.ofComponents fun b => Iso.refl _
+
+theorem flip_comp_evaluation (F : A ⥤ B ⥤ C) (a) : F.flip ⋙ (evaluation _ _).obj a = F.obj a :=
+  rfl
+
+/-- `F` composed with evaluation is the same as evaluating `F.flip`. -/
+@[simps!]
+def compEvaluation (F : A ⥤ B ⥤ C) (b) : F ⋙ (evaluation _ _).obj b ≅ F.flip.obj b :=
+  NatIso.ofComponents fun a => Iso.refl _
+
+theorem comp_evaluation (F : A ⥤ B ⥤ C) (b) : F ⋙ (evaluation _ _).obj b = F.flip.obj b :=
+  rfl
 
 variable (A B C)