feat(CategoryTheory): semicartesian monoidal categories (#31064)

This PR refactors Cartesian Monoidal Categories through Semicartesian Monoidal Categories. 

There are interesting weaker settings where it is too much to ask the full monoidal structure to be given by the cartesian structure, but reasonable for the monoidal unit to be terminal. A category like this is usually referred to as "Semicartesian".  In semicartesian setting we have `fst (X Y : C) : X ⊗ Y ⟶ X` and  `snd (X Y : C) : X ⊗ Y ⟶ Y` for free, but without their universal property.

https://ncatlab.org/nlab/show/semicartesian+monoidal+category

This PR makes`CartesianMonoidalCategory` an extension of `SemiCartesianMonoidalCategory` 

Some examples of semicartesian but not cartesian monoidal categories:

- The opposite of the category FinInj of finite sets with injections. 
- The category of nominal sets.
- The category of commutative (semi-) rings. 

Personally, I need semicartesian structure for two other downstream projects where the use cases are natural number objects in semicartesian monoidal categories and the category of context of certain type theories.

Author: sinhp

Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean

@@ -45,6 +45,45 @@ universe v v₁ v₂ v₃ u u₁ u₂ u₃
 
 open MonoidalCategory Limits
 
+/-- A monoidal category is semicartesian if the unit for the tensor product is a terminal object. -/
+class SemiCartesianMonoidalCategory (C : Type u) [Category.{v} C] extends MonoidalCategory C where
+  /-- The tensor unit is a terminal object. -/
+  isTerminalTensorUnit : IsTerminal (𝟙_ C)
+  /-- The first projection from the product. -/
+  fst (X Y : C) : X ⊗ Y ⟶ X
+  /-- The second projection from the product. -/
+  snd (X Y : C) : X ⊗ Y ⟶ Y
+  fst_def (X Y : C) : fst X Y = X ◁ isTerminalTensorUnit.from Y ≫ (ρ_ X).hom := by cat_disch
+  snd_def (X Y : C) : snd X Y = isTerminalTensorUnit.from X ▷ Y ≫ (λ_ Y).hom := by cat_disch
+
+namespace SemiCartesianMonoidalCategory
+
+variable {C : Type u} [Category.{v} C] [SemiCartesianMonoidalCategory C]
+
+/-- The unique map to the terminal object. -/
+def toUnit (X : C) : X ⟶ 𝟙_ C := isTerminalTensorUnit.from X
+
+instance (X : C) : Unique (X ⟶ 𝟙_ C) := isTerminalEquivUnique _ _ isTerminalTensorUnit _
+
+lemma default_eq_toUnit (X : C) : default = toUnit X := rfl
+
+/--
+This lemma follows from the preexisting `Unique` instance, but
+it is often convenient to use it directly as `apply toUnit_unique` forcing
+lean to do the necessary elaboration.
+-/
+@[ext]
+lemma toUnit_unique {X : C} (f g : X ⟶ 𝟙_ _) : f = g :=
+  Subsingleton.elim _ _
+
+@[simp] lemma toUnit_unit : toUnit (𝟙_ C) = 𝟙 (𝟙_ C) := toUnit_unique ..
+
+@[reassoc (attr := simp)]
+theorem comp_toUnit {X Y : C} (f : X ⟶ Y) : f ≫ toUnit Y = toUnit X :=
+  toUnit_unique _ _
+
+end SemiCartesianMonoidalCategory
+
 variable (C) in
 /--
 An instance of `CartesianMonoidalCategory C` bundles an explicit choice of a binary
@@ -53,22 +92,18 @@ product of two objects of `C`, and a terminal object in `C`.
 Users should use the monoidal notation: `X ⊗ Y` for the product and `𝟙_ C` for
 the terminal object.
 -/
-class CartesianMonoidalCategory (C : Type u) [Category.{v} C] extends MonoidalCategory C where
-  /-- The tensor unit is a terminal object. -/
-  isTerminalTensorUnit : IsTerminal (𝟙_ C)
-  /-- The first projection from the product. -/
-  fst (X Y : C) : X ⊗ Y ⟶ X
-  /-- The second projection from the product. -/
-  snd (X Y : C) : X ⊗ Y ⟶ Y
+class CartesianMonoidalCategory (C : Type u) [Category.{v} C] extends
+    SemiCartesianMonoidalCategory C where
   /-- The monoidal product is the categorical product. -/
   tensorProductIsBinaryProduct (X Y : C) : IsLimit <| BinaryFan.mk (fst X Y) (snd X Y)
-  fst_def (X Y : C) : fst X Y = X ◁ isTerminalTensorUnit.from Y ≫ (ρ_ X).hom := by cat_disch
-  snd_def (X Y : C) : snd X Y = isTerminalTensorUnit.from X ▷ Y ≫ (λ_ Y).hom := by cat_disch
 
 @[deprecated (since := "2025-05-15")] alias ChosenFiniteProducts := CartesianMonoidalCategory
 
 namespace CartesianMonoidalCategory
 
+export SemiCartesianMonoidalCategory (isTerminalTensorUnit fst snd fst_def snd_def toUnit
+  toUnit_unique toUnit_unit comp_toUnit comp_toUnit_assoc default_eq_toUnit)
+
 variable {C : Type u} [Category.{v} C]
 
 section OfChosenFiniteProducts
@@ -180,7 +215,7 @@ abbrev ofChosenFiniteProducts : CartesianMonoidalCategory C :=
   }
 
 omit 𝒯 in
-/-- Construct an instance of `CartesianMonoidalCategory C` given the existence of finite products
+/-- Constructs an instance of `CartesianMonoidalCategory C` given the existence of finite products
 in `C`. -/
 noncomputable abbrev ofHasFiniteProducts [HasFiniteProducts C] : CartesianMonoidalCategory C :=
   .ofChosenFiniteProducts (getLimitCone (.empty C)) (getLimitCone <| pair · ·)
@@ -194,31 +229,7 @@ variable {C : Type u} [Category.{v} C] [CartesianMonoidalCategory C]
 open MonoidalCategory
 
 /--
-The unique map to the terminal object.
--/
-def toUnit (X : C) : X ⟶ 𝟙_ C := isTerminalTensorUnit.from _
-
-instance (X : C) : Unique (X ⟶ 𝟙_ C) := isTerminalEquivUnique _ _ isTerminalTensorUnit _
-
-lemma default_eq_toUnit (X : C) : default = toUnit X := rfl
-
-/--
-This lemma follows from the preexisting `Unique` instance, but
-it is often convenient to use it directly as `apply toUnit_unique` forcing
-lean to do the necessary elaboration.
--/
-@[ext]
-lemma toUnit_unique {X : C} (f g : X ⟶ 𝟙_ _) : f = g :=
-  Subsingleton.elim _ _
-
-@[simp] lemma toUnit_unit : toUnit (𝟙_ C) = 𝟙 (𝟙_ C) := toUnit_unique ..
-
-@[reassoc (attr := simp)]
-theorem comp_toUnit {X Y : C} (f : X ⟶ Y) : f ≫ toUnit Y = toUnit X :=
-  toUnit_unique _ _
-
-/--
-Construct a morphism to the product given its two components.
+Constructs a morphism to the product given its two components.
 -/
 def lift {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) : T ⟶ X ⊗ Y :=
   (BinaryFan.IsLimit.lift' (tensorProductIsBinaryProduct X Y) f g).1