Tensor Product of (multivariate) polynomial rings

Let Semiring R, Algebra R S and Module R N.

• MvPolynomial.rTensor gives the linear equivalence MvPolynomial σ S ⊗[R] N ≃ₗ[R] (σ →₀ ℕ) →₀ (S ⊗[R] N) characterized, for p : MvPolynomial σ S, n : N and d : σ →₀ ℕ, by rTensor (p ⊗ₜ[R] n) d = (coeff d p) ⊗ₜ[R] n

• MvPolynomial.scalarRTensor gives the linear equivalence MvPolynomial σ R ⊗[R] N ≃ₗ[R] (σ →₀ ℕ) →₀ N such that MvPolynomial.scalarRTensor (p ⊗ₜ[R] n) d = coeff d p • n for p : MvPolynomial σ R, n : N and d : σ →₀ ℕ, by

• 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.

noncomputable def MvPolynomial.rTensor {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] [DecidableEq σ] [AddCommMonoid N] [Module R N] : TensorProduct R (MvPolynomial σ S) N ≃ₗ[S] (σ →₀ ℕ) →₀ TensorProduct R S N

The tensor product of a polynomial ring by a module is linearly equivalent to a Finsupp of a tensor product

theorem MvPolynomial.rTensor_apply_tmul {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] [DecidableEq σ] [AddCommMonoid N] [Module R N] (p : MvPolynomial σ S) (n : N) : rTensor (p ⊗ₜ[R] n) = Finsupp.sum p fun (i : σ →₀ ℕ) (m : S) => fun₀ | i => m ⊗ₜ[R] n

theorem MvPolynomial.rTensor_apply_tmul_apply {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] [DecidableEq σ] [AddCommMonoid N] [Module R N] (p : MvPolynomial σ S) (n : N) (d : σ →₀ ℕ) : (rTensor (p ⊗ₜ[R] n)) d = coeff d p ⊗ₜ[R] n

theorem MvPolynomial.rTensor_apply_monomial_tmul {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] [DecidableEq σ] [AddCommMonoid N] [Module R N] (e : σ →₀ ℕ) (s : S) (n : N) (d : σ →₀ ℕ) : (rTensor ((monomial e) s ⊗ₜ[R] n)) d = if e = d then s ⊗ₜ[R] n else 0

theorem MvPolynomial.rTensor_apply_X_tmul {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] [DecidableEq σ] [AddCommMonoid N] [Module R N] (s : σ) (n : N) (d : σ →₀ ℕ) : (rTensor (X s ⊗ₜ[R] n)) d = if (fun₀ | s => 1) = d then 1 ⊗ₜ[R] n else 0

theorem MvPolynomial.rTensor_apply {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] [DecidableEq σ] [AddCommMonoid N] [Module R N] (t : TensorProduct R (MvPolynomial σ S) N) (d : σ →₀ ℕ) : (rTensor t) d = (LinearMap.rTensor N (↑R (lcoeff S d))) t

@[simp]

theorem MvPolynomial.rTensor_symm_apply_single {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] [DecidableEq σ] [AddCommMonoid N] [Module R N] (d : σ →₀ ℕ) (s : S) (n : N) : (rTensor.symm fun₀ | d => s ⊗ₜ[R] n) = (monomial d) s ⊗ₜ[R] n

noncomputable def MvPolynomial.scalarRTensor {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} [DecidableEq σ] [AddCommMonoid N] [Module R N] : TensorProduct R (MvPolynomial σ R) N ≃ₗ[R] (σ →₀ ℕ) →₀ N

The tensor product of the polynomial algebra by a module is linearly equivalent to a Finsupp of that module

theorem MvPolynomial.scalarRTensor_apply_tmul {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} [DecidableEq σ] [AddCommMonoid N] [Module R N] (p : MvPolynomial σ R) (n : N) : scalarRTensor (p ⊗ₜ[R] n) = Finsupp.sum p fun (i : σ →₀ ℕ) (m : R) => fun₀ | i => m • n

theorem MvPolynomial.scalarRTensor_apply_tmul_apply {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} [DecidableEq σ] [AddCommMonoid N] [Module R N] (p : MvPolynomial σ R) (n : N) (d : σ →₀ ℕ) : (scalarRTensor (p ⊗ₜ[R] n)) d = coeff d p • n

theorem MvPolynomial.scalarRTensor_apply_monomial_tmul {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} [DecidableEq σ] [AddCommMonoid N] [Module R N] (e : σ →₀ ℕ) (r : R) (n : N) (d : σ →₀ ℕ) : (scalarRTensor ((monomial e) r ⊗ₜ[R] n)) d = if e = d then r • n else 0

theorem MvPolynomial.scalarRTensor_apply_X_tmul_apply {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} [DecidableEq σ] [AddCommMonoid N] [Module R N] (s : σ) (n : N) (d : σ →₀ ℕ) : (scalarRTensor (X s ⊗ₜ[R] n)) d = if (fun₀ | s => 1) = d then n else 0

theorem MvPolynomial.scalarRTensor_symm_apply_single {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} [DecidableEq σ] [AddCommMonoid N] [Module R N] (d : σ →₀ ℕ) (n : N) : (scalarRTensor.symm fun₀ | d => n) = (monomial d) 1 ⊗ₜ[R] n

noncomputable def MvPolynomial.rTensorAlgHom {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] [CommSemiring N] [Algebra R N] : TensorProduct R (MvPolynomial σ S) N →ₐ[S] MvPolynomial σ (TensorProduct R S N)

The algebra morphism from a tensor product of a polynomial algebra by an algebra to a polynomial algebra

@[simp]

theorem MvPolynomial.coeff_rTensorAlgHom_tmul {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] [CommSemiring N] [Algebra R N] (p : MvPolynomial σ S) (n : N) (d : σ →₀ ℕ) : coeff d (rTensorAlgHom (p ⊗ₜ[R] n)) = coeff d p ⊗ₜ[R] n

theorem MvPolynomial.coeff_rTensorAlgHom_monomial_tmul {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] [CommSemiring N] [Algebra R N] [DecidableEq σ] (e : σ →₀ ℕ) (s : S) (n : N) (d : σ →₀ ℕ) : coeff d (rTensorAlgHom ((monomial e) s ⊗ₜ[R] n)) = if e = d then s ⊗ₜ[R] n else 0

theorem MvPolynomial.rTensorAlgHom_toLinearMap {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] [CommSemiring N] [Algebra R N] [DecidableEq σ] : rTensorAlgHom.toLinearMap = ↑rTensor

theorem MvPolynomial.rTensorAlgHom_apply_eq {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] [CommSemiring N] [Algebra R N] [DecidableEq σ] (p : TensorProduct R (MvPolynomial σ S) N) : rTensorAlgHom p = rTensor p

noncomputable def MvPolynomial.rTensorAlgEquiv {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] [CommSemiring N] [Algebra R N] [DecidableEq σ] : TensorProduct R (MvPolynomial σ S) N ≃ₐ[S] MvPolynomial σ (TensorProduct R S N)

The tensor product of a polynomial algebra by an algebra is algebraically equivalent to a polynomial algebra

@[simp]

theorem MvPolynomial.rTensorAlgEquiv_apply {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] [CommSemiring N] [Algebra R N] [DecidableEq σ] (x : TensorProduct R (MvPolynomial σ S) N) : rTensorAlgEquiv x = rTensorAlgHom x

noncomputable def MvPolynomial.scalarRTensorAlgEquiv {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} [CommSemiring N] [Algebra R N] [DecidableEq σ] : TensorProduct R (MvPolynomial σ R) N ≃ₐ[R] MvPolynomial σ N

The tensor product of the polynomial algebra by an algebra is algebraically equivalent to a polynomial algebra with coefficients in that algebra

noncomputable def MvPolynomial.algebraTensorAlgEquiv (R : Type u) [CommSemiring R] {σ : Type u_1} (A : Type u_4) [CommSemiring A] [Algebra R A] : TensorProduct R A (MvPolynomial σ R) ≃ₐ[A] MvPolynomial σ A

Tensoring MvPolynomial σ R on the left by an R-algebra A is algebraically equivalent to MvPolynomial σ A.

@[simp]

theorem MvPolynomial.algebraTensorAlgEquiv_tmul (R : Type u) [CommSemiring R] {σ : Type u_1} (A : Type u_4) [CommSemiring A] [Algebra R A] (a : A) (p : MvPolynomial σ R) : (algebraTensorAlgEquiv R A) (a ⊗ₜ[R] p) = a • (map (algebraMap R A)) p

@[simp]

theorem MvPolynomial.algebraTensorAlgEquiv_symm_X (R : Type u) [CommSemiring R] {σ : Type u_1} (A : Type u_4) [CommSemiring A] [Algebra R A] (s : σ) : (algebraTensorAlgEquiv R A).symm (X s) = 1 ⊗ₜ[R] X s

@[simp]

theorem MvPolynomial.algebraTensorAlgEquiv_symm_monomial (R : Type u) [CommSemiring R] {σ : Type u_1} (A : Type u_4) [CommSemiring A] [Algebra R A] (m : σ →₀ ℕ) (a : A) : (algebraTensorAlgEquiv R A).symm ((monomial m) a) = a ⊗ₜ[R] (monomial m) 1

@[simp]

theorem MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval (R : Type u) [CommSemiring R] {σ : Type u_1} (A : Type u_4) [CommSemiring A] [Algebra R A] : (↑(AlgEquiv.restrictScalars R (algebraTensorAlgEquiv R A).symm)).comp (mapAlgHom (Algebra.ofId R A)) = Algebra.TensorProduct.includeRight

@[simp]

theorem MvPolynomial.algebraTensorAlgEquiv_symm_map (R : Type u) [CommSemiring R] {σ : Type u_1} (A : Type u_4) [CommSemiring A] [Algebra R A] (x : MvPolynomial σ R) : (algebraTensorAlgEquiv R A).symm ((map (algebraMap R A)) x) = 1 ⊗ₜ[R] x

theorem MvPolynomial.aeval_one_tmul (R : Type u) {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] [CommSemiring N] [Algebra R N] (f : σ → S) (p : MvPolynomial σ R) : (aeval fun (x : σ) => 1 ⊗ₜ[R] f x) p = 1 ⊗ₜ[R] (aeval f) p

def MvPolynomial.tensorEquivSum (R : Type u) [CommSemiring R] (σ : Type u_1) (ι : Type u_2) (S : Type u_3) [CommSemiring S] [Algebra R S] : TensorProduct R (MvPolynomial σ S) (MvPolynomial ι R) ≃ₐ[S] MvPolynomial (σ ⊕ ι) S

S[X] ⊗[R] R[Y] ≃ S[X, Y]

@[simp]

theorem MvPolynomial.tensorEquivSum_X_tmul_one {R : Type u} [CommSemiring R] {σ : Type u_1} {ι : Type u_2} {S : Type u_3} [CommSemiring S] [Algebra R S] (i : σ) : (tensorEquivSum R σ ι S) (X i ⊗ₜ[R] 1) = X (Sum.inl i)

@[simp]

theorem MvPolynomial.tensorEquivSum_C_tmul_one {R : Type u} [CommSemiring R] {σ : Type u_1} {ι : Type u_2} {S : Type u_3} [CommSemiring S] [Algebra R S] (r : S) : (tensorEquivSum R σ ι S) (C r ⊗ₜ[R] 1) = C r

@[simp]

theorem MvPolynomial.tensorEquivSum_one_tmul_X {R : Type u} [CommSemiring R] {σ : Type u_1} {ι : Type u_2} {S : Type u_3} [CommSemiring S] [Algebra R S] (i : ι) : (tensorEquivSum R σ ι S) (1 ⊗ₜ[R] X i) = X (Sum.inr i)

@[simp]

theorem MvPolynomial.tensorEquivSum_one_tmul_C {R : Type u} [CommSemiring R] {σ : Type u_1} {ι : Type u_2} {S : Type u_3} [CommSemiring S] [Algebra R S] (r : R) : (tensorEquivSum R σ ι S) (1 ⊗ₜ[R] C r) = C ((algebraMap R S) r)

@[simp]

theorem MvPolynomial.tensorEquivSum_C_tmul_C {R : Type u} [CommSemiring R] {σ : Type u_1} {ι : Type u_2} {S : Type u_3} [CommSemiring S] [Algebra R S] (r : R) (s : S) : (tensorEquivSum R σ ι S) (C s ⊗ₜ[R] C r) = C (r • s)

@[simp]

theorem MvPolynomial.tensorEquivSum_X_tmul_X {R : Type u} [CommSemiring R] {σ : Type u_1} {ι : Type u_2} {S : Type u_3} [CommSemiring S] [Algebra R S] (i : σ) (j : ι) : (tensorEquivSum R σ ι S) (X i ⊗ₜ[R] X j) = X (Sum.inl i) * X (Sum.inr j)

instance MvPolynomial.instIsPushout {R : Type u} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] : Algebra.IsPushout R S (MvPolynomial σ R) (MvPolynomial σ S)

instance MvPolynomial.instIsPushout_1 {R : Type u} [CommSemiring R] {σ : Type u_1} {S : Type u_3} [CommSemiring S] [Algebra R S] : Algebra.IsPushout R (MvPolynomial σ R) S (MvPolynomial σ S)