Commit 2024-06-05 00:51 ab26390e

feat(Mathlib.RingTheory.TensorProduct.MvPolynomial) : tensor product of a (multivariate) polynomial ring (#12293) 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