Commit 2023-06-15 07:21 379a2ae3

View on Github →

feat: port CategoryTheory.Closed.Functor (#4922)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Closed/Functor.lean

added def CategoryTheory.cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts

added theorem CategoryTheory.coev_expComparison

added def CategoryTheory.expComparison

added theorem CategoryTheory.expComparison_ev

added theorem CategoryTheory.expComparison_iso_of_frobeniusMorphism_iso

added theorem CategoryTheory.expComparison_whiskerLeft

added def CategoryTheory.frobeniusMorphism

added theorem CategoryTheory.frobeniusMorphism_iso_of_expComparison_iso

added theorem CategoryTheory.frobeniusMorphism_mate

added theorem CategoryTheory.uncurry_expComparison

Modified Mathlib/CategoryTheory/Iso.lean

modified theorem CategoryTheory.asIso_hom

modified theorem CategoryTheory.asIso_inv

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

Modified Mathlib/CategoryTheory/NatIso.lean

modified theorem CategoryTheory.NatIso.isIso_inv_app

modified theorem CategoryTheory.NatIso.naturality_1'

modified theorem CategoryTheory.NatIso.naturality_2'