Revision #2571 → #3175 · back to history
modifiedExponentiation as right adjoint to product6e223ae980ee
| Field | From #2571 | To #3175 |
|---|
| mathlib.decl | CategoryTheory.exp.adjunction | CategoryTheory.ihom.adjunction |
| mathlib.match_kind | exact | generalization |
| mathlib.module | Mathlib.CategoryTheory.Monoidal.Closed.Cartesian | Mathlib.CategoryTheory.Monoidal.Closed.Basic |
| note | `CategoryTheory.exp.adjunction` is the prod ⊣ exp adjunction in Cartesian closed categories. | `CategoryTheory.ihom.adjunction` gives the `tensorLeft A ⊣ ihom A` adjunction, which specialises to the product ⊣ exp adjunction in a cartesian monoidal category. |
modifiedCartesian closed categoryab285dea869e
| Field | From #2571 | To #3175 |
|---|
| mathlib.decl | CategoryTheory.CartesianClosed | CategoryTheory.MonoidalClosed |
| mathlib.match_kind | exact | generalization |
| mathlib.module | Mathlib.CategoryTheory.Monoidal.Closed.Cartesian | Mathlib.CategoryTheory.Monoidal.Closed.Basic |
| note | `CartesianClosed` is Mathlib's typeclass for CCCs. | The dedicated `CartesianClosed` class was deprecated; cartesian closed categories are now `MonoidalClosed C` with `[CartesianMonoidalCategory C]`. |
| status | formalized | partial |