feat(LinearAlgebra): make TensorProduct.finsuppLeft and friends heterobasic (#33469)

Author: erdOne

Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

@@ -31,34 +31,6 @@ public import Mathlib.LinearAlgebra.Finsupp.SumProd
 * `finsuppTensorFinsupp`, the tensor product of `ι →₀ M` and `κ →₀ N`
   is linearly equivalent to `(ι × κ) →₀ (M ⊗ N)`.
 
-## Case of MvPolynomial
-
-These functions apply to `MvPolynomial`, one can define
-```
-noncomputable def MvPolynomial.rTensor' :
-    MvPolynomial σ S ⊗[R] N ≃ₗ[S] (σ →₀ ℕ) →₀ (S ⊗[R] N) :=
-  TensorProduct.finsuppLeft'
-
-noncomputable def MvPolynomial.rTensor :
-    MvPolynomial σ R ⊗[R] N ≃ₗ[R] (σ →₀ ℕ) →₀ N :=
-  TensorProduct.finsuppScalarLeft
-```
-
-However, to be actually usable, these definitions need lemmas to be given in companion PR.
-
-## Case of `Polynomial`
-
-`Polynomial` is a structure containing a `Finsupp`, so these functions
-can't be applied directly to `Polynomial`.
-
-Some linear equivs need to be added to mathlib for that.
-This belongs to a companion PR.
-
-## TODO
-
-* generalize to `MonoidAlgebra`, `AlgHom `
-
-* reprove `TensorProduct.finsuppLeft'` using existing heterobasic version of `TensorProduct.congr`
 -/
 
 @[expose] public section
@@ -72,8 +44,8 @@ open Set LinearMap Submodule
 
 section TensorProduct
 
-variable (R : Type*) [CommSemiring R]
-  (M : Type*) [AddCommMonoid M] [Module R M]
+variable (R S : Type*) [CommSemiring R] [Semiring S] [Algebra R S]
+  (M : Type*) [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M]
   (N : Type*) [AddCommMonoid N] [Module R N]
 
 namespace TensorProduct
@@ -82,110 +54,95 @@ variable (ι : Type*) [DecidableEq ι]
 
 /-- The tensor product of `ι →₀ M` and `N` is linearly equivalent to `ι →₀ M ⊗[R] N` -/
 noncomputable def finsuppLeft :
-    (ι →₀ M) ⊗[R] N ≃ₗ[R] ι →₀ M ⊗[R] N :=
-  congr (finsuppLEquivDirectSum R M ι) (.refl R N) ≪≫ₗ
-    directSumLeft R (fun _ ↦ M) N ≪≫ₗ (finsuppLEquivDirectSum R _ ι).symm
+    (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N :=
+  AlgebraTensorModule.congr (finsuppLEquivDirectSum S M ι) (.refl R N) ≪≫ₗ
+    directSumLeft _ S (fun _ ↦ M) N ≪≫ₗ (finsuppLEquivDirectSum _ _ ι).symm
 
-variable {R M N ι}
+variable {R S M N ι}
 
 lemma finsuppLeft_apply_tmul (p : ι →₀ M) (n : N) :
-    finsuppLeft R M N ι (p ⊗ₜ[R] n) = p.sum fun i m ↦ Finsupp.single i (m ⊗ₜ[R] n) := by
+    finsuppLeft R S M N ι (p ⊗ₜ[R] n) = p.sum fun i m ↦ Finsupp.single i (m ⊗ₜ[R] n) := by
   induction p using Finsupp.induction_linear with
   | zero => simp
   | add f g hf hg => simp [add_tmul, map_add, hf, hg, Finsupp.sum_add_index]
   | single => simp [finsuppLeft]
 
 @[simp]
 lemma finsuppLeft_apply_tmul_apply (p : ι →₀ M) (n : N) (i : ι) :
-    finsuppLeft R M N ι (p ⊗ₜ[R] n) i = p i ⊗ₜ[R] n := by
+    finsuppLeft R S M N ι (p ⊗ₜ[R] n) i = p i ⊗ₜ[R] n := by
   rw [finsuppLeft_apply_tmul, Finsupp.sum_apply,
     Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]
 
 theorem finsuppLeft_apply (t : (ι →₀ M) ⊗[R] N) (i : ι) :
-    finsuppLeft R M N ι t i = rTensor N (Finsupp.lapply i) t := by
+    finsuppLeft R S M N ι t i = rTensor N (Finsupp.lapply i) t := by
   induction t with
   | zero => simp
   | tmul f n => simp only [finsuppLeft_apply_tmul_apply, rTensor_tmul, Finsupp.lapply_apply]
   | add x y hx hy => simp [map_add, hx, hy]
 
 @[simp]
 lemma finsuppLeft_symm_apply_single (i : ι) (m : M) (n : N) :
-    (finsuppLeft R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) =
+    (finsuppLeft R S M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) =
       Finsupp.single i m ⊗ₜ[R] n := by
   simp [finsuppLeft]
 
-variable (R M N ι)
+variable (R S M N ι) in
 /-- The tensor product of `M` and `ι →₀ N` is linearly equivalent to `ι →₀ M ⊗[R] N` -/
 noncomputable def finsuppRight :
-    M ⊗[R] (ι →₀ N) ≃ₗ[R] ι →₀ M ⊗[R] N :=
-  congr (.refl R M) (finsuppLEquivDirectSum R N ι) ≪≫ₗ
-    directSumRight R M (fun _ : ι ↦ N) ≪≫ₗ (finsuppLEquivDirectSum R _ ι).symm
-
-variable {R M N ι}
+    M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N :=
+  AlgebraTensorModule.congr (.refl S M) (finsuppLEquivDirectSum R N ι) ≪≫ₗ
+    directSumRight' R S M (fun _ : ι ↦ N) ≪≫ₗ (finsuppLEquivDirectSum _ _ ι).symm
 
 lemma finsuppRight_apply_tmul (m : M) (p : ι →₀ N) :
-    finsuppRight R M N ι (m ⊗ₜ[R] p) = p.sum fun i n ↦ Finsupp.single i (m ⊗ₜ[R] n) := by
+    finsuppRight R S M N ι (m ⊗ₜ[R] p) = p.sum fun i n ↦ Finsupp.single i (m ⊗ₜ[R] n) := by
   induction p using Finsupp.induction_linear with
   | zero => simp
   | add f g hf hg => simp [tmul_add, map_add, hf, hg, Finsupp.sum_add_index]
-  | single => simp [finsuppRight]
+  | single => simp [finsuppRight, directSumRight']; simp [lof_eq_of R, ← lof_eq_of S]
 
 @[simp]
 lemma finsuppRight_apply_tmul_apply (m : M) (p : ι →₀ N) (i : ι) :
-    finsuppRight R M N ι (m ⊗ₜ[R] p) i = m ⊗ₜ[R] p i := by
+    finsuppRight R S M N ι (m ⊗ₜ[R] p) i = m ⊗ₜ[R] p i := by
   rw [finsuppRight_apply_tmul, Finsupp.sum_apply,
     Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]
 
 theorem finsuppRight_apply (t : M ⊗[R] (ι →₀ N)) (i : ι) :
-    finsuppRight R M N ι t i = lTensor M (Finsupp.lapply i) t := by
+    finsuppRight R S M N ι t i = lTensor M (Finsupp.lapply i) t := by
   induction t with
   | zero => simp
   | tmul m f => simp [finsuppRight_apply_tmul_apply]
   | add x y hx hy => simp [map_add, hx, hy]
 
+@[simp]
+lemma finsuppRight_tmul_single (i : ι) (m : M) (n : N) :
+    finsuppRight R S M N ι (m ⊗ₜ[R] Finsupp.single i n) = Finsupp.single i (m ⊗ₜ[R] n) := by
+  ext; simp +contextual [Finsupp.single_apply, apply_ite]
+
 @[simp]
 lemma finsuppRight_symm_apply_single (i : ι) (m : M) (n : N) :
-    (finsuppRight R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) =
+    (finsuppRight R S M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) =
       m ⊗ₜ[R] Finsupp.single i n := by
-  simp [finsuppRight]
-
-variable {S : Type*} [CommSemiring S] [Algebra R S]
-  [Module S M] [IsScalarTower R S M]
+  simp [LinearEquiv.symm_apply_eq]
 
 lemma finsuppLeft_smul' (s : S) (t : (ι →₀ M) ⊗[R] N) :
-    finsuppLeft R M N ι (s • t) = s • finsuppLeft R M N ι t := by
+    finsuppLeft R S M N ι (s • t) = s • finsuppLeft R S M N ι t := by
   induction t with
   | zero => simp
   | add x y hx hy => simp [hx, hy]
   | tmul p n => ext; simp [smul_tmul', finsuppLeft_apply_tmul_apply]
 
-variable (R M N ι S)
-/-- When `M` is also an `S`-module, then `TensorProduct.finsuppLeft R M N`
-  is an `S`-linear equiv -/
-noncomputable def finsuppLeft' :
-    (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N where
-  __ := finsuppLeft R M N ι
-  map_smul' := finsuppLeft_smul'
+@[deprecated (since := "2026-01-01")] alias finsuppLeft' := finsuppLeft
 
-variable {R M N ι S}
+@[nolint synTaut, deprecated "is syntactic rfl now" (since := "2026-01-01")]
 lemma finsuppLeft'_apply (x : (ι →₀ M) ⊗[R] N) :
-    finsuppLeft' R M N ι S x = finsuppLeft R M N ι x := rfl
-
-/- -- TODO : reprove using the existing heterobasic lemmas
-noncomputable example :
-    (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ (M ⊗[R] N) := by
-  have f : (⨁ (i₁ : ι), M) ⊗[R] N ≃ₗ[S] ⨁ (i : ι), M ⊗[R] N := sorry
-  exact (AlgebraTensorModule.congr
-    (finsuppLEquivDirectSum S M ι) (.refl R N)).trans
-    (f.trans (finsuppLEquivDirectSum S (M ⊗[R] N) ι).symm) -/
+    finsuppLeft R S M N ι x = finsuppLeft R S M N ι x := rfl
 
-variable (R M N ι)
+variable (R M N ι) in
 /-- The tensor product of `ι →₀ R` and `N` is linearly equivalent to `ι →₀ N` -/
 noncomputable def finsuppScalarLeft :
     (ι →₀ R) ⊗[R] N ≃ₗ[R] ι →₀ N :=
-  finsuppLeft R R N ι ≪≫ₗ (Finsupp.mapRange.linearEquiv (TensorProduct.lid R N))
+  finsuppLeft R R R N ι ≪≫ₗ (Finsupp.mapRange.linearEquiv (TensorProduct.lid R N))
 
-variable {R M N ι}
 @[simp]
 lemma finsuppScalarLeft_apply_tmul_apply (p : ι →₀ R) (n : N) (i : ι) :
     finsuppScalarLeft R N ι (p ⊗ₜ[R] n) i = p i • n := by
@@ -207,38 +164,36 @@ lemma finsuppScalarLeft_symm_apply_single (i : ι) (n : N) :
       (Finsupp.single i 1) ⊗ₜ[R] n := by
   simp [finsuppScalarLeft, finsuppLeft_symm_apply_single]
 
-variable (R M N ι)
-
+variable (R S M N ι) in
 /-- The tensor product of `M` and `ι →₀ R` is linearly equivalent to `ι →₀ M` -/
 noncomputable def finsuppScalarRight :
-    M ⊗[R] (ι →₀ R) ≃ₗ[R] ι →₀ M :=
-  finsuppRight R M R ι ≪≫ₗ Finsupp.mapRange.linearEquiv (TensorProduct.rid R M)
-
-variable {R M N ι}
+    M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M :=
+  finsuppRight R S M R ι ≪≫ₗ Finsupp.mapRange.linearEquiv (AlgebraTensorModule.rid R S M)
 
 @[simp]
 lemma finsuppScalarRight_apply_tmul_apply (m : M) (p : ι →₀ R) (i : ι) :
-    finsuppScalarRight R M ι (m ⊗ₜ[R] p) i = p i • m := by
+    finsuppScalarRight R S M ι (m ⊗ₜ[R] p) i = p i • m := by
   simp [finsuppScalarRight]
 
 lemma finsuppScalarRight_apply_tmul (m : M) (p : ι →₀ R) :
-    finsuppScalarRight R M ι (m ⊗ₜ[R] p) = p.sum fun i n ↦ Finsupp.single i (n • m) := by
+    finsuppScalarRight R S M ι (m ⊗ₜ[R] p) = p.sum fun i n ↦ Finsupp.single i (n • m) := by
   ext i
   rw [finsuppScalarRight_apply_tmul_apply, Finsupp.sum_apply,
     Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]
 
 lemma finsuppScalarRight_apply (t : M ⊗[R] (ι →₀ R)) (i : ι) :
-    finsuppScalarRight R M ι t i = TensorProduct.rid R M ((Finsupp.lapply i).lTensor M t) := by
+    finsuppScalarRight R S M ι t i =
+      AlgebraTensorModule.rid R S M ((Finsupp.lapply i).lTensor M t) := by
   simp [finsuppScalarRight, finsuppRight_apply]
 
 @[simp]
 lemma finsuppScalarRight_symm_apply_single (i : ι) (m : M) :
-    (finsuppScalarRight R M ι).symm (Finsupp.single i m) =
+    (finsuppScalarRight R S M ι).symm (Finsupp.single i m) =
       m ⊗ₜ[R] (Finsupp.single i 1) := by
   simp [finsuppScalarRight, finsuppRight_symm_apply_single]
 
 theorem finsuppScalarRight_smul (s : S) (t) :
-    finsuppScalarRight R M ι (s • t) = s • finsuppScalarRight R M ι t := by
+    finsuppScalarRight R S M ι (s • t) = s • finsuppScalarRight R S M ι t := by
   induction t using TensorProduct.induction_on with
   | zero => simp
   | add x y hx hy => simp [hx, hy]
@@ -248,15 +203,11 @@ theorem finsuppScalarRight_smul (s : S) (t) :
     ext i n j
     simp [smul_comm n s m]
 
-variable (R S M ι) in
-/-- When `M` is also an `S`-module, `TensorProduct.finsuppScalarRight R M ι` is `S`-linear. -/
-noncomputable def finsuppScalarRight' :
-    M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M where
-  toAddEquiv := finsuppScalarRight R M ι
-  map_smul' s x := finsuppScalarRight_smul s x
+@[deprecated (since := "2026-01-01")] alias finsuppScalarRight' := finsuppScalarRight
 
+@[nolint synTaut, deprecated "is syntactic rfl now" (since := "2026-01-01")]
 theorem coe_finsuppScalarRight' :
-    ⇑(finsuppScalarRight' R M ι S) = finsuppScalarRight R M ι :=
+    ⇑(finsuppScalarRight R S M ι) = finsuppScalarRight R S M ι :=
   rfl
 
 end TensorProduct
@@ -269,7 +220,7 @@ variable (R S M N ι κ : Type*)
 
 theorem Finsupp.linearCombination_one_tmul [DecidableEq ι] {v : ι → M} :
     (linearCombination S ((1 : S) ⊗ₜ[R] v ·)).restrictScalars R =
-      (linearCombination R v).lTensor S ∘ₗ (finsuppScalarRight R S ι).symm := by
+      (linearCombination R v).lTensor S ∘ₗ (finsuppScalarRight R R S ι).symm := by
   ext; simp [smul_tmul']
 
 variable [Module S M] [IsScalarTower R S M]

Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

@@ -63,28 +63,18 @@ protected def directSum :
       AlgebraTensorModule.map_tmul, id_coe, id_eq]
 
 /-- Tensor products distribute over a direct sum on the left . -/
-def directSumLeft : (⨁ i₁, M₁ i₁) ⊗[R] M₂' ≃ₗ[R] ⨁ i, M₁ i ⊗[R] M₂' :=
+def directSumLeft : (⨁ i₁, M₁ i₁) ⊗[R] M₂' ≃ₗ[S] ⨁ i, M₁ i ⊗[R] M₂' :=
   LinearEquiv.ofLinear
-    (lift <|
-      DirectSum.toModule R _ _ fun _ =>
-        (mk R _ _).compr₂ <| DirectSum.lof R ι₁ (fun i => M₁ i ⊗[R] M₂') _)
-    (DirectSum.toModule R _ _ fun _ => rTensor _ (DirectSum.lof R ι₁ _ _))
-    (DirectSum.linearMap_ext R fun i =>
-      TensorProduct.ext <|
-        LinearMap.ext₂ fun m₁ m₂ => by
-          dsimp only [comp_apply, compr₂ₛₗ_apply, id_apply, mk_apply]
-          simp_rw [DirectSum.toModule_lof, rTensor_tmul, lift.tmul, DirectSum.toModule_lof,
-            compr₂_apply, mk_apply])
-    (TensorProduct.ext <|
-      DirectSum.linearMap_ext R fun i =>
-        LinearMap.ext₂ fun m₁ m₂ => by
-          dsimp only [comp_apply, compr₂ₛₗ_apply, id_apply, mk_apply]
-          simp_rw [lift.tmul, DirectSum.toModule_lof, compr₂_apply,
-            mk_apply, DirectSum.toModule_lof, rTensor_tmul])
+    (AlgebraTensorModule.lift <|
+      DirectSum.toModule S _ _ fun _ =>
+        (AlgebraTensorModule.mk _ S _ _).compr₂ <| DirectSum.lof _ ι₁ (fun i => M₁ i ⊗[R] M₂') _)
+    (DirectSum.toModule _ _ _ fun i => AlgebraTensorModule.map (DirectSum.lof _ ι₁ M₁ i) .id)
+    (by ext; simp)
+    (by ext; simp)
 
 /-- Tensor products distribute over a direct sum on the right. -/
 def directSumRight : (M₁' ⊗[R] ⨁ i, M₂ i) ≃ₗ[R] ⨁ i, M₁' ⊗[R] M₂ i :=
-  TensorProduct.comm R _ _ ≪≫ₗ directSumLeft R M₂ M₁' ≪≫ₗ
+  TensorProduct.comm R _ _ ≪≫ₗ directSumLeft R R M₂ M₁' ≪≫ₗ
     DFinsupp.mapRange.linearEquiv fun _ => TensorProduct.comm R _ _
 
 variable {M₁ M₁' M₂ M₂'}
@@ -104,24 +94,24 @@ theorem directSum_symm_lof_tmul (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂)
 
 @[simp]
 theorem directSumLeft_tmul_lof (i : ι₁) (x : M₁ i) (y : M₂') :
-    directSumLeft R M₁ M₂' (DirectSum.lof R _ _ i x ⊗ₜ[R] y) =
-    DirectSum.lof R _ _ i (x ⊗ₜ[R] y) := by
-  dsimp only [directSumLeft, LinearEquiv.ofLinear_apply, lift.tmul]
-  rw [DirectSum.toModule_lof R i]
+    directSumLeft R S M₁ M₂' (DirectSum.lof S _ _ i x ⊗ₜ[R] y) =
+    DirectSum.lof S _ _ i (x ⊗ₜ[R] y) := by
+  dsimp [directSumLeft, LinearEquiv.ofLinear_apply, lift.tmul]
+  rw [DirectSum.toModule_lof S]
   rfl
 
 @[simp]
 theorem directSumLeft_symm_lof_tmul (i : ι₁) (x : M₁ i) (y : M₂') :
-    (directSumLeft R M₁ M₂').symm (DirectSum.lof R _ _ i (x ⊗ₜ[R] y)) =
-      DirectSum.lof R _ _ i x ⊗ₜ[R] y := by
+    (directSumLeft R S M₁ M₂').symm (DirectSum.lof S _ _ i (x ⊗ₜ[R] y)) =
+      DirectSum.lof S _ _ i x ⊗ₜ[R] y := by
   rw [LinearEquiv.symm_apply_eq, directSumLeft_tmul_lof]
 
 @[simp]
 lemma directSumLeft_tmul (m : ⨁ i, M₁ i) (n : M₂') (i : ι₁) :
-    directSumLeft R M₁ M₂' (m ⊗ₜ[R] n) i = (m i) ⊗ₜ[R] n := by
-  suffices (DirectSum.component R ι₁ _ i) ∘ₗ (directSumLeft R M₁ M₂').toLinearMap ∘ₗ
-      ((TensorProduct.mk R (⨁ i, M₁ i) M₂').flip n) =
-        ((TensorProduct.mk R (M₁ i) M₂').flip n) ∘ₗ (DirectSum.component R ι₁ M₁ i) by
+    directSumLeft R S M₁ M₂' (m ⊗ₜ[R] n) i = (m i) ⊗ₜ[R] n := by
+  suffices (DirectSum.component S ι₁ _ i) ∘ₗ (directSumLeft R S M₁ M₂').toLinearMap ∘ₗ
+      ((AlgebraTensorModule.mk R S (⨁ i, M₁ i) M₂').flip n) =
+        ((AlgebraTensorModule.mk R S (M₁ i) M₂').flip n) ∘ₗ (DirectSum.component S ι₁ M₁ i) by
     simpa using LinearMap.congr_fun this m
   ext j n
   by_cases hj : j = i

Mathlib/LinearAlgebra/TensorProduct/Basis.lean

@@ -86,7 +86,7 @@ If `{𝒞ᵢ}` is a basis for the module `N`, then every elements of `x ∈ M 
 as `∑ᵢ mᵢ ⊗ 𝒞ᵢ` for some `mᵢ ∈ M`.
 -/
 def TensorProduct.equivFinsuppOfBasisRight : M ⊗[R] N ≃ₗ[R] κ →₀ M :=
-  LinearEquiv.lTensor M 𝒞.repr ≪≫ₗ TensorProduct.finsuppScalarRight R M κ
+  LinearEquiv.lTensor M 𝒞.repr ≪≫ₗ TensorProduct.finsuppScalarRight R R M κ
 
 @[simp]
 lemma TensorProduct.equivFinsuppOfBasisRight_apply_tmul (m : M) (n : N) :

Mathlib/LinearAlgebra/TensorProduct/Submodule.lean

@@ -265,7 +265,7 @@ theorem mulLeftMap_eq_mulMap_comp {ι : Type*} [DecidableEq ι] (m : ι → M) :
 variable {N} in
 theorem mulRightMap_eq_mulMap_comp {ι : Type*} [DecidableEq ι] (n : ι → N) :
     mulRightMap M n = mulMap M N ∘ₗ LinearMap.lTensor M (Finsupp.linearCombination R n) ∘ₗ
-      (TensorProduct.finsuppScalarRight R M ι).symm.toLinearMap := by
+      (TensorProduct.finsuppScalarRight R R M ι).symm.toLinearMap := by
   ext; simp
 
 end Semiring

Mathlib/RepresentationTheory/Coinvariants.lean

@@ -468,8 +468,7 @@ lemma coinvariantsTensorFreeToFinsupp_mk_tmul_single (x : A) (i : α) (g : G) (r
     DFunLike.coe (F := (A.ρ.tprod (Representation.free k G α)).Coinvariants →ₗ[k] α →₀ A.V)
       (coinvariantsTensorFreeToFinsupp A α) (Coinvariants.mk _ (x ⊗ₜ single i (single g r))) =
       single i (r • A.ρ g⁻¹ x) := by
-  simp [tensorObj_carrier, coinvariantsTensorFreeToFinsupp,
-    Coinvariants.map, finsuppTensorRight, TensorProduct.finsuppRight]
+  simp [tensorObj_carrier, coinvariantsTensorFreeToFinsupp, Coinvariants.map]
 
 variable (A α)
 

Mathlib/RepresentationTheory/Rep.lean

@@ -481,7 +481,7 @@ open ModuleCat.MonoidalCategory
 @[simps! hom_hom inv_hom]
 def finsuppTensorLeft :
     A.finsupp α ⊗ B ≅ (A ⊗ B).finsupp α :=
-  Action.mkIso (TensorProduct.finsuppLeft k A B α).toModuleIso
+  Action.mkIso (TensorProduct.finsuppLeft k _ A B α).toModuleIso
     fun _ => ModuleCat.hom_ext <| TensorProduct.ext <| lhom_ext fun _ _ => by
       ext
       simp [Action_ρ_eq_ρ, TensorProduct.finsuppLeft_apply_tmul,
@@ -492,7 +492,7 @@ def finsuppTensorLeft :
 @[simps! hom_hom inv_hom]
 def finsuppTensorRight :
     A ⊗ B.finsupp α ≅ (A ⊗ B).finsupp α :=
-  Action.mkIso (TensorProduct.finsuppRight k A B α).toModuleIso fun _ => ModuleCat.hom_ext <|
+  Action.mkIso (TensorProduct.finsuppRight k _ A B α).toModuleIso fun _ => ModuleCat.hom_ext <|
       TensorProduct.ext <| LinearMap.ext fun _ => lhom_ext fun _ _ => by
       ext
       simp [Action_ρ_eq_ρ, TensorProduct.finsuppRight_apply_tmul, ModuleCat.endRingEquiv,

Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean

@@ -196,7 +196,7 @@ instance directSum {ι : Type*} [Nonempty ι] (M : ι → Type*) [∀ i, AddComm
   obtain ⟨x, y, hxy⟩ := Nontrivial.exists_pair_ne (α := M i ⊗[R] N)
   haveI : Nontrivial (⨁ (i : ι), M i ⊗[R] N) :=
     ⟨DirectSum.of _ i x, DirectSum.of _ i y, fun h ↦ hxy (DirectSum.of_injective i h)⟩
-  apply (TensorProduct.directSumLeft R M N).toEquiv.nontrivial
+  apply (TensorProduct.directSumLeft R R M N).toEquiv.nontrivial
 
 /-- Free `R`-modules over discrete types are flat. -/
 instance finsupp (ι : Type v) [Nonempty ι] : FaithfullyFlat R (ι →₀ R) := by

Mathlib/RingTheory/Ideal/Quotient/Index.lean

@@ -80,7 +80,7 @@ lemma Submodule.index_smul_le [Finite (R ⧸ I)]
   have hf : Function.Surjective f := fun x ↦ by
     obtain ⟨y, hy⟩ := H.ge x.2; exact ⟨y, Subtype.ext hy⟩
   have : Function.Surjective
-      (f.lTensor (R ⧸ I) ∘ₗ (finsuppScalarRight R (R ⧸ I) s).symm.toLinearMap) :=
+      (f.lTensor (R ⧸ I) ∘ₗ (finsuppScalarRight R R (R ⧸ I) s).symm.toLinearMap) :=
     (LinearMap.lTensor_surjective (R ⧸ I) hf).comp (LinearEquiv.surjective _)
   refine (Nat.card_le_card_of_surjective _ this).trans ?_
   simp only [Nat.card_eq_fintype_card, Fintype.card_finsupp, Fintype.card_coe, le_rfl]