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

Mathlib/Algebra/DirectSum/Finsupp.lean

@@ -24,7 +24,7 @@ open DirectSum
 
 open LinearMap Submodule
 
-variable {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M]
+variable {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M]
 
 section finsuppLequivDirectSum
 

Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

@@ -1,18 +1,52 @@
 /-
 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
 import Mathlib.LinearAlgebra.DirectSum.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Tower
 
 #align_import linear_algebra.direct_sum.finsupp from "leanprover-community/mathlib"@"9b9d125b7be0930f564a68f1d73ace10cf46064d"
 
 /-!
 # Results on finitely supported functions.
 
-The tensor product of `ι →₀ M` and `κ →₀ N` is linearly equivalent to `(ι × κ) →₀ (M ⊗ N)`.
+* `Finsupp.rTensor`, the tensor product of `i →₀ M` and `N` is linearly equivalent to `i →₀ M ⊗[R] N`
+
+* `Finsupp.lTensor`, the tensor product of `M` and `i →₀ N` is linearly equivalent to `i →₀ M ⊗[R] N`
+
+* `Finsupp.rTensor'`, if `M` is an `S`-module, then the tensor product of `i →₀ M` and `N` is `S`-linearly equivalent to `i →₀ 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) :=
+  Finsupp.rTensor'
+
+noncomputable def MvPolynomial.rTensor :
+    MvPolynomial σ R ⊗[R] N ≃ₗ[R] (σ →₀ ℕ) →₀ N :=
+  (MvPolynomial.rTensor' σ (S := R) (N := N) (R := R)).trans
+    (Finsupp.mapRange.linearEquiv (TensorProduct.lid R N))
+```
+
+## 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 `Finsupp.rTensor'` using existing heterobasic version of `TensorProduct.congr`
 -/
 
 
@@ -24,36 +58,134 @@
 
 open Set LinearMap Submodule
 
-variable {R : Type u} {M : Type v} {N : Type w} [Ring R] [AddCommGroup M] [Module R M]
-  [AddCommGroup N] [Module R N]
+variable {R : Type u} {M : Type v} {N : Type w}
+  [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
 
 section TensorProduct
 
 open TensorProduct
 
-open TensorProduct
+variable {ι : Type*} [DecidableEq ι]
+
+/-- The tensor product of `i →₀ M` and `N` is linearly equivalent to `i →₀ M ⊗[R] N` -/
+noncomputable def Finsupp.rTensor :
+    (ι →₀ M) ⊗[R] N ≃ₗ[R] ι →₀ (M ⊗[R] N) :=
+  (TensorProduct.congr (finsuppLEquivDirectSum R M ι) (LinearEquiv.refl R N)).trans
+    ((TensorProduct.directSumLeft R (fun _ : ι => M) N).trans
+      (finsuppLEquivDirectSum R (M ⊗[R] N) ι).symm)
+
+lemma Finsupp.rTensor_apply_tmul (p : ι →₀ M) (n : N) :
+    Finsupp.rTensor (p ⊗ₜ[R] n) = p.sum (fun i m ↦ Finsupp.single i (m ⊗ₜ[R] n)) := by
+  simp [Finsupp.rTensor]
+  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 Finsupp.rTensor_apply_tmul_apply (p : ι →₀ M) (n : N) (i : ι) :
+    Finsupp.rTensor (p ⊗ₜ[R] n) i = p i ⊗ₜ[R] n := by
+  rw [Finsupp.rTensor_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 Finsupp.rTensor_symm_apply_single (i : ι) (m : M) (n : N) :
+    Finsupp.rTensor.symm (Finsupp.single i (m ⊗ₜ[R] n)) =
+      Finsupp.single i m ⊗ₜ[R] n := by
+  simp [Finsupp.rTensor, Finsupp.lsum]
+
+/-- The tensor product of `M` and `i →₀ N` is linearly equivalent to `i →₀ M ⊗[R] N` -/
+noncomputable def Finsupp.lTensor₀ :
+    M ⊗[R] (ι →₀ N) ≃ₗ[R] ι →₀ (M ⊗[R] N) :=
+  ((TensorProduct.comm R _ _).trans
+    (Finsupp.rTensor (ι := ι) (M := N) (N := M) (R := R))).trans
+      (Finsupp.mapRange.linearEquiv (TensorProduct.comm R _ _))
+
+/-- The tensor product of `M` and `i →₀ N` is linearly equivalent to `i →₀ M ⊗[R] N` -/
+noncomputable def Finsupp.lTensor :
+    M ⊗[R] (ι →₀ N) ≃ₗ[R] ι →₀ (M ⊗[R] N) :=
+  (TensorProduct.congr (LinearEquiv.refl R M) (finsuppLEquivDirectSum R N ι)).trans
+    ((TensorProduct.directSumRight R M (fun _ : ι => N)).trans
+      (finsuppLEquivDirectSum R (M ⊗[R] N) ι).symm)
+
+lemma Finsupp.lTensor_apply_tmul (m : M) (p : ι →₀ N) :
+    Finsupp.lTensor (m ⊗ₜ[R] p) = p.sum (fun i n ↦ Finsupp.single i (m ⊗ₜ[R] n)) := by
+  simp [Finsupp.lTensor]
+  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 Finsupp.lTensor_symm_apply_single (i : ι) (m : M) (n : N) :
+    Finsupp.rTensor.symm (Finsupp.single i (m ⊗ₜ[R] n)) =
+      Finsupp.single i m ⊗ₜ[R] n := by
+  simp [Finsupp.rTensor, Finsupp.lsum]
+
+variable {S : Type*} [CommSemiring S] [Algebra R S]
+  [Module S M] [IsScalarTower R S M]
+
+lemma Finsupp.rTensor_smul' (s : S) (t : (ι →₀ M) ⊗[R] N) :
+    Finsupp.rTensor (s • t) = s • Finsupp.rTensor 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 [TensorProduct.smul_tmul', rTensor_apply_tmul]
+    rw [Finsupp.smul_sum]
+    simp only [smul_single]
+    apply Finsupp.sum_smul_index'
+    simp
+
+/-- When `M` is also an `S`-module, then `Finsupp.rTensor R M N``
+  is an `S`-linear equiv -/
+noncomputable def Finsupp.rTensor' :
+    (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ (M ⊗[R] N) := {
+  Finsupp.rTensor with
+  map_smul' := Finsupp.rTensor_smul' }
+
+/- -- 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 (TensorProduct.AlgebraTensorModule.congr
+    (finsuppLEquivDirectSum S M ι) (LinearEquiv.refl R N)).trans
+    (f.trans (finsuppLEquivDirectSum S (M ⊗[R] N) ι).symm) -/
 
 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 _) [CommRing R] [AddCommGroup M]
-    [Module R M] [AddCommGroup 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)
 #align finsupp_tensor_finsupp finsuppTensorFinsupp
 
 @[simp]
-theorem finsuppTensorFinsupp_single (R M N ι κ : Sort _) [CommRing R] [AddCommGroup M] [Module R M]
-    [AddCommGroup N] [Module R N] (i : ι) (m : M) (k : κ) (n : N) :
+theorem finsuppTensorFinsupp_single (R M N ι κ : Sort _) [CommSemiring R] [AddCommMonoid M] [Module R M]
+    [AddCommMonoid N] [Module R N] (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]
 #align finsupp_tensor_finsupp_single finsuppTensorFinsupp_single
 
 @[simp]
-theorem finsuppTensorFinsupp_apply (R M N ι κ : Sort _) [CommRing R] [AddCommGroup M] [Module R M]
-    [AddCommGroup N] [Module R N] (f : ι →₀ M) (g : κ →₀ N) (i : ι) (k : κ) :
+theorem finsuppTensorFinsupp_apply (R M N ι κ : Sort _) [CommSemiring R] [AddCommMonoid M] [Module R M]
+    [AddCommMonoid N] [Module R N] (f : ι →₀ M) (g : κ →₀ N) (i : ι) (k : κ) :
     finsuppTensorFinsupp R M N ι κ (f ⊗ₜ g) (i, k) = f i ⊗ₜ g k := by
   apply Finsupp.induction_linear f
   · simp
@@ -75,15 +207,15 @@
 #align finsupp_tensor_finsupp_apply finsuppTensorFinsupp_apply
 
 @[simp]
-theorem finsuppTensorFinsupp_symm_single (R M N ι κ : Sort _) [CommRing R] [AddCommGroup M]
-    [Module R M] [AddCommGroup N] [Module R N] (i : ι × κ) (m : M) (n : N) :
+theorem finsuppTensorFinsupp_symm_single (R M N ι κ : Sort _) [CommSemiring R] [AddCommMonoid M]
+    [Module R M] [AddCommMonoid N] [Module R N] (i : ι × κ) (m : M) (n : N) :
     (finsuppTensorFinsupp R M N ι κ).symm (Finsupp.single i (m ⊗ₜ n)) =
       Finsupp.single i.1 m ⊗ₜ Finsupp.single i.2 n :=
   Prod.casesOn i fun _ _ =>
     (LinearEquiv.symm_apply_eq _).2 (finsuppTensorFinsupp_single _ _ _ _ _ _ _ _ _).symm
 #align finsupp_tensor_finsupp_symm_single finsuppTensorFinsupp_symm_single
 
-variable (S : Type*) [CommRing S] (α β : Type*)
+variable (S : Type*) [CommSemiring S] (α β : Type*)
 
 /-- A variant of `finsuppTensorFinsupp` where both modules are the ground ring. -/
 def finsuppTensorFinsupp' : (α →₀ S) ⊗[S] (β →₀ S) ≃ₗ[S] α × β →₀ S :=

Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

@@ -35,17 +35,17 @@ open LinearMap
 
 attribute [local ext] TensorProduct.ext
 
-variable (R : Type u) [CommRing R]
+variable (R : Type u) [CommSemiring R]
 
 variable {ι₁ : Type v₁} {ι₂ : Type v₂}
 
 variable [DecidableEq ι₁] [DecidableEq ι₂]
 
 variable (M₁ : ι₁ → Type w₁) (M₁' : Type w₁') (M₂ : ι₂ → Type w₂) (M₂' : Type w₂')
 
-variable [∀ i₁, AddCommGroup (M₁ i₁)] [AddCommGroup M₁']
+variable [∀ i₁, AddCommMonoid (M₁ i₁)] [AddCommMonoid M₁']
 
-variable [∀ i₂, AddCommGroup (M₂ i₂)] [AddCommGroup M₂']
+variable [∀ i₂, AddCommMonoid (M₂ i₂)] [AddCommMonoid M₂']
 
 variable [∀ i₁, Module R (M₁ i₁)] [Module R M₁'] [∀ i₂, Module R (M₂ i₂)] [Module R M₂']
 

Mathlib/LinearAlgebra/TensorProduct/MvPolynomial.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2024 Antoine Chambert-Loir. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Antoine Chambert-Loir
+-/
+
+import Mathlib.LinearAlgebra.DirectSum.Finsupp
+import Mathlib.Data.MvPolynomial.Basic
+import Mathlib.RingTheory.TensorProduct
+/-!
+
+# Tensor Product of polynomial rings
+
+-/
+
+
+universe u v w
+
+noncomputable section
+
+open DirectSum TensorProduct
+
+open Set LinearMap Submodule
+
+variable {R : Type u} {M : Type v} {N : Type w}
+  [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
+
+variable (σ : Type u) [DecidableEq σ]
+
+variable {S : Type*} [CommSemiring S] [Algebra R S]
+
+noncomputable def MvPolynomial.rTensor' :
+    MvPolynomial σ S ⊗[R] N ≃ₗ[S] (σ →₀ ℕ) →₀ (S ⊗[R] N) :=
+  Finsupp.rTensor'
+
+noncomputable def MvPolynomial.rTensor :
+    MvPolynomial σ R ⊗[R] N ≃ₗ[R] (σ →₀ ℕ) →₀ N := by
+  exact (MvPolynomial.rTensor' σ (S := R) (N := N) (R := R)).trans
+    (Finsupp.mapRange.linearEquiv (TensorProduct.lid R N))
+
+end
+
+section MonoidAlgebra
+
+open TensorProduct
+variable (α : Type*) [Monoid α] [DecidableEq α]
+  (R : Type*) [CommSemiring R]
+  (N : Type*) [Semiring N] [Algebra R N]
+
+noncomputable example : Semiring (MonoidAlgebra R α) := inferInstance
+
+noncomputable example : Algebra R (MonoidAlgebra R α) := inferInstance
+
+noncomputable example : Semiring ((MonoidAlgebra R α) ⊗[R] N) := inferInstance
+
+noncomputable example : Algebra R ((MonoidAlgebra R α) ⊗[R] N) := inferInstance
+
+#check Finsupp.rTensor (R := R) (ι := α) (M := R) (N := N)
+
+variable {α R N}
+
+noncomputable def MonoidAlgebra.AlgEquiv {N' : Type*} [Semiring N'] [Algebra R N'] (e : N ≃ₐ[R] N') :
+    MonoidAlgebra N α ≃ₐ[R] MonoidAlgebra N' α := {
+  Finsupp.mapRange.linearEquiv e.toLinearEquiv with
+  map_mul' := sorry
+  commutes' := sorry  }
+
+noncomputable def MonoidAlgebra.rTensorEquiv :
+    (MonoidAlgebra R α) ⊗[R] N ≃ₗ[R] MonoidAlgebra N α :=
+  (Finsupp.rTensor (R := R) (ι := α) (M := R) (N := N)).trans
+    (MonoidAlgebra.AlgEquiv (α := α) (Algebra.TensorProduct.lid R N)).toLinearEquiv
+
+example (f g : (MonoidAlgebra R α) ⊗[R] N) :
+    MonoidAlgebra.rTensorEquiv (N := N) (R := R) (f * g) = MonoidAlgebra.rTensorEquiv f * MonoidAlgebra.rTensorEquiv g := by
+  induction f using TensorProduct.induction_on with
+  | zero => simp only [zero_mul, LinearEquiv.map_zero]
+  | tmul f n => sorry
+  | add => sorry
+
+noncomputable example : (MonoidAlgebra R α) ⊗[R] N ≃ₐ[R] MonoidAlgebra N α := {
+  MonoidAlgebra.rTensorEquiv with
+  map_mul' := fun f g ↦ by
+    simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe,
+      LinearEquiv.trans_apply]
+    apply MonoidAlgebra.induction_on
+    · intro a
+      apply MonoidAlgebra.induction_on
+      · intro b
+        simp only [MonoidAlgebra.of_apply]
+        sorry
+      · sorry
+      · sorry
+    · sorry -- add
+    · sorry -- hsmul
+  commutes' := sorry }