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_2} [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

Equations

• MvPolynomial.rTensor = TensorProduct.finsuppLeft' R S N (σ →₀ ℕ) S

theorem MvPolynomial.rTensor_apply_tmul {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_2} [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) => Finsupp.single i (m ⊗ₜ[R] n)

theorem MvPolynomial.rTensor_apply_tmul_apply {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_2} [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_2} [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_2} [CommSemiring S] [Algebra R S] [DecidableEq σ] [AddCommMonoid N] [Module R N] (s : σ) (n : N) (d : σ →₀ ℕ) : (rTensor (X s ⊗ₜ[R] n)) d = if Finsupp.single 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_2} [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_2} [CommSemiring S] [Algebra R S] [DecidableEq σ] [AddCommMonoid N] [Module R N] (d : σ →₀ ℕ) (s : S) (n : N) : rTensor.symm (Finsupp.single 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

Equations

• MvPolynomial.scalarRTensor = TensorProduct.finsuppScalarLeft R N (σ →₀ ℕ)

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) => Finsupp.single 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 Finsupp.single 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 (Finsupp.single 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_2} [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

Equations

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

@[simp]

theorem MvPolynomial.coeff_rTensorAlgHom_tmul {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_2} [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_2} [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_2} [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_2} [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_2} [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

Equations

• MvPolynomial.rTensorAlgEquiv = AlgEquiv.ofLinearEquiv MvPolynomial.rTensor ⋯ ⋯

@[simp]

theorem MvPolynomial.rTensorAlgEquiv_apply {R : Type u} {N : Type v} [CommSemiring R] {σ : Type u_1} {S : Type u_2} [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

Equations

• MvPolynomial.scalarRTensorAlgEquiv = MvPolynomial.rTensorAlgEquiv.trans (MvPolynomial.mapAlgEquiv σ (Algebra.TensorProduct.lid R N))

noncomputable def MvPolynomial.algebraTensorAlgEquiv (R : Type u) [CommSemiring R] {σ : Type u_1} (A : Type u_3) [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

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

@[simp]

theorem MvPolynomial.algebraTensorAlgEquiv_tmul (R : Type u) [CommSemiring R] {σ : Type u_1} (A : Type u_3) [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_3) [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_3) [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_3) [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_3) [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_2} [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

instance MvPolynomial.instIsPushout (R : Type u) [CommSemiring R] {σ : Type u_1} {S : Type u_2} [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_2} [CommSemiring S] [Algebra R S] : Algebra.IsPushout R (MvPolynomial σ R) S (MvPolynomial σ S)