Commit 2024-11-14 20:44 daed990b

View on Github →

refactor: change CartesianClosed to rely on ChosenFiniteProducts (#17766) Change the API for CartesianClosed categories: they are now defined as MonoidalClosed for the monoidal structure inherited by a ChosenFiniteProducts instance. They were previously relying on HasFiniteProducts.

Estimated changes

Modified Mathlib/CategoryTheory/Closed/Cartesian.lean

modified def CategoryTheory.CartesianClosed.curry

modified theorem CategoryTheory.CartesianClosed.curry_eq

modified theorem CategoryTheory.CartesianClosed.curry_eq_iff

modified theorem CategoryTheory.CartesianClosed.curry_injective

modified theorem CategoryTheory.CartesianClosed.curry_natural_left

modified theorem CategoryTheory.CartesianClosed.curry_natural_right

modified theorem CategoryTheory.CartesianClosed.eq_curry_iff

modified theorem CategoryTheory.CartesianClosed.homEquiv_apply_eq

modified def CategoryTheory.CartesianClosed.mk

modified def CategoryTheory.CartesianClosed.uncurry

modified theorem CategoryTheory.CartesianClosed.uncurry_curry

modified theorem CategoryTheory.CartesianClosed.uncurry_eq

modified theorem CategoryTheory.CartesianClosed.uncurry_injective

modified def CategoryTheory.binaryProductExponentiable

modified theorem CategoryTheory.exp.ev_coev

deleted def CategoryTheory.expTerminalIsoSelf

deleted def CategoryTheory.expTerminalNatIso

added def CategoryTheory.expUnitIsoSelf

added def CategoryTheory.expUnitNatIso

modified def CategoryTheory.mulZero

modified theorem CategoryTheory.pre_id

modified def CategoryTheory.terminalExponentiable

modified def CategoryTheory.zeroMul

Modified Mathlib/CategoryTheory/Closed/Functor.lean

Modified Mathlib/CategoryTheory/Closed/Ideal.lean

modified theorem CategoryTheory.bijection_natural

modified def CategoryTheory.cartesianClosedOfReflective

modified theorem CategoryTheory.prodComparison_iso

added def CategoryTheory.reflectiveChosenFiniteProducts

modified theorem CategoryTheory.reflective_products

Modified Mathlib/CategoryTheory/Closed/Types.lean

deleted def CategoryTheory.Types.binaryProductAdjunction

added def CategoryTheory.Types.tensorProductAdjunction

Modified Mathlib/CategoryTheory/Closed/Zero.lean

deleted def CategoryTheory.uniqueHomsetOfInitialIsoTerminal

added def CategoryTheory.uniqueHomsetOfInitialIsoUnit

Modified Mathlib/CategoryTheory/Sites/CartesianClosed.lean

Modified Mathlib/Condensed/CartesianClosed.lean

Modified Mathlib/Condensed/Light/CartesianClosed.lean