feat(LinearAlgebra/DirectSum/Finsupp): add some more variants of `fin…

…suppTensorFinsupp` (#11598)

- add `finsuppTensorFinsuppLid`, `finsuppTensorFinsuppRid` as well as their simp lemmas
- make `finsuppTensorFinsupp'` a special case of `finsuppTensorFinsuppLid`
- add `TensorProduct.lid_eq_rid`

Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

@@ -34,8 +34,8 @@ def finsuppTensorFinsupp : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[R] ι × κ
 @[simp]
 theorem finsuppTensorFinsupp_single (i : ι) (m : M) (k : κ) (n : N) :
     finsuppTensorFinsupp R M N ι κ (Finsupp.single i m ⊗ₜ Finsupp.single k n) =
-      Finsupp.single (i, k) (m ⊗ₜ n) :=
-  by classical simp [finsuppTensorFinsupp]
+      Finsupp.single (i, k) (m ⊗ₜ n) := by
+  simp [finsuppTensorFinsupp]
 #align finsupp_tensor_finsupp_single finsuppTensorFinsupp_single
 
 @[simp]
@@ -68,24 +68,89 @@ theorem finsuppTensorFinsupp_symm_single (i : ι × κ) (m : M) (n : N) :
     (LinearEquiv.symm_apply_eq _).2 (finsuppTensorFinsupp_single _ _ _ _ _ _ _ _ _).symm
 #align finsupp_tensor_finsupp_symm_single finsuppTensorFinsupp_symm_single
 
+/-- A variant of `finsuppTensorFinsupp` where the first module is the ground ring. -/
+def finsuppTensorFinsuppLid : (ι →₀ R) ⊗[R] (κ →₀ N) ≃ₗ[R] ι × κ →₀ N :=
+  finsuppTensorFinsupp R R N ι κ ≪≫ₗ Finsupp.lcongr (Equiv.refl _) (TensorProduct.lid R N)
+
+@[simp]
+theorem finsuppTensorFinsuppLid_apply_apply (f : ι →₀ R) (g : κ →₀ N) (a : ι) (b : κ) :
+    finsuppTensorFinsuppLid R N ι κ (f ⊗ₜ[R] g) (a, b) = f a • g b := by
+  simp [finsuppTensorFinsuppLid]
+
+@[simp]
+theorem finsuppTensorFinsuppLid_single_tmul_single (a : ι) (b : κ) (r : R) (n : N) :
+    finsuppTensorFinsuppLid R N ι κ (Finsupp.single a r ⊗ₜ[R] Finsupp.single b n) =
+      Finsupp.single (a, b) (r • n) := by
+  simp [finsuppTensorFinsuppLid]
+
+@[simp]
+theorem finsuppTensorFinsuppLid_symm_single_smul (i : ι × κ) (r : R) (n : N) :
+    (finsuppTensorFinsuppLid R N ι κ).symm (Finsupp.single i (r • n)) =
+      Finsupp.single i.1 r ⊗ₜ Finsupp.single i.2 n :=
+  Prod.casesOn i fun _ _ =>
+    (LinearEquiv.symm_apply_eq _).2 (finsuppTensorFinsuppLid_single_tmul_single ..).symm
+
+/-- A variant of `finsuppTensorFinsupp` where the second module is the ground ring. -/
+def finsuppTensorFinsuppRid : (ι →₀ M) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ M :=
+  finsuppTensorFinsupp R M R ι κ ≪≫ₗ Finsupp.lcongr (Equiv.refl _) (TensorProduct.rid R M)
+
+@[simp]
+theorem finsuppTensorFinsuppRid_apply_apply (f : ι →₀ M) (g : κ →₀ R) (a : ι) (b : κ) :
+    finsuppTensorFinsuppRid R M ι κ (f ⊗ₜ[R] g) (a, b) = g b • f a := by
+  simp [finsuppTensorFinsuppRid]
+
+@[simp]
+theorem finsuppTensorFinsuppRid_single_tmul_single (a : ι) (b : κ) (m : M) (r : R) :
+    finsuppTensorFinsuppRid R M ι κ (Finsupp.single a m ⊗ₜ[R] Finsupp.single b r) =
+      Finsupp.single (a, b) (r • m) := by
+  simp [finsuppTensorFinsuppRid]
+
+@[simp]
+theorem finsuppTensorFinsuppRid_symm_single_smul (i : ι × κ) (m : M) (r : R) :
+    (finsuppTensorFinsuppRid R M ι κ).symm (Finsupp.single i (r • m)) =
+      Finsupp.single i.1 m ⊗ₜ Finsupp.single i.2 r :=
+  Prod.casesOn i fun _ _ =>
+    (LinearEquiv.symm_apply_eq _).2 (finsuppTensorFinsuppRid_single_tmul_single ..).symm
+
 /-- A variant of `finsuppTensorFinsupp` where both modules are the ground ring. -/
 def finsuppTensorFinsupp' : (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R :=
-  finsuppTensorFinsupp R R R ι κ ≪≫ₗ Finsupp.lcongr (Equiv.refl _) (TensorProduct.lid R R)
+  finsuppTensorFinsuppLid R R ι κ
 #align finsupp_tensor_finsupp' finsuppTensorFinsupp'
 
 @[simp]
 theorem finsuppTensorFinsupp'_apply_apply (f : ι →₀ R) (g : κ →₀ R) (a : ι) (b : κ) :
-    finsuppTensorFinsupp' R ι κ (f ⊗ₜ[R] g) (a, b) = f a * g b := by
-  simp [finsuppTensorFinsupp']
+    finsuppTensorFinsupp' R ι κ (f ⊗ₜ[R] g) (a, b) = f a * g b :=
+  finsuppTensorFinsuppLid_apply_apply R R ι κ f g a b
 #align finsupp_tensor_finsupp'_apply_apply finsuppTensorFinsupp'_apply_apply
 
 @[simp]
 theorem finsuppTensorFinsupp'_single_tmul_single (a : ι) (b : κ) (r₁ r₂ : R) :
     finsuppTensorFinsupp' R ι κ (Finsupp.single a r₁ ⊗ₜ[R] Finsupp.single b r₂) =
-      Finsupp.single (a, b) (r₁ * r₂) := by
-  ext ⟨a', b'⟩
-  classical
-  aesop (add norm [Finsupp.single_apply])
+      Finsupp.single (a, b) (r₁ * r₂) :=
+  finsuppTensorFinsuppLid_single_tmul_single R R ι κ a b r₁ r₂
 #align finsupp_tensor_finsupp'_single_tmul_single finsuppTensorFinsupp'_single_tmul_single
 
-end
+theorem finsuppTensorFinsupp'_symm_single_mul (i : ι × κ) (r₁ r₂ : R) :
+    (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i (r₁ * r₂)) =
+      Finsupp.single i.1 r₁ ⊗ₜ Finsupp.single i.2 r₂ :=
+  finsuppTensorFinsuppLid_symm_single_smul R R ι κ i r₁ r₂
+
+theorem finsuppTensorFinsupp'_symm_single_eq_single_one_tmul (i : ι × κ) (r : R) :
+    (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) =
+      Finsupp.single i.1 1 ⊗ₜ Finsupp.single i.2 r := by
+  nth_rw 1 [← one_mul r]
+  exact finsuppTensorFinsupp'_symm_single_mul R ι κ i _ _
+
+theorem finsuppTensorFinsupp'_symm_single_eq_tmul_single_one (i : ι × κ) (r : R) :
+    (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) =
+      Finsupp.single i.1 r ⊗ₜ Finsupp.single i.2 1 := by
+  nth_rw 1 [← mul_one r]
+  exact finsuppTensorFinsupp'_symm_single_mul R ι κ i _ _
+
+theorem finsuppTensorFinsuppLid_self :
+    finsuppTensorFinsuppLid R R ι κ = finsuppTensorFinsupp' R ι κ := rfl
+
+theorem finsuppTensorFinsuppRid_self :
+    finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ := by
+  rw [finsuppTensorFinsupp', finsuppTensorFinsuppLid, finsuppTensorFinsuppRid,
+    TensorProduct.lid_eq_rid]

Mathlib/LinearAlgebra/TensorProduct/Basic.lean

@@ -760,6 +760,10 @@ theorem rid_symm_apply (m : M) : (TensorProduct.rid R M).symm m = m ⊗ₜ 1 :=
   rfl
 #align tensor_product.rid_symm_apply TensorProduct.rid_symm_apply
 
+variable (R) in
+theorem lid_eq_rid : TensorProduct.lid R R = TensorProduct.rid R R :=
+  LinearEquiv.toLinearMap_injective <| ext' mul_comm
+
 open LinearMap
 
 section