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.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] : TensorProduct R S (MvPolynomial σ 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

Equations

• MvPolynomial.rTensorAlgEquiv = AddMonoidAlgebra.rTensorEquivAlgEquiv R S S N

@[deprecated MvPolynomial.rTensorAlgEquiv (since := "2026-06-18")]

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 S (MvPolynomial σ N) ≃ₐ[S] MvPolynomial σ (TensorProduct R S N)

Alias of MvPolynomial.rTensorAlgEquiv.

---

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

Equations

• @MvPolynomial.rTensorAlgHom = @MvPolynomial.rTensorAlgEquiv

@[simp]

theorem MvPolynomial.coeff_rTensorAlgEquiv_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] (s : S) (p : MvPolynomial σ N) (d : σ →₀ ℕ) : coeff d (rTensorAlgEquiv (s ⊗ₜ[R] p)) = s ⊗ₜ[R] coeff d p

theorem MvPolynomial.coeff_rTensorAlgEquiv_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 (rTensorAlgEquiv (s ⊗ₜ[R] (monomial e) n)) = if e = d then s ⊗ₜ[R] n else 0

@[deprecated "Now a syntactic tautology" (since := "2026-06-18")]

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] (x : TensorProduct R N (MvPolynomial σ S)) : rTensorAlgEquiv x = rTensorAlgHom x

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

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

Equations

• MvPolynomial.scalarRTensorAlgEquiv = AddMonoidAlgebra.scalarTensorEquiv R N

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.

Equations

• MvPolynomial.algebraTensorAlgEquiv R A = AddMonoidAlgebra.scalarTensorEquiv R 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] : (AlgHom.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

noncomputable 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]

Equations

• One or more equations did not get rendered due to their size.

@[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)