chore(CategoryTheory): rename monoidal transport constructions (#31022)

+ Rename `symmetricCategory/monoidalLinear/exactPairingOf(Fully)Faithful` to `SymmetricCategory.ofFaithful` etc. following [CategoryTheory.BraidedCategory.ofFaithful](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Monoidal/Braided/Basic.html#CategoryTheory.BraidedCategory.ofFaithful).

+ Remove some `noncomputable section`s and make some noncomputable defs computable.

Author: alreadydone

Mathlib/Algebra/Category/AlgCat/Symmetric.lean

@@ -31,6 +31,6 @@ instance : BraidedCategory (AlgCat.{u} R) :=
 instance : (forget₂ (AlgCat R) (ModuleCat R)).Braided where
 
 instance instSymmetricCategory : SymmetricCategory (AlgCat.{u} R) :=
-  symmetricCategoryOfFaithful (forget₂ (AlgCat R) (ModuleCat R))
+  .ofFaithful (forget₂ (AlgCat R) (ModuleCat R))
 
 end AlgCat

Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

@@ -363,6 +363,9 @@ theorem hom_inv_associator {M N K : ModuleCat.{u} R} :
 
 namespace MonoidalCategory
 
+@[deprecated (since := "2025-10-29")] alias tensorObj := tensorObj_carrier
+@[deprecated (since := "2025-10-29")] alias tensorObj_def := tensorObj_carrier
+
 @[simp]
 theorem tensorHom_tmul {K L M N : ModuleCat.{u} R} (f : K ⟶ L) (g : M ⟶ N) (k : K) (m : M) :
     (f ⊗ₘ g) (k ⊗ₜ m) = f k ⊗ₜ g m :=

Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean

@@ -113,7 +113,7 @@ instance : BraidedCategory (ModuleCat.{u} R) :=
 instance : equivalenceSemimoduleCat (R := R).functor.Braided where
 
 instance symmetricCategory : SymmetricCategory (ModuleCat.{u} R) :=
-  symmetricCategoryOfFaithful equivalenceSemimoduleCat.functor
+  .ofFaithful equivalenceSemimoduleCat.functor
 
 @[simp]
 theorem braiding_hom_apply {M N : ModuleCat.{u} R} (m : M) (n : N) :

Mathlib/CategoryTheory/Action/Monoidal.lean

@@ -93,7 +93,7 @@ instance : (Action.forget V G).Braided where
 end
 
 instance [SymmetricCategory V] : SymmetricCategory (Action V G) :=
-  symmetricCategoryOfFaithful (Action.forget V G)
+  .ofFaithful (Action.forget V G)
 
 section
 

Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean

@@ -525,19 +525,25 @@ lemma Functor.map_braiding (F : C ⥤ D) (X Y : C) [F.Braided] :
 /--
 A braided category with a faithful braided functor to a symmetric category is itself symmetric.
 -/
-def symmetricCategoryOfFaithful {C D : Type*} [Category C] [Category D] [MonoidalCategory C]
+def SymmetricCategory.ofFaithful {C D : Type*} [Category C] [Category D] [MonoidalCategory C]
     [MonoidalCategory D] [BraidedCategory C] [SymmetricCategory D] (F : C ⥤ D) [F.Braided]
     [F.Faithful] : SymmetricCategory C where
   symmetry X Y := F.map_injective (by simp)
 
 /-- Pull back a symmetric braiding along a fully faithful monoidal functor. -/
-noncomputable def symmetricCategoryOfFullyFaithful {C D : Type*} [Category C] [Category D]
+noncomputable def SymmetricCategory.ofFullyFaithful {C D : Type*} [Category C] [Category D]
     [MonoidalCategory C] [MonoidalCategory D] (F : C ⥤ D) [F.Monoidal] [F.Full]
     [F.Faithful] [SymmetricCategory D] : SymmetricCategory C :=
   let h : BraidedCategory C := BraidedCategory.ofFullyFaithful F
   let _ : F.Braided := {
     braided X Y := by simp [h, BraidedCategory.ofFullyFaithful, BraidedCategory.ofFaithful] }
-  symmetricCategoryOfFaithful F
+  .ofFaithful F
+
+@[deprecated (since := "2025-10-17")]
+alias symmetricCategoryOfFaithful := SymmetricCategory.ofFaithful
+
+@[deprecated (since := "2025-10-17")]
+alias symmetricCategoryOfFullyFaithful := SymmetricCategory.ofFullyFaithful
 
 namespace Functor.Braided
 

Mathlib/CategoryTheory/Monoidal/Braided/Transport.lean

@@ -15,8 +15,6 @@ universe v₁ v₂ u₁ u₂
 
 open CategoryTheory Category Monoidal MonoidalCategory
 
-noncomputable section
-
 variable {C : Type u₁} [Category.{v₁} C]
 variable {D : Type u₂} [Category.{v₂} D]
 
@@ -26,15 +24,18 @@ open Functor.LaxMonoidal Functor.OplaxMonoidal
 
 instance Transported.instBraidedCategory (e : C ≌ D) [MonoidalCategory C] [BraidedCategory C] :
     BraidedCategory (Transported e) :=
-  BraidedCategory.ofFullyFaithful (equivalenceTransported e).inverse
+  .ofFaithful e.inverse (fun _ _ ↦ e.functor.mapIso (β_ _ _)) fun _ _ ↦ by
+    simp [fromInducedCoreMonoidal, Functor.CoreMonoidal.toLaxMonoidal]
 
 local notation "e'" e => equivalenceTransported e
 
 instance (e : C ≌ D) [MonoidalCategory C] [BraidedCategory C] :
     (e' e).inverse.Braided where
   braided X Y := by
-    simp [Transported.instBraidedCategory, BraidedCategory.ofFullyFaithful,
-      BraidedCategory.ofFaithful]
+    simp [Transported.instBraidedCategory, BraidedCategory.ofFaithful,
+      fromInducedCoreMonoidal, Functor.CoreMonoidal.toLaxMonoidal]
+
+noncomputable section
 
 /--
 This is a def because once we have that both `(e' e).inverse` and `(e' e).functor` are
@@ -72,8 +73,10 @@ instance (e : C ≌ D) [MonoidalCategory C] [BraidedCategory C] :
         Equivalence.inv_fun_map, Functor.id_obj, comp_δ, assoc] at this
     simp [-Adjunction.rightAdjointLaxMonoidal_μ, ← this]
 
+end
+
 instance Transported.instSymmetricCategory (e : C ≌ D) [MonoidalCategory C]
     [SymmetricCategory C] : SymmetricCategory (Transported e) :=
-  symmetricCategoryOfFullyFaithful (equivalenceTransported e).inverse
+  .ofFaithful (equivalenceTransported e).inverse
 
 end CategoryTheory.Monoidal

Mathlib/CategoryTheory/Monoidal/Linear.lean

@@ -47,7 +47,7 @@ instance tensoringRight_linear (X : C) : ((tensoringRight C).obj X).Linear R whe
 
 /-- A faithful linear monoidal functor to a linear monoidal category
 ensures that the domain is linear monoidal. -/
-theorem monoidalLinearOfFaithful {D : Type*} [Category D] [Preadditive D] [Linear R D]
+theorem MonoidalLinear.ofFaithful {D : Type*} [Category D] [Preadditive D] [Linear R D]
     [MonoidalCategory D] [MonoidalPreadditive D] (F : D ⥤ C) [F.Monoidal] [F.Faithful]
     [F.Linear R] : MonoidalLinear R D :=
   { whiskerLeft_smul := by
@@ -61,4 +61,6 @@ theorem monoidalLinearOfFaithful {D : Type*} [Category D] [Preadditive D] [Linea
       rw [Functor.Monoidal.map_whiskerRight]
       simp }
 
+@[deprecated (since := "2025-10-17")] alias monoidalLinearOfFaithful := MonoidalLinear.ofFaithful
+
 end CategoryTheory

Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean

@@ -10,8 +10,6 @@ import Mathlib.CategoryTheory.Monoidal.Rigid.Basic
 -/
 
 
-noncomputable section
-
 namespace CategoryTheory
 
 open MonoidalCategory Functor.LaxMonoidal Functor.OplaxMonoidal
@@ -22,7 +20,7 @@ variable {C D : Type*} [Category C] [Category D] [MonoidalCategory C] [MonoidalC
 /-- Given candidate data for an exact pairing,
 which is sent by a faithful monoidal functor to an exact pairing,
 the equations holds automatically. -/
-def exactPairingOfFaithful [F.Faithful] {X Y : C} (eval : Y ⊗ X ⟶ 𝟙_ C)
+def ExactPairing.ofFaithful [F.Faithful] {X Y : C} (eval : Y ⊗ X ⟶ 𝟙_ C)
     (coeval : 𝟙_ C ⟶ X ⊗ Y) [ExactPairing (F.obj X) (F.obj Y)]
     (map_eval : F.map eval = (δ F _ _) ≫ ε_ _ _ ≫ ε F)
     (map_coeval : F.map coeval = (η F) ≫ η_ _ _ ≫ μ F _ _) : ExactPairing X Y where
@@ -40,22 +38,29 @@ def exactPairingOfFaithful [F.Faithful] {X Y : C} (eval : Y ⊗ X ⟶ 𝟙_ C)
 /-- Given a pair of objects which are sent by a fully faithful functor to a pair of objects
 with an exact pairing, we get an exact pairing.
 -/
-def exactPairingOfFullyFaithful [F.Full] [F.Faithful] (X Y : C)
+noncomputable def ExactPairing.ofFullyFaithful [F.Full] [F.Faithful] (X Y : C)
     [ExactPairing (F.obj X) (F.obj Y)] : ExactPairing X Y :=
-  exactPairingOfFaithful F (F.preimage (δ F _ _ ≫ ε_ _ _ ≫ (ε F)))
+  .ofFaithful F (F.preimage (δ F _ _ ≫ ε_ _ _ ≫ (ε F)))
     (F.preimage (η F ≫ η_ _ _ ≫ μ F _ _)) (by simp) (by simp)
 
+@[deprecated (since := "2025-10-17")] alias exactPairingOfFaithful := ExactPairing.ofFaithful
+
+@[deprecated (since := "2025-10-17")]
+alias exactPairingOfFullyFaithful := ExactPairing.ofFullyFaithful
+
 variable {F}
 variable {G : D ⥤ C} (adj : F ⊣ G) [F.IsEquivalence]
 
+noncomputable section
+
 /-- Pull back a left dual along an equivalence. -/
 def hasLeftDualOfEquivalence (X : C) [HasLeftDual (F.obj X)] :
     HasLeftDual X where
   leftDual := G.obj (ᘁ(F.obj X))
   exact := by
     letI := exactPairingCongrLeft (X := F.obj (G.obj ᘁ(F.obj X)))
       (X' := ᘁ(F.obj X)) (Y := F.obj X) (adj.toEquivalence.counitIso.app ᘁ(F.obj X))
-    apply exactPairingOfFullyFaithful F
+    apply ExactPairing.ofFullyFaithful F
 
 /-- Pull back a right dual along an equivalence. -/
 def hasRightDualOfEquivalence (X : C) [HasRightDual (F.obj X)] :
@@ -64,7 +69,7 @@ def hasRightDualOfEquivalence (X : C) [HasRightDual (F.obj X)] :
   exact := by
     letI := exactPairingCongrRight (X := F.obj X) (Y := F.obj (G.obj (F.obj X)ᘁ))
       (Y' := (F.obj X)ᘁ) (adj.toEquivalence.counitIso.app (F.obj X)ᘁ)
-    apply exactPairingOfFullyFaithful F
+    apply ExactPairing.ofFullyFaithful F
 
 /-- Pull back a left rigid structure along an equivalence. -/
 def leftRigidCategoryOfEquivalence [LeftRigidCategory D] :
@@ -79,4 +84,6 @@ def rigidCategoryOfEquivalence [RigidCategory D] : RigidCategory C where
   leftDual X := hasLeftDualOfEquivalence adj X
   rightDual X := hasRightDualOfEquivalence adj X
 
+end
+
 end CategoryTheory

Mathlib/CategoryTheory/Monoidal/Subcategory.lean

@@ -116,7 +116,7 @@ instance [MonoidalPreadditive C] : MonoidalPreadditive P.FullSubcategory :=
 variable (R : Type*) [Ring R] [Linear R C]
 
 instance [MonoidalPreadditive C] [MonoidalLinear R C] : MonoidalLinear R P.FullSubcategory :=
-  monoidalLinearOfFaithful R P.ι
+  .ofFaithful R P.ι
 
 end
 
@@ -166,7 +166,7 @@ section Symmetric
 variable [SymmetricCategory C]
 
 instance fullSymmetricSubcategory : SymmetricCategory P.FullSubcategory :=
-  symmetricCategoryOfFaithful P.ι
+  .ofFaithful P.ι
 
 end Symmetric
 

Mathlib/CategoryTheory/Monoidal/Transport.lean

@@ -24,8 +24,6 @@ with respect to the new monoidal structure on `D`.
 
 universe v₁ v₂ u₁ u₂
 
-noncomputable section
-
 open CategoryTheory
 
 open CategoryTheory.Category
@@ -188,10 +186,10 @@ instance : (equivalenceTransported e).inverse.Monoidal := by
 instance : (equivalenceTransported e).symm.functor.Monoidal :=
   inferInstanceAs (equivalenceTransported e).inverse.Monoidal
 
-instance : (equivalenceTransported e).functor.Monoidal :=
+noncomputable instance : (equivalenceTransported e).functor.Monoidal :=
   (equivalenceTransported e).symm.inverseMonoidal
 
-instance : (equivalenceTransported e).symm.inverse.Monoidal :=
+noncomputable instance : (equivalenceTransported e).symm.inverse.Monoidal :=
   inferInstanceAs (equivalenceTransported e).functor.Monoidal
 
 instance : (equivalenceTransported e).symm.IsMonoidal := by