feat(LinearAlgebra/DirectSum/Finsupp) : tensor products of finsupp functions

Mathlib.lean

@@ -3336,6 +3336,9 @@ import Mathlib.RingTheory.Subring.Pointwise
 import Mathlib.RingTheory.Subsemiring.Basic
 import Mathlib.RingTheory.Subsemiring.Pointwise
 import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.MonoidAlgebra
+import Mathlib.LinearAlgebra.TensorProduct.MvPolynomial
+import Mathlib.LinearAlgebra.TensorProduct.Polynomial
 import Mathlib.RingTheory.Trace
 import Mathlib.RingTheory.UniqueFactorizationDomain
 import Mathlib.RingTheory.Valuation.Basic

Mathlib/Algebra/Lie/TensorProduct.lean

@@ -65,10 +65,7 @@ instance lieRingModule : LieRingModule L (M ⊗[R] N) where
         hasBracketAux ⁅x, y⁆ + (hasBracketAux y).comp (hasBracketAux x) by
       simp only [← LinearMap.add_apply]; rw [← LinearMap.comp_apply, this]; rfl
     ext m n
-    simp only [hasBracketAux, LieRing.of_associative_ring_bracket, LinearMap.mul_apply, mk_apply,
-      LinearMap.lTensor_sub, LinearMap.compr₂_apply, Function.comp_apply, LinearMap.coe_comp,
-      LinearMap.rTensor_tmul, LieHom.map_lie, toEndomorphism_apply_apply, LinearMap.add_apply,
-      LinearMap.map_add, LinearMap.rTensor_sub, LinearMap.sub_apply, LinearMap.lTensor_tmul]
+    simp [hasBracketAux, LieRing.of_associative_ring_bracket]
     abel
 #align tensor_product.lie_module.lie_ring_module TensorProduct.LieModule.lieRingModule
 
@@ -96,8 +93,7 @@ def lift : (M →ₗ[R] N →ₗ[R] P) ≃ₗ⁅R,L⁆ M ⊗[R] N →ₗ[R] P :=
   { TensorProduct.lift.equiv R M N P with
     map_lie' := fun {x f} => by
       ext m n
-      simp only [mk_apply, LinearMap.compr₂_apply, lie_tmul_right, LinearMap.sub_apply,
-        lift.equiv_apply, LinearEquiv.toFun_eq_coe, LieHom.lie_apply, LinearMap.map_add]
+      simp
       abel }
 #align tensor_product.lie_module.lift TensorProduct.LieModule.lift
 

Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johannes Hölzl
+Authors: Johannes Hölzl, Antoine Chambert-Loir
 -/
 import Mathlib.Algebra.DirectSum.Finsupp
 import Mathlib.LinearAlgebra.Finsupp
@@ -12,29 +12,234 @@ import Mathlib.LinearAlgebra.DirectSum.TensorProduct
 /-!
 # Results on finitely supported functions.
 
-The tensor product of `ι →₀ M` and `κ →₀ N` is linearly equivalent to `(ι × κ) →₀ (M ⊗ N)`.
+* `TensorProduct.finsuppLeft`, the tensor product of `ι →₀ M` and `N`
+  is linearly equivalent to `ι →₀ M ⊗[R] N`
+
+* `TensorProduct.finsuppScalarLeft`, the tensor product of `ι →₀ R` and `N`
+  is linearly equivalent to `ι →₀ N`
+
+* `TensorProduct.finsuppRight`, the tensor product of `M` and `ι →₀ N`
+  is linearly equivalent to `ι →₀ M ⊗[R] N`
+
+* `TensorProduct.finsuppScalarRight`, the tensor product of `M` and `ι →₀ R`
+  is linearly equivalent to `ι →₀ N`
+
+
+* `TensorProduct.finsuppLeft'`, if `M` is an `S`-module,
+  then the tensor product of `ι →₀ M` and `N` is `S`-linearly equivalent
+  to `ι →₀ M ⊗[R] N`
+
+* `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
+ ```
+
+## 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.
+
+## TODO
+
+* generalize to `MonoidAlgebra`, `AlgHom `
+
+* reprove `TensorProduct.finsuppLeft'` using existing heterobasic version of `TensorProduct.congr`
 -/
 
 
 universe u v w
 
 noncomputable section
 
-open DirectSum
+open DirectSum TensorProduct
 
 open Set LinearMap Submodule
 
 section TensorProduct
 
-open TensorProduct
+variable {R : Type*} [CommSemiring R]
+  {M : Type*} [AddCommMonoid M] [Module R M]
+  {N : Type*} [AddCommMonoid N] [Module R N]
+
+namespace TensorProduct
+
+variable {ι : Type*} [DecidableEq ι]
+
+/-- The tensor product of `i →₀ M` and `N` is linearly equivalent to `i →₀ M ⊗[R] N` -/
+noncomputable def finsuppLeft :
+    (ι →₀ M) ⊗[R] N ≃ₗ[R] ι →₀ (M ⊗[R] N) :=
+  (congr (finsuppLEquivDirectSum R M ι) (LinearEquiv.refl R N)).trans
+    ((directSumLeft R (fun _ : ι => M) N).trans
+      (finsuppLEquivDirectSum R (M ⊗[R] N) ι).symm)
+
+lemma finsuppLeft_apply_tmul (p : ι →₀ M) (n : N) :
+    finsuppLeft (p ⊗ₜ[R] n) = p.sum (fun i m ↦ Finsupp.single i (m ⊗ₜ[R] n)) := by
+  simp only [finsuppLeft, LinearEquiv.trans_apply, congr_tmul, LinearEquiv.refl_apply]
+  conv_lhs => rw [← Finsupp.sum_single p]
+  rw [LinearEquiv.symm_apply_eq]
+  simp only [map_finsupp_sum]
+  simp only [finsuppLEquivDirectSum_single]
+  rw [← LinearEquiv.eq_symm_apply]
+  simp only [map_finsupp_sum]
+  simp only [directSumLeft_symm_lof_tmul]
+  simp only [Finsupp.sum, sum_tmul]
+
+lemma finsuppLeft_apply_tmul_apply (p : ι →₀ M) (n : N) (i : ι) :
+    finsuppLeft (p ⊗ₜ[R] n) i = p i ⊗ₜ[R] n := by
+  rw [finsuppLeft_apply_tmul]
+  simp only [Finsupp.sum_apply]
+  conv_rhs => rw [← Finsupp.single_eq_same (a := i) (b := p i ⊗ₜ[R] n)]
+  apply Finsupp.sum_eq_single i
+  · exact fun _ _ ↦ Finsupp.single_eq_of_ne
+  · intro _
+    simp
+
+lemma finsuppLeft_symm_apply_single (i : ι) (m : M) (n : N) :
+    finsuppLeft.symm (Finsupp.single i (m ⊗ₜ[R] n)) =
+      Finsupp.single i m ⊗ₜ[R] n := by
+  simp [finsuppLeft, Finsupp.lsum]
 
-open TensorProduct
+/-- The tensor product of `M` and `i →₀ N` is linearly equivalent to `i →₀ M ⊗[R] N` -/
+noncomputable def finsuppRight :
+    M ⊗[R] (ι →₀ N) ≃ₗ[R] ι →₀ (M ⊗[R] N) :=
+  (congr (LinearEquiv.refl R M) (finsuppLEquivDirectSum R N ι)).trans
+    ((directSumRight R M (fun _ : ι => N)).trans
+      (finsuppLEquivDirectSum R (M ⊗[R] N) ι).symm)
+
+lemma finsuppRight_apply_tmul (m : M) (p : ι →₀ N) :
+    finsuppRight (m ⊗ₜ[R] p) = p.sum (fun i n ↦ Finsupp.single i (m ⊗ₜ[R] n)) := by
+  simp [finsuppRight]
+  conv_lhs => rw [← Finsupp.sum_single p]
+  rw [LinearEquiv.symm_apply_eq]
+  simp only [map_finsupp_sum]
+  simp only [finsuppLEquivDirectSum_single]
+  rw [← LinearEquiv.eq_symm_apply]
+  simp only [map_finsupp_sum]
+  simp only [directSumRight_symm_lof_tmul]
+  simp only [Finsupp.sum, tmul_sum]
+
+lemma finsuppRight_symm_apply_single (i : ι) (m : M) (n : N) :
+    finsuppRight.symm (Finsupp.single i (m ⊗ₜ[R] n)) =
+      m ⊗ₜ[R] Finsupp.single i n := by
+  simp [finsuppRight, Finsupp.lsum]
+
+variable {S : Type*} [CommSemiring S] [Algebra R S]
+  [Module S M] [IsScalarTower R S M]
+
+lemma finsuppLeft_smul' (s : S) (t : (ι →₀ M) ⊗[R] N) :
+    finsuppLeft (s • t) = s • finsuppLeft t := by
+  induction t using TensorProduct.induction_on with
+  | zero => simp
+  | add x y hx hy =>
+    simp only [AddHom.toFun_eq_coe, coe_toAddHom, LinearEquiv.coe_coe, RingHom.id_apply] at hx hy ⊢
+    simp only [smul_add, map_add, hx, hy]
+  | tmul p n =>
+    simp only [smul_tmul', finsuppLeft_apply_tmul]
+    rw [Finsupp.smul_sum]
+    simp only [Finsupp.smul_single]
+    apply Finsupp.sum_smul_index'
+    simp
+
+/-- 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) := {
+  finsuppLeft with
+  map_smul' := finsuppLeft_smul' }
+
+lemma finsuppLeft'_apply (x : (ι →₀ M) ⊗[R] N) :
+    finsuppLeft' (S := S) x = finsuppLeft 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 ι) (LinearEquiv.refl R N)).trans
+    (f.trans (finsuppLEquivDirectSum S (M ⊗[R] N) ι).symm) -/
+
+/-- The tensor product of `i →₀ R` and `N` is linearly equivalent to `i →₀ N` -/
+noncomputable def finsuppScalarLeft :
+    (ι →₀ R) ⊗[R] N ≃ₗ[R] ι →₀ N :=
+  finsuppLeft.trans (Finsupp.mapRange.linearEquiv (TensorProduct.lid R N))
+
+lemma finsuppScalarLeft_apply_tmul_apply (p : ι →₀ R) (n : N) (i : ι) :
+    finsuppScalarLeft (p ⊗ₜ[R] n) i = (p i) • n := by
+  simp only [finsuppScalarLeft, LinearEquiv.trans_apply, finsuppLeft_apply_tmul,
+    Finsupp.mapRange.linearEquiv_apply, Finsupp.mapRange.linearMap_apply, LinearEquiv.coe_coe,
+    Finsupp.mapRange_apply, Finsupp.sum_apply]
+  apply symm
+  rw [← LinearEquiv.symm_apply_eq, lid_symm_apply]
+  rw [Finsupp.sum_eq_single i (fun _ _ => Finsupp.single_eq_of_ne) (fun _ => by simp)]
+  simp only [Finsupp.single_eq_same]
+  rw [tmul_smul, smul_tmul', smul_eq_mul, mul_one]
+
+lemma finsuppScalarLeft_apply_tmul (p : ι →₀ R) (n : N) :
+    finsuppScalarLeft (p ⊗ₜ[R] n) = p.sum (fun i m ↦ Finsupp.single i (m • n)) := by
+  ext i
+  rw [finsuppScalarLeft_apply_tmul_apply]
+  simp only [Finsupp.sum_apply]
+  rw [Finsupp.sum_eq_single i (fun _ _ => Finsupp.single_eq_of_ne) (fun _ => by simp)]
+  simp only [Finsupp.single_eq_same]
+
+lemma finsuppScalarLeft_symm_apply_single (i : ι) (n : N) :
+    finsuppScalarLeft.symm (Finsupp.single i n) =
+      (Finsupp.single i 1) ⊗ₜ[R] n := by
+  simp [finsuppScalarLeft, finsuppLeft_symm_apply_single]
+
+/-- The tensor product of `M` and `ι →₀ R` is linearly equivalent to `ι →₀ N` -/
+noncomputable def finsuppScalarRight :
+    M ⊗[R] (ι →₀ R) ≃ₗ[R] ι →₀ M :=
+  finsuppRight.trans (Finsupp.mapRange.linearEquiv (TensorProduct.rid R M))
+
+lemma finsuppScalarRight_apply_tmul_apply (m : M) (p : ι →₀ R) (i : ι) :
+    finsuppScalarRight (m ⊗ₜ[R] p) i = (p i) • m := by
+  simp only [finsuppScalarRight, LinearEquiv.trans_apply, finsuppRight_apply_tmul,
+    Finsupp.mapRange.linearEquiv_apply, Finsupp.mapRange.linearMap_apply, LinearEquiv.coe_coe,
+    Finsupp.mapRange_apply, Finsupp.sum_apply]
+  apply symm
+  rw [← LinearEquiv.symm_apply_eq, rid_symm_apply]
+  rw [Finsupp.sum_eq_single i (fun _ _ => Finsupp.single_eq_of_ne) (fun _ => by simp)]
+  simp only [Finsupp.single_eq_same]
+  rw [smul_tmul, smul_eq_mul, mul_one]
+
+lemma finsuppScalarRight_apply_tmul (m : M) (p : ι →₀ R) :
+    finsuppScalarRight (m ⊗ₜ[R] p) = p.sum (fun i n ↦ Finsupp.single i (n • m)) := by
+  ext i
+  rw [finsuppScalarRight_apply_tmul_apply]
+  simp only [Finsupp.sum_apply]
+  rw [Finsupp.sum_eq_single i (fun _ _ => Finsupp.single_eq_of_ne) (fun _ => by simp)]
+  simp only [Finsupp.single_eq_same]
+
+lemma finsuppScalarRight_symm_apply_single (i : ι) (m : M) :
+    finsuppScalarRight.symm (Finsupp.single i m) =
+      m ⊗ₜ[R] (Finsupp.single i 1) := by
+  simp [finsuppScalarRight, finsuppRight_symm_apply_single]
+
+end TensorProduct
+
+end TensorProduct
 
 open scoped Classical in
 -- `noncomputable` is a performance workaround for mathlib4#7103
 /-- The tensor product of `ι →₀ M` and `κ →₀ N` is linearly equivalent to `(ι × κ) →₀ (M ⊗ N)`. -/
-noncomputable def finsuppTensorFinsupp (R M N ι κ : Sort _) [CommSemiring R] [AddCommMonoid M]
-    [Module R M] [AddCommMonoid N] [Module R N] : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[R] ι × κ →₀ M ⊗[R] N :=
+noncomputable def finsuppTensorFinsupp (R M N ι κ : Sort _)
+    [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] :
+    (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[R] ι × κ →₀ M ⊗[R] N :=
   TensorProduct.congr (finsuppLEquivDirectSum R M ι) (finsuppLEquivDirectSum R N κ) ≪≫ₗ
     ((TensorProduct.directSum R (fun _ : ι => M) fun _ : κ => N) ≪≫ₗ
       (finsuppLEquivDirectSum R (M ⊗[R] N) (ι × κ)).symm)
@@ -103,4 +308,4 @@ theorem finsuppTensorFinsupp'_single_tmul_single (a : α) (b : β) (r₁ r₂ :
   aesop (add norm [Finsupp.single_apply])
 #align finsupp_tensor_finsupp'_single_tmul_single finsuppTensorFinsupp'_single_tmul_single
 
-end TensorProduct
+end