Commit 2025-05-07 21:03 1def1b4f

refactor(CategoryTheory): Make ChosenFiniteProducts extend MonoidalCategory (#24399) There are cases where we have an existing monoidal structure on a category, which turns out to be cartesian monoidal in certain situations. The existing design cannot support such scenarios, as the monoidal category instance is currently forced to come from monoidalOfChosenFiniteProducts. We refactor ChosenFiniteProducts to instead extend MonoidalCategory, and to contain extra data that the existing monoidal structure is cartesian. The plan is to rename ChosenFiniteProducts to CartesianMonoidalCategory in a follow up PR. Examples of such cases include

1. If C is a monoidal category, then Cᵒᵖ has a canonical monoidal structure. It is cartesian when e.g. C = Ab.
2. If C is a monoidal category, then Mon_ C has a canonical monoidal structure. It is cartesian when C is. Also see https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Bimon.20C.20.3D.20Mon.20C.20when.20C.20is.20cartesian-monoidal From Toric