[Merged by Bors] - feat(Mathlib.RingTheory.TensorProduct.MvPolynomial) : tensor product of a (multivariate) polynomial ring

Mathlib.lean

@@ -3465,6 +3465,7 @@ import Mathlib.RingTheory.Subsemiring.Basic
 import Mathlib.RingTheory.Subsemiring.Order
 import Mathlib.RingTheory.Subsemiring.Pointwise
 import Mathlib.RingTheory.TensorProduct.Basic
+import Mathlib.RingTheory.TensorProduct.MvPolynomial
 import Mathlib.RingTheory.Trace
 import Mathlib.RingTheory.UniqueFactorizationDomain
 import Mathlib.RingTheory.Unramified.Basic

Mathlib/Algebra/Lie/TensorProduct.lean

@@ -60,10 +60,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
 
@@ -91,9 +88,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]
-      abel }
+      simp [sub_add_eq_sub_sub_swap] }
 #align tensor_product.lie_module.lift TensorProduct.LieModule.lift
 
 @[simp]

Mathlib/Algebra/MvPolynomial/Basic.lean

@@ -645,6 +645,20 @@ def coeffAddMonoidHom (m : σ →₀ ℕ) : MvPolynomial σ R →+ R
   map_add' := coeff_add m
 #align mv_polynomial.coeff_add_monoid_hom MvPolynomial.coeffAddMonoidHom
 
+variable (R)
+/-- `MvPolynomial.coeff m` but promoted to a `LinearMap`. -/
+def lcoeff (m : σ →₀ ℕ) : MvPolynomial σ R →ₗ[R] R where
+  toFun := coeff m
+  map_add' := coeff_add m
+  map_smul' := coeff_smul m
+
+variable {R}
+
+@[simp]
+theorem lcoeff_apply (m : σ →₀ ℕ) (f : MvPolynomial σ R) :
+    lcoeff R m f = coeff m f :=
+  rfl
+
 theorem coeff_sum {X : Type*} (s : Finset X) (f : X → MvPolynomial σ R) (m : σ →₀ ℕ) :
     coeff m (∑ x in s, f x) = ∑ x in s, coeff m (f x) :=
   map_sum (@coeffAddMonoidHom R σ _ _) _ s

Mathlib/Data/Finsupp/Basic.lean

@@ -214,6 +214,11 @@ def mapRange.addMonoidHom (f : M →+ N) : (α →₀ M) →+ α →₀ N
   map_add' a b := by dsimp only; exact mapRange_add f.map_add _ _; -- Porting note: `dsimp` needed
 #align finsupp.map_range.add_monoid_hom Finsupp.mapRange.addMonoidHom
 
+lemma mapRange.addMonoidHom_apply_single
+    [AddCommMonoid N] [AddCommMonoid P] (e : N →+ P) (a : α) (n : N) :
+    mapRange.addMonoidHom e (single a n) = single a (e n) := by
+    simp only [addMonoidHom_apply, mapRange_single]
+
 @[simp]
 theorem mapRange.addMonoidHom_id :
     mapRange.addMonoidHom (AddMonoidHom.id M) = AddMonoidHom.id (α →₀ M) :=

Mathlib/Data/Finsupp/Defs.lean

@@ -455,6 +455,13 @@ theorem unique_single_eq_iff [Unique α] {b' : M} : single a b = single a' b' 
   rw [unique_ext_iff, Unique.eq_default a, Unique.eq_default a', single_eq_same, single_eq_same]
 #align finsupp.unique_single_eq_iff Finsupp.unique_single_eq_iff
 
+lemma apply_single [AddCommMonoid N] [AddCommMonoid P]
+    (e : N →+ P) (a : α) (n : N) (b : α) :
+    e ((single a n) b) = single a (e n) b := by
+  classical
+  simp only [single_apply]
+  split_ifs; rfl; exact map_zero e
+
 theorem support_eq_singleton {f : α →₀ M} {a : α} :
     f.support = {a} ↔ f a ≠ 0 ∧ f = single a (f a) :=
   ⟨fun h =>

Mathlib/RingTheory/TensorProduct/MvPolynomial.lean

@@ -0,0 +1,169 @@
+/-
+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.Algebra.MvPolynomial.Basic
+import Mathlib.RingTheory.TensorProduct.Basic
+import Mathlib.Algebra.MvPolynomial.Equiv
+/-!
+
+# Tensor Product of (multivariate) polynomial rings
+
+* `MvPolynomial.rTensor`, `MvPolynomial.scalarRTensor`:  the tensor product of
+  a polynomial algebra by a module is linearly equivalent
+  to a Finsupp of a tensor product
+* `MvPolynomial.rTensorAlgHom`, the algebra morphism from the tensor product
+  of a polynomial algebra by an algebra to a polynomial algebra
+* `MvPolynomial.rTensorAlgEquiv`, `MvPolynomial.scalarRTensorAlgEquiv`,
+  the tensor product of a polynomial algebra by an algebra
+  is algebraically equivalent to a polynomial algebra
+
+## TODO :
+* `MvPolynomial.rTensor` could be phrased in terms of `AddMonoidAlgebra`, and
+  `MvPolynomial.rTensor` then has `smul` by the polynomial algebra.
+* `MvPolynomial.rTensorAlgHom` and `MvPolynomial.scalarRTensorAlgEquiv`
+  are morphisms for the algebra structure by `MvPolynomial σ R`.
+-/
+
+
+universe u v w
+
+noncomputable section
+
+namespace MvPolynomial
+
+open DirectSum TensorProduct
+
+open Set LinearMap Submodule
+
+variable {R : Type u} {M : Type v} {N : Type w}
+  [CommSemiring R] [AddCommMonoid M] [Module R M]
+
+variable {σ : Type*} [DecidableEq σ]
+
+variable {S : Type*} [CommSemiring S] [Algebra R S]
+
+section Module
+
+variable   [AddCommMonoid N] [Module R N]
+
+/-- The tensor product of a polynomial ring by a module is
+  linearly equivalent to a Finsupp of a tensor product -/
+noncomputable def rTensor :
+    MvPolynomial σ S ⊗[R] N ≃ₗ[S] (σ →₀ ℕ) →₀ (S ⊗[R] N) :=
+  TensorProduct.finsuppLeft' _ _ _ _ _
+
+lemma rTensor_apply_tmul (p : MvPolynomial σ S) (n : N) :
+    rTensor (p ⊗ₜ[R] n) = p.sum (fun i m ↦ Finsupp.single i (m ⊗ₜ[R] n)) :=
+  TensorProduct.finsuppLeft_apply_tmul p n
+
+lemma rTensor_apply_tmul_apply (p : MvPolynomial σ S) (n : N) (d : σ →₀ ℕ) :
+    rTensor (p ⊗ₜ[R] n) d = (coeff d p) ⊗ₜ[R] n :=
+  TensorProduct.finsuppLeft_apply_tmul_apply p n d
+
+lemma rTensor_apply (t : MvPolynomial σ S ⊗[R] N) (d : σ →₀ ℕ) :
+    rTensor t d = ((lcoeff S d).restrictScalars R).rTensor N t :=
+  TensorProduct.finsuppLeft_apply t d
+
+lemma rTensor_symm_apply_single (d : σ →₀ ℕ) (s : S) (n : N) :
+    rTensor.symm (Finsupp.single d (s ⊗ₜ n)) =
+      (monomial d s) ⊗ₜ[R] n :=
+  TensorProduct.finsuppLeft_symm_apply_single d s n
+
+/-- The tensor product of the polynomial algebra by a module
+  is linearly equivalent to a Finsupp of that module -/
+noncomputable def scalarRTensor :
+    MvPolynomial σ R ⊗[R] N ≃ₗ[R] (σ →₀ ℕ) →₀ N :=
+  TensorProduct.finsuppScalarLeft _ _ _
+
+lemma scalarRTensor_apply_tmul (p : MvPolynomial σ R) (n : N) :
+    scalarRTensor (p ⊗ₜ[R] n) = p.sum (fun i m ↦ Finsupp.single i (m • n)) :=
+  TensorProduct.finsuppScalarLeft_apply_tmul p n
+
+lemma scalarRTensor_apply_tmul_apply (p : MvPolynomial σ R) (n : N) (d : σ →₀ ℕ):
+    scalarRTensor (p ⊗ₜ[R] n) d = (coeff d p) • n :=
+  TensorProduct.finsuppScalarLeft_apply_tmul_apply p n d
+
+lemma scalarRTensor_symm_apply_single (d : σ →₀ ℕ) (n : N) :
+    scalarRTensor.symm (Finsupp.single d n) = (monomial d 1) ⊗ₜ[R] n :=
+  TensorProduct.finsuppScalarLeft_symm_apply_single d n
+
+end Module
+
+section Algebra
+
+variable [CommSemiring N] [Algebra R N]
+
+/-- The algebra morphism from a tensor product of a polynomial algebra
+  by an algebra to a polynomial algebra -/
+noncomputable def rTensorAlgHom :
+    (MvPolynomial σ S) ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N) :=
+  Algebra.TensorProduct.lift
+    (mapAlgHom Algebra.TensorProduct.includeLeft)
+    ((IsScalarTower.toAlgHom R (S ⊗[R] N) _).comp Algebra.TensorProduct.includeRight)
+    (fun p n => by simp [commute_iff_eq, algebraMap_eq, mul_comm])
+
+lemma rTensorAlgHom_coeff_tmul
+    (p : MvPolynomial σ S) (n : N) (d : σ →₀ ℕ) :
+    coeff d (rTensorAlgHom (p ⊗ₜ[R] n)) = (coeff d p) ⊗ₜ[R] n := by
+  rw [rTensorAlgHom, Algebra.TensorProduct.lift_tmul]
+  rw [AlgHom.coe_comp, IsScalarTower.coe_toAlgHom', Function.comp_apply,
+    Algebra.TensorProduct.includeRight_apply]
+  rw [algebraMap_eq, mul_comm, coeff_C_mul]
+  simp [mapAlgHom, coeff_map]
+
+lemma rTensorAlgHom_toLinearMap :
+    (rTensorAlgHom :
+      MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N)).toLinearMap =
+      (finsuppLeft' _ _ _ _ _).toLinearMap := by
+  ext d n e
+  dsimp only [AlgebraTensorModule.curry_apply, TensorProduct.curry_apply,
+    LinearMap.coe_restrictScalars, AlgHom.toLinearMap_apply]
+  simp only [coe_comp, Function.comp_apply, AlgebraTensorModule.curry_apply, curry_apply,
+    LinearMap.coe_restrictScalars, AlgHom.toLinearMap_apply]
+  rw [rTensorAlgHom_coeff_tmul]
+  simp only [coeff]
+  erw [finsuppLeft_apply_tmul_apply]
+
+lemma rTensorAlgHom_toLinearMap' :
+    (rTensorAlgHom :
+      MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N)).toLinearMap.restrictScalars R =
+      (finsuppLeft _ _ _ _).toLinearMap := by
+  rw [rTensorAlgHom_toLinearMap]
+  rfl
+
+lemma rTensorAlgHom_apply_eq (p : MvPolynomial σ S ⊗[R] N) :
+    rTensorAlgHom (S := S) p = finsuppLeft' _ _ _ _ S  p := by
+  rw [← AlgHom.toLinearMap_apply, rTensorAlgHom_toLinearMap]
+  rfl
+
+/-- The tensor product of a polynomial algebra by an algebra
+  is algebraically equivalent to a polynomial algebra -/
+noncomputable def rTensorAlgEquiv :
+    (MvPolynomial σ S) ⊗[R] N ≃ₐ[S] MvPolynomial σ (S ⊗[R] N) := by
+  apply AlgEquiv.ofLinearEquiv
+    (finsuppLeft' _ _ _ _ _ : MvPolynomial σ S ⊗[R] N ≃ₗ[S] MvPolynomial σ (S ⊗[R] N))
+  · simp only [Algebra.TensorProduct.one_def]
+    apply symm
+    rw [← LinearEquiv.symm_apply_eq]
+    exact finsuppLeft_symm_apply_single (0 : σ →₀ ℕ) (1 : S) (1 : N)
+  · intro x y
+    erw [← rTensorAlgHom_apply_eq (S := S)]
+    simp only [_root_.map_mul, rTensorAlgHom_apply_eq]
+    rfl
+
+/-- The tensor product of the polynomial algebra by an algebra
+  is algebraically equivalent to a polynomial algebra with
+  coefficients in that algegra -/
+noncomputable def scalarRTensorAlgEquiv :
+    MvPolynomial σ R ⊗[R] N ≃ₐ[R] MvPolynomial σ N :=
+  rTensorAlgEquiv.trans (mapAlgEquiv σ (Algebra.TensorProduct.lid R N))
+
+end Algebra
+
+end MvPolynomial
+
+end