chore: rename ChosenFiniteProducts to CartesianMonoidalCategory (#24390)

Now that `ChosenFiniteProducts` extends `MonoidalCategory`, the name `ChosenFiniteProducts` is less relevant. `CartesianMonoidalCategory` is a better name for this class.

From Toric

Author: YaelDillies

Mathlib.lean

@@ -97,7 +97,7 @@ import Mathlib.Algebra.Category.Grp.Abelian
 import Mathlib.Algebra.Category.Grp.Adjunctions
 import Mathlib.Algebra.Category.Grp.Basic
 import Mathlib.Algebra.Category.Grp.Biproducts
-import Mathlib.Algebra.Category.Grp.ChosenFiniteProducts
+import Mathlib.Algebra.Category.Grp.CartesianMonoidal
 import Mathlib.Algebra.Category.Grp.Colimits
 import Mathlib.Algebra.Category.Grp.EnoughInjectives
 import Mathlib.Algebra.Category.Grp.EpiMono
@@ -1933,11 +1933,6 @@ import Mathlib.CategoryTheory.Category.ULift
 import Mathlib.CategoryTheory.Center.Basic
 import Mathlib.CategoryTheory.Center.Linear
 import Mathlib.CategoryTheory.Center.Localization
-import Mathlib.CategoryTheory.ChosenFiniteProducts
-import Mathlib.CategoryTheory.ChosenFiniteProducts.Cat
-import Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory
-import Mathlib.CategoryTheory.ChosenFiniteProducts.InfSemilattice
-import Mathlib.CategoryTheory.ChosenFiniteProducts.Over
 import Mathlib.CategoryTheory.Closed.Cartesian
 import Mathlib.CategoryTheory.Closed.Enrichment
 import Mathlib.CategoryTheory.Closed.Functor
@@ -2311,12 +2306,17 @@ import Mathlib.CategoryTheory.Monoidal.Bimon_
 import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 import Mathlib.CategoryTheory.Monoidal.Braided.Opposite
 import Mathlib.CategoryTheory.Monoidal.Braided.Reflection
+import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
+import Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
 import Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
 import Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_
 import Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
+import Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
 import Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_
+import Mathlib.CategoryTheory.Monoidal.Cartesian.InfSemilattice
 import Mathlib.CategoryTheory.Monoidal.Cartesian.Mod_
 import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_
+import Mathlib.CategoryTheory.Monoidal.Cartesian.Over
 import Mathlib.CategoryTheory.Monoidal.Category
 import Mathlib.CategoryTheory.Monoidal.Center
 import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
@@ -2453,6 +2453,7 @@ import Mathlib.CategoryTheory.Sites.Abelian
 import Mathlib.CategoryTheory.Sites.Adjunction
 import Mathlib.CategoryTheory.Sites.Canonical
 import Mathlib.CategoryTheory.Sites.CartesianClosed
+import Mathlib.CategoryTheory.Sites.CartesianMonoidal
 import Mathlib.CategoryTheory.Sites.ChosenFiniteProducts
 import Mathlib.CategoryTheory.Sites.Closed
 import Mathlib.CategoryTheory.Sites.Coherent.Basic

Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean renamed to Mathlib/Algebra/Category/Grp/CartesianMonoidal.lean

@@ -26,11 +26,11 @@ def binaryProductLimitCone (G H : Grp.{u}) : LimitCone (pair G H) where
 
 /-- We choose `Grp.of (G × H)` as the product of `G` and `H` and `Grp.of PUnit` as
 the terminal object. -/
-noncomputable instance chosenFiniteProductsGrp : ChosenFiniteProducts Grp.{u} :=
+noncomputable instance cartesianMonoidalCategoryGrp : CartesianMonoidalCategory Grp.{u} :=
   .ofChosenFiniteProducts ⟨_, (isZero_of_subsingleton (Grp.of PUnit.{u + 1})).isTerminal⟩
     fun G H ↦ binaryProductLimitCone G H
 
-noncomputable instance : BraidedCategory Grp.{u} := .ofChosenFiniteProducts
+noncomputable instance : BraidedCategory Grp.{u} := .ofCartesianMonoidalCategory
 
 noncomputable instance : (forget Grp.{u}).Braided := .ofChosenFiniteProducts _
 
@@ -56,11 +56,11 @@ def binaryProductLimitCone (G H : AddGrp.{u}) : LimitCone (pair G H) where
 
 /-- We choose `AddGrp.of (G × H)` as the product of `G` and `H` and `AddGrp.of PUnit` as
 the terminal object. -/
-noncomputable instance chosenFiniteProductsAddGrp : ChosenFiniteProducts AddGrp.{u} :=
+noncomputable instance cartesianMonoidalCategoryAddGrp : CartesianMonoidalCategory AddGrp.{u} :=
   .ofChosenFiniteProducts ⟨_, (isZero_of_subsingleton (AddGrp.of PUnit.{u + 1})).isTerminal⟩
     fun G H ↦ binaryProductLimitCone G H
 
-noncomputable instance : BraidedCategory AddGrp.{u} := .ofChosenFiniteProducts
+noncomputable instance : BraidedCategory AddGrp.{u} := .ofCartesianMonoidalCategory
 
 noncomputable instance : (forget AddGrp.{u}).Braided := .ofChosenFiniteProducts _
 
@@ -86,11 +86,11 @@ def binaryProductLimitCone (G H : CommGrp.{u}) : LimitCone (pair G H) where
 
 /-- We choose `CommGrp.of (G × H)` as the product of `G` and `H` and `CommGrp.of PUnit` as
 the terminal object. -/
-noncomputable instance chosenFiniteProductsCommGrp : ChosenFiniteProducts CommGrp.{u} :=
+noncomputable instance cartesianMonoidalCategoryCommGrp : CartesianMonoidalCategory CommGrp.{u} :=
   .ofChosenFiniteProducts ⟨_, (isZero_of_subsingleton (CommGrp.of PUnit.{u + 1})).isTerminal⟩
     fun G H ↦ binaryProductLimitCone G H
 
-noncomputable instance : BraidedCategory CommGrp.{u} := .ofChosenFiniteProducts
+noncomputable instance : BraidedCategory CommGrp.{u} := .ofCartesianMonoidalCategory
 
 noncomputable instance : (forget CommGrp.{u}).Braided := .ofChosenFiniteProducts _
 
@@ -109,13 +109,16 @@ namespace AddCommGrp
 
 /-- We choose `AddCommGrp.of (G × H)` as the product of `G` and `H` and `AddGrp.of PUnit` as
 the terminal object. -/
-noncomputable def chosenFiniteProductsAddCommGrp : ChosenFiniteProducts AddCommGrp.{u} :=
+noncomputable def cartesianMonoidalCategoryAddCommGrp : CartesianMonoidalCategory AddCommGrp.{u} :=
   .ofChosenFiniteProducts ⟨_, (isZero_of_subsingleton (AddCommGrp.of PUnit.{u + 1})).isTerminal⟩
     fun G H ↦ binaryProductLimitCone G H
 
-attribute [local instance] chosenFiniteProductsAddCommGrp
+@[deprecated (since := "2025-05-15")]
+alias chosenFiniteProductsAddCommGrp := cartesianMonoidalCategoryAddCommGrp
 
-noncomputable instance : BraidedCategory AddCommGrp.{u} := .ofChosenFiniteProducts
+attribute [local instance] cartesianMonoidalCategoryAddCommGrp
+
+noncomputable instance : BraidedCategory AddCommGrp.{u} := .ofCartesianMonoidalCategory
 
 noncomputable instance : (forget AddCommGrp.{u}).Braided := .ofChosenFiniteProducts _
 

Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean

@@ -3,7 +3,7 @@ Copyright (c) 2025 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-import Mathlib.Algebra.Category.Grp.ChosenFiniteProducts
+import Mathlib.Algebra.Category.Grp.CartesianMonoidal
 import Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
 import Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
 import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
@@ -40,11 +40,11 @@ variable {C : Type u} [Category.{v} C] [Preadditive C] [HasFiniteBiproducts C]
 namespace leftExactFunctorForgetEquivalence
 
 attribute [local instance] hasFiniteProducts_of_hasFiniteBiproducts
-attribute [local instance] AddCommGrp.chosenFiniteProductsAddCommGrp
+attribute [local instance] AddCommGrp.cartesianMonoidalCategoryAddCommGrp
 
-private noncomputable local instance : ChosenFiniteProducts C := .ofHasFiniteProducts
+private noncomputable local instance : CartesianMonoidalCategory C := .ofHasFiniteProducts
 
-private noncomputable local instance : BraidedCategory C := .ofChosenFiniteProducts
+private noncomputable local instance : BraidedCategory C := .ofCartesianMonoidalCategory
 
 /-- Implementation, see `leftExactFunctorForgetEquivalence`. -/
 noncomputable def inverseAux : (C ⥤ₗ Type v) ⥤ C ⥤ AddCommGrp.{v} :=

Mathlib/AlgebraicGeometry/Limits.lean

@@ -646,7 +646,7 @@ instance [IsAffine X] [IsAffine Y] : IsAffine (X ⨿ Y) :=
 
 end Coproduct
 
-instance : ChosenFiniteProducts Scheme := .ofHasFiniteProducts
-instance : BraidedCategory Scheme := .ofChosenFiniteProducts
+instance : CartesianMonoidalCategory Scheme := .ofHasFiniteProducts
+instance : BraidedCategory Scheme := .ofCartesianMonoidalCategory
 
 end AlgebraicGeometry

Mathlib/AlgebraicGeometry/Pullbacks.lean

@@ -3,11 +3,11 @@ Copyright (c) 2022 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
+import Mathlib.AlgebraicGeometry.AffineScheme
 import Mathlib.AlgebraicGeometry.Gluing
 import Mathlib.CategoryTheory.Limits.Opposites
-import Mathlib.AlgebraicGeometry.AffineScheme
 import Mathlib.CategoryTheory.Limits.Shapes.Diagonal
-import Mathlib.CategoryTheory.ChosenFiniteProducts.Over
+import Mathlib.CategoryTheory.Monoidal.Cartesian.Over
 
 /-!
 # Fibred products of schemes
@@ -696,12 +696,12 @@ lemma diagonal_Spec_map :
 
 end Spec
 
-section ChosenFiniteProducts
+section CartesianMonoidalCategory
 variable {S : Scheme}
 
-instance : ChosenFiniteProducts (Over S) := Over.chosenFiniteProducts _
-instance : BraidedCategory (Over S) := .ofChosenFiniteProducts
+instance : CartesianMonoidalCategory (Over S) := Over.cartesianMonoidalCategory _
+instance : BraidedCategory (Over S) := .ofCartesianMonoidalCategory
 
-end ChosenFiniteProducts
+end CartesianMonoidalCategory
 
 end AlgebraicGeometry

Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou, Jack McKoen
 -/
 import Mathlib.AlgebraicTopology.SimplicialSet.Basic
-import Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory
+import Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
 import Mathlib.CategoryTheory.Monoidal.Types.Basic
 
 /-!
@@ -25,8 +25,8 @@ open Simplicial CategoryTheory MonoidalCategory
 
 namespace SSet
 
-noncomputable instance : ChosenFiniteProducts SSet.{u} :=
-  (inferInstance : ChosenFiniteProducts (SimplexCategoryᵒᵖ ⥤ Type u))
+noncomputable instance : CartesianMonoidalCategory SSet.{u} :=
+  (inferInstance : CartesianMonoidalCategory (SimplexCategoryᵒᵖ ⥤ Type u))
 
 @[simp]
 lemma leftUnitor_hom_app_apply (K : SSet.{u}) {Δ : SimplexCategoryᵒᵖ} (x : (𝟙_ _ ⊗ K).obj Δ) :

Mathlib/CategoryTheory/Closed/Cartesian.lean

@@ -3,21 +3,13 @@ Copyright (c) 2020 Bhavik Mehta, Edward Ayers, Thomas Read. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Edward Ayers, Thomas Read
 -/
-import Mathlib.CategoryTheory.EpiMono
-import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
-import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
-import Mathlib.CategoryTheory.ChosenFiniteProducts
-import Mathlib.CategoryTheory.Adjunction.Limits
-import Mathlib.CategoryTheory.Adjunction.Mates
 import Mathlib.CategoryTheory.Closed.Monoidal
+import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
 
 /-!
 # Cartesian closed categories
 
-Given a category with chosen finite products, the cartesian monoidal structure is provided by the
-instance `monoidalOfChosenFiniteProducts`.
-
-We define exponentiable objects to be closed objects with respect to this monoidal structure,
+We define exponentiable objects to be closed objects in a cartesian monoidal category,
 i.e. `(X × -)` is a left adjoint.
 
 We say a category is cartesian closed if every object is exponentiable
@@ -27,10 +19,10 @@ Show that exponential forms a difunctor and define the exponential comparison mo
 
 ## Implementation Details
 
-Cartesian closed categories require a `ChosenFiniteProducts` instance. If one whishes to state that
-a category that `hasFiniteProducts` is cartesian closed, they should first promote the
-`hasFiniteProducts` instance to a `ChosenFiniteProducts` one using
-`CategoryTheory.ChosenFiniteProducts.ofFiniteProducts`.
+Cartesian closed categories require a `CartesianMonoidalCategory` instance. If one wishes to state
+that a category that `hasFiniteProducts` is cartesian closed, they should first promote the
+`hasFiniteProducts` instance to a `CartesianMonoidalCategory` one using
+`CategoryTheory.ofChosenFiniteProducts`.
 
 ## TODO
 Some of the results here are true more generally for closed objects and
@@ -42,54 +34,45 @@ universe v v₂ u u₂
 
 namespace CategoryTheory
 
-open Category Limits MonoidalCategory
+open Category Limits MonoidalCategory CartesianMonoidalCategory
 
-/-- An object `X` is *exponentiable* if `(X × -)` is a left adjoint.
-We define this as being `Closed` in the cartesian monoidal structure.
--/
+variable {C : Type u} [Category.{v} C] [CartesianMonoidalCategory C] {X X' Y Y' Z : C}
 
-abbrev Exponentiable {C : Type u} [Category.{v} C] [ChosenFiniteProducts C] (X : C) :=
-  Closed X
+/-- An object `X` is *exponentiable* if `(X × -)` is a left adjoint.
+We define this as being `Closed` in the cartesian monoidal structure. -/
+abbrev Exponentiable (X : C) := Closed X
 
 /-- Constructor for `Exponentiable X` which takes as an input an adjunction
 `MonoidalCategory.tensorLeft X ⊣ exp` for some functor `exp : C ⥤ C`. -/
-abbrev Exponentiable.mk {C : Type u} [Category.{v} C] [ChosenFiniteProducts C] (X : C)
-    (exp : C ⥤ C) (adj : MonoidalCategory.tensorLeft X ⊣ exp) :
-    Exponentiable X where
+abbrev Exponentiable.mk (X : C) (exp : C ⥤ C) (adj : tensorLeft X ⊣ exp) : Exponentiable X where
   rightAdj := exp
   adj := adj
 
 /-- If `X` and `Y` are exponentiable then `X ⨯ Y` is.
 This isn't an instance because it's not usually how we want to construct exponentials, we'll usually
 prove all objects are exponential uniformly.
 -/
-def binaryProductExponentiable {C : Type u} [Category.{v} C] [ChosenFiniteProducts C] {X Y : C}
-    (hX : Exponentiable X) (hY : Exponentiable Y) : Exponentiable (X ⊗ Y) :=
-  tensorClosed hX hY
+def binaryProductExponentiable (hX : Exponentiable X) (hY : Exponentiable Y) :
+    Exponentiable (X ⊗ Y) := tensorClosed hX hY
 
 /-- The terminal object is always exponentiable.
 This isn't an instance because most of the time we'll prove cartesian closed for all objects
 at once, rather than just for this one.
 -/
-def terminalExponentiable {C : Type u} [Category.{v} C] [ChosenFiniteProducts C] :
-    Exponentiable (𝟙_ C) :=
-  unitClosed
+def terminalExponentiable : Exponentiable (𝟙_ C) := unitClosed
 
+variable (C) in
 /-- A category `C` is cartesian closed if it has finite products and every object is exponentiable.
-We define this as `monoidal_closed` with respect to the cartesian monoidal structure.
--/
-abbrev CartesianClosed (C : Type u) [Category.{v} C] [ChosenFiniteProducts C] :=
-  MonoidalClosed C
+We define this as `MonoidalClosed` with respect to the cartesian monoidal structure. -/
+abbrev CartesianClosed := MonoidalClosed C
 
+variable (C) in
 -- Porting note: added to ease the port of `CategoryTheory.Closed.Types`
 /-- Constructor for `CartesianClosed C`. -/
-def CartesianClosed.mk (C : Type u) [Category.{v} C] [ChosenFiniteProducts C]
-    (exp : ∀ (X : C), Exponentiable X) :
-    CartesianClosed C where
+def CartesianClosed.mk (exp : ∀ (X : C), Exponentiable X) : CartesianClosed C where
   closed X := exp X
 
-variable {C : Type u} [Category.{v} C] (A B : C) {X X' Y Y' Z : C}
-variable [ChosenFiniteProducts C] [Exponentiable A]
+variable (A B : C) [Exponentiable A]
 
 /-- This is (-)^A. -/
 abbrev exp : C ⥤ C :=
@@ -238,7 +221,7 @@ def expUnitIsoSelf [Exponentiable (𝟙_ C)] : (𝟙_ C) ⟹ X ≅ X :=
 
 /-- The internal element which points at the given morphism. -/
 def internalizeHom (f : A ⟶ Y) : 𝟙_ C ⟶ A ⟹ Y :=
-  CartesianClosed.curry (ChosenFiniteProducts.fst _ _ ≫ f)
+  CartesianClosed.curry (fst _ _ ≫ f)
 
 section Pre
 
@@ -284,10 +267,10 @@ def internalHom [CartesianClosed C] : Cᵒᵖ ⥤ C ⥤ C where
 /-- If an initial object `I` exists in a CCC, then `A ⨯ I ≅ I`. -/
 @[simps]
 def zeroMul {I : C} (t : IsInitial I) : A ⊗ I ≅ I where
-  hom := ChosenFiniteProducts.snd _ _
+  hom := snd _ _
   inv := t.to _
   hom_inv_id := by
-    have : ChosenFiniteProducts.snd A I = CartesianClosed.uncurry (t.to _) := by
+    have : snd A I = CartesianClosed.uncurry (t.to _) := by
       rw [← curry_eq_iff]
       apply t.hom_ext
     rw [this, ← uncurry_natural_right, ← eq_curry_iff]
@@ -334,7 +317,7 @@ exponentiable object is an isomorphism.
 -/
 theorem strict_initial {I : C} (t : IsInitial I) (f : A ⟶ I) : IsIso f := by
   haveI : Mono f := by
-    rw [← ChosenFiniteProducts.lift_snd (𝟙 A) f, ← zeroMul_hom t]
+    rw [← lift_snd (𝟙 A) f, ← zeroMul_hom t]
     exact mono_comp _ _
   haveI : IsSplitEpi f := IsSplitEpi.mk' ⟨t.to _, t.hom_ext _ _⟩
   apply isIso_of_mono_of_isSplitEpi
@@ -356,7 +339,7 @@ variable {D : Type u₂} [Category.{v₂} D]
 
 section Functor
 
-variable [ChosenFiniteProducts D]
+variable [CartesianMonoidalCategory D]
 
 /-- Transport the property of being cartesian closed across an equivalence of categories.
 

Mathlib/CategoryTheory/Closed/Functor.lean

@@ -34,13 +34,13 @@ noncomputable section
 
 namespace CategoryTheory
 
-open Category CartesianClosed MonoidalCategory ChosenFiniteProducts TwoSquare
+open Category CartesianClosed MonoidalCategory CartesianMonoidalCategory TwoSquare
 
 universe v u u'
 
 variable {C : Type u} [Category.{v} C]
 variable {D : Type u'} [Category.{v} D]
-variable [ChosenFiniteProducts C] [ChosenFiniteProducts D]
+variable [CartesianMonoidalCategory C] [CartesianMonoidalCategory D]
 variable (F : C ⥤ D) {L : D ⥤ C}
 
 /-- The Frobenius morphism for an adjunction `L ⊣ F` at `A` is given by the morphism