chore: deprecate monoidalOfHasFiniteProducts (#30684)

Over the summer, this was replaced everywhere with `CartesianMonoidalCategory.ofHasFiniteProducts`, but hadn't been deprecated.

Author: YaelDillies

Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison, Simon Hudon
 -/
-import Mathlib.CategoryTheory.Monoidal.Braided.Basic
+import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
 
@@ -21,8 +21,8 @@ we don't set up either construct as an instance.
 
 ## TODO
 
-Replace `monoidalOfHasFiniteProducts` and `symmetricOfHasFiniteProducts`
-with `CartesianMonoidalCategory.ofHasFiniteProducts`.
+Once we have cocartesian-monoidal categories, replace `monoidalOfHasFiniteCoproducts` and
+`symmetricOfHasFiniteCoproducts` with `CocartesianMonoidalCategory.ofHasFiniteCoproducts`.
 -/
 
 
@@ -39,21 +39,11 @@ open CategoryTheory.Limits
 section
 
 /-- A category with a terminal object and binary products has a natural monoidal structure. -/
+@[deprecated CartesianMonoidalCategory.ofHasFiniteProducts (since := "2025-10-19")]
 def monoidalOfHasFiniteProducts [HasTerminal C] [HasBinaryProducts C] : MonoidalCategory C :=
-  letI : MonoidalCategoryStruct C := {
-    tensorObj := fun X Y ↦ X ⨯ Y
-    whiskerLeft := fun _ _ _ g ↦ Limits.prod.map (𝟙 _) g
-    whiskerRight := fun {_ _} f _ ↦ Limits.prod.map f (𝟙 _)
-    tensorHom := fun f g ↦ Limits.prod.map f g
-    tensorUnit := ⊤_ C
-    associator := prod.associator
-    leftUnitor := fun P ↦ Limits.prod.leftUnitor P
-    rightUnitor := fun P ↦ Limits.prod.rightUnitor P
-  }
-  .ofTensorHom
-    (pentagon := prod.pentagon)
-    (triangle := prod.triangle)
-    (associator_naturality := @prod.associator_naturality _ _ _)
+  have : HasFiniteProducts C := hasFiniteProducts_of_has_binary_and_terminal
+  let +nondep : CartesianMonoidalCategory C := .ofHasFiniteProducts
+  inferInstance
 
 end
 
@@ -65,76 +55,72 @@ attribute [local instance] monoidalOfHasFiniteProducts
 
 open scoped MonoidalCategory
 
-@[ext] theorem unit_ext {X : C} (f g : X ⟶ 𝟙_ C) : f = g := terminal.hom_ext f g
+@[deprecated CartesianMonoidalCategory.toUnit_unique (since := "2025-10-19")]
+theorem unit_ext {X : C} (f g : X ⟶ 𝟙_ C) : f = g := terminal.hom_ext f g
 
-@[ext] theorem tensor_ext {X Y Z : C} (f g : X ⟶ Y ⊗ Z)
+@[deprecated CartesianMonoidalCategory.hom_ext (since := "2025-10-19")]
+theorem tensor_ext {X Y Z : C} (f g : X ⟶ Y ⊗ Z)
     (w₁ : f ≫ prod.fst = g ≫ prod.fst) (w₂ : f ≫ prod.snd = g ≫ prod.snd) : f = g :=
   Limits.prod.hom_ext w₁ w₂
 
-@[simp] theorem tensorUnit : 𝟙_ C = ⊤_ C := rfl
+@[deprecated "This is an implementation detail." (since := "2025-10-19"), simp]
+theorem tensorUnit : 𝟙_ C = ⊤_ C := rfl
 
-@[simp]
+@[deprecated "This is an implementation detail." (since := "2025-10-19"), simp]
 theorem tensorObj (X Y : C) : X ⊗ Y = (X ⨯ Y) :=
   rfl
 
-@[simp]
-theorem tensorHom {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : f ⊗ₘ g = Limits.prod.map f g :=
-  rfl
-
-@[simp]
-theorem whiskerLeft (X : C) {Y Z : C} (f : Y ⟶ Z) : X ◁ f = Limits.prod.map (𝟙 X) f :=
-  rfl
-
-@[simp]
-theorem whiskerRight {X Y : C} (f : X ⟶ Y) (Z : C) : f ▷ Z = Limits.prod.map f (𝟙 Z) :=
-  rfl
-
-@[simp]
+@[deprecated CartesianMonoidalCategory.leftUnitor_hom (since := "2025-10-19"), simp]
 theorem leftUnitor_hom (X : C) : (λ_ X).hom = Limits.prod.snd :=
   rfl
 
-@[simp]
-theorem leftUnitor_inv (X : C) : (λ_ X).inv = prod.lift (terminal.from X) (𝟙 _) :=
-  rfl
-
-@[simp]
+@[deprecated CartesianMonoidalCategory.rightUnitor_hom (since := "2025-10-19"), simp]
 theorem rightUnitor_hom (X : C) : (ρ_ X).hom = Limits.prod.fst :=
   rfl
 
-@[simp]
-theorem rightUnitor_inv (X : C) : (ρ_ X).inv = prod.lift (𝟙 _) (terminal.from X) :=
-  rfl
-
--- We don't mark this as a simp lemma, even though in many particular
--- categories the right-hand side will simplify significantly further.
--- For now, we'll plan to create specialised simp lemmas in each particular category.
+@[deprecated "Use the `CartesianMonoidalCategory.associator_hom_...` lemmas"
+  (since := "2025-10-19"), simp]
 theorem associator_hom (X Y Z : C) :
     (α_ X Y Z).hom =
       prod.lift (Limits.prod.fst ≫ Limits.prod.fst)
         (prod.lift (Limits.prod.fst ≫ Limits.prod.snd) Limits.prod.snd) :=
   rfl
 
+@[deprecated "Use the `CartesianMonoidalCategory.associator_inv_...` lemmas"
+  (since := "2025-10-19")]
 theorem associator_inv (X Y Z : C) :
     (α_ X Y Z).inv =
       prod.lift (prod.lift prod.fst (prod.snd ≫ prod.fst)) (prod.snd ≫ prod.snd) :=
   rfl
 
-@[reassoc] theorem associator_hom_fst (X Y Z : C) :
+set_option linter.deprecated false in
+@[deprecated CartesianMonoidalCategory.associator_hom_fst (since := "2025-10-19")]
+theorem associator_hom_fst (X Y Z : C) :
     (α_ X Y Z).hom ≫ prod.fst = prod.fst ≫ prod.fst := by simp [associator_hom]
 
-@[reassoc] theorem associator_hom_snd_fst (X Y Z : C) :
+set_option linter.deprecated false in
+@[deprecated CartesianMonoidalCategory.associator_hom_snd_fst (since := "2025-10-19")]
+theorem associator_hom_snd_fst (X Y Z : C) :
     (α_ X Y Z).hom ≫ prod.snd ≫ prod.fst = prod.fst ≫ prod.snd := by simp [associator_hom]
 
-@[reassoc] theorem associator_hom_snd_snd (X Y Z : C) :
+set_option linter.deprecated false in
+@[deprecated CartesianMonoidalCategory.associator_hom_snd_snd (since := "2025-10-19")]
+theorem associator_hom_snd_snd (X Y Z : C) :
     (α_ X Y Z).hom ≫ prod.snd ≫ prod.snd = prod.snd := by simp [associator_hom]
 
-@[reassoc] theorem associator_inv_fst_fst (X Y Z : C) :
+set_option linter.deprecated false in
+@[deprecated CartesianMonoidalCategory.associator_inv_fst_fst (since := "2025-10-19")]
+theorem associator_inv_fst_fst (X Y Z : C) :
     (α_ X Y Z).inv ≫ prod.fst ≫ prod.fst = prod.fst := by simp [associator_inv]
 
-@[reassoc] theorem associator_inv_fst_snd (X Y Z : C) :
+set_option linter.deprecated false in
+@[deprecated CartesianMonoidalCategory.associator_inv_fst_snd (since := "2025-10-19")]
+theorem associator_inv_fst_snd (X Y Z : C) :
     (α_ X Y Z).inv ≫ prod.fst ≫ prod.snd = prod.snd ≫ prod.fst := by simp [associator_inv]
 
-@[reassoc] theorem associator_inv_snd (X Y Z : C) :
+set_option linter.deprecated false in
+@[deprecated CartesianMonoidalCategory.associator_inv_snd (since := "2025-10-19")]
+theorem associator_inv_snd (X Y Z : C) :
     (α_ X Y Z).inv ≫ prod.snd = prod.snd ≫ prod.snd := by simp [associator_inv]
 
 end monoidalOfHasFiniteProducts
@@ -145,16 +131,15 @@ attribute [local instance] monoidalOfHasFiniteProducts
 
 open MonoidalCategory
 
+set_option linter.deprecated false in
 /-- The monoidal structure coming from finite products is symmetric.
 -/
-@[simps]
-def symmetricOfHasFiniteProducts [HasTerminal C] [HasBinaryProducts C] : SymmetricCategory C where
-  braiding X Y := Limits.prod.braiding X Y
-  braiding_naturality_left f X := by simp
-  braiding_naturality_right X _ _ f := by simp
-  hexagon_forward X Y Z := by dsimp [monoidalOfHasFiniteProducts.associator_hom]; simp
-  hexagon_reverse X Y Z := by dsimp [monoidalOfHasFiniteProducts.associator_inv]; simp
-  symmetry X Y := by simp
+@[deprecated CartesianMonoidalCategory.toSymmetricCategory (since := "2025-10-19"), simps!]
+def symmetricOfHasFiniteProducts [HasTerminal C] [HasBinaryProducts C] : SymmetricCategory C :=
+  have : HasFiniteProducts C := hasFiniteProducts_of_has_binary_and_terminal
+  let : CartesianMonoidalCategory C := .ofHasFiniteProducts
+  let +nondep : BraidedCategory C := .ofCartesianMonoidalCategory
+  inferInstance
 
 end
 
@@ -256,54 +241,69 @@ end
 
 namespace monoidalOfHasFiniteProducts
 
-attribute [local instance] monoidalOfHasFiniteProducts
-
 variable {C}
 variable {D : Type*} [Category D] (F : C ⥤ D)
   [HasTerminal C] [HasBinaryProducts C]
   [HasTerminal D] [HasBinaryProducts D]
 
+set_option linter.deprecated false in
 attribute [local simp] associator_hom_fst
-instance : F.OplaxMonoidal where
-  η := terminalComparison F
-  δ X Y := prodComparison F X Y
-  δ_natural_left _ _ := by simp [prodComparison_natural]
-  δ_natural_right _ _ := by simp [prodComparison_natural]
-  oplax_associativity _ _ _ := by
-    dsimp
-    ext
-    · dsimp
-      simp only [Category.assoc, prod.map_fst, Category.comp_id, prodComparison_fst, ←
-        Functor.map_comp]
-      erw [associator_hom_fst, associator_hom_fst]
-      simp
-    · dsimp
-      simp only [Category.assoc, prod.map_snd, prodComparison_snd_assoc, prodComparison_fst,
-        ← Functor.map_comp]
-      erw [associator_hom_snd_fst, associator_hom_snd_fst]
-      simp
-    · dsimp
-      simp only [Category.assoc, prod.map_snd, prodComparison_snd_assoc, prodComparison_snd, ←
-        Functor.map_comp]
-      erw [associator_hom_snd_snd, associator_hom_snd_snd]
-      simp
-  oplax_left_unitality _ := by ext; simp [← Functor.map_comp]
-  oplax_right_unitality _ := by ext; simp [← Functor.map_comp]
+@[deprecated Functor.OplaxMonoidal.ofChosenFiniteProducts (since := "2025-10-19")]
+instance :
+    have : HasFiniteProducts C := hasFiniteProducts_of_has_binary_and_terminal
+    have : HasFiniteProducts D := hasFiniteProducts_of_has_binary_and_terminal
+    let : CartesianMonoidalCategory C := .ofHasFiniteProducts
+    let : CartesianMonoidalCategory D := .ofHasFiniteProducts
+    F.OplaxMonoidal := by extract_lets; exact .ofChosenFiniteProducts F
 
 open Functor.OplaxMonoidal
 
-lemma η_eq : η F = terminalComparison F := rfl
-lemma δ_eq (X Y : C) : δ F X Y = prodComparison F X Y := rfl
+@[deprecated "No replacement" (since := "2025-10-19")]
+lemma η_eq :
+    have : HasFiniteProducts C := hasFiniteProducts_of_has_binary_and_terminal
+    have : HasFiniteProducts D := hasFiniteProducts_of_has_binary_and_terminal
+    let : CartesianMonoidalCategory C := .ofHasFiniteProducts
+    let : CartesianMonoidalCategory D := .ofHasFiniteProducts
+    η F = terminalComparison F := rfl
+
+@[deprecated "No replacement" (since := "2025-10-19")]
+lemma δ_eq (X Y : C) :
+    have : HasFiniteProducts C := hasFiniteProducts_of_has_binary_and_terminal
+    have : HasFiniteProducts D := hasFiniteProducts_of_has_binary_and_terminal
+    let : CartesianMonoidalCategory C := .ofHasFiniteProducts
+    let : CartesianMonoidalCategory D := .ofHasFiniteProducts
+    δ F X Y = prodComparison F X Y := rfl
 
 variable [PreservesLimit (Functor.empty.{0} C) F]
   [PreservesLimitsOfShape (Discrete WalkingPair) F]
 
-instance : IsIso (η F) := by dsimp [η_eq]; infer_instance
-instance (X Y : C) : IsIso (δ F X Y) := by dsimp [δ_eq]; infer_instance
+set_option linter.deprecated false in
+@[deprecated inferInstance (since := "2025-10-19")]
+instance :
+    have : HasFiniteProducts C := hasFiniteProducts_of_has_binary_and_terminal
+    have : HasFiniteProducts D := hasFiniteProducts_of_has_binary_and_terminal
+    let : CartesianMonoidalCategory C := .ofHasFiniteProducts
+    let : CartesianMonoidalCategory D := .ofHasFiniteProducts
+    IsIso (η F) := by dsimp [η_eq]; infer_instance
+
+set_option linter.deprecated false in
+@[deprecated inferInstance (since := "2025-10-19")]
+instance (X Y : C) :
+    have : HasFiniteProducts C := hasFiniteProducts_of_has_binary_and_terminal
+    have : HasFiniteProducts D := hasFiniteProducts_of_has_binary_and_terminal
+    let : CartesianMonoidalCategory C := .ofHasFiniteProducts
+    let : CartesianMonoidalCategory D := .ofHasFiniteProducts
+    IsIso (δ F X Y) := by dsimp [δ_eq]; infer_instance
 
 /-- Promote a functor that preserves finite products to a monoidal functor between
 categories equipped with the monoidal category structure given by finite products. -/
-instance : F.Monoidal := .ofOplaxMonoidal F
+@[deprecated Functor.Monoidal.ofChosenFiniteProducts (since := "2025-10-19")]
+instance :
+    have : HasFiniteProducts C := hasFiniteProducts_of_has_binary_and_terminal
+    have : HasFiniteProducts D := hasFiniteProducts_of_has_binary_and_terminal
+    let : CartesianMonoidalCategory C := .ofHasFiniteProducts
+    let : CartesianMonoidalCategory D := .ofHasFiniteProducts
+    F.Monoidal := by extract_lets; exact .ofOplaxMonoidal F
 
 end monoidalOfHasFiniteProducts