Base change of polynomial algebras

Given [CommSemiring R] [Semiring A] [Algebra R A] we show A[X] ≃ₐ[R] (A ⊗[R] R[X]).

def PolyEquivTensor.toFunBilinear (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : A →ₗ[A] Polynomial R →ₗ[R] Polynomial A

(Implementation detail). The function underlying A ⊗[R] R[X] →ₐ[R] A[X], as a bilinear function of two arguments.

theorem PolyEquivTensor.toFunBilinear_apply_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : ((toFunBilinear R A) a) p = a • (Polynomial.aeval Polynomial.X) p

@[simp]

theorem PolyEquivTensor.toFunBilinear_apply_eq_smul (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : ((toFunBilinear R A) a) p = a • Polynomial.map (algebraMap R A) p

theorem PolyEquivTensor.toFunBilinear_apply_eq_sum (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : ((toFunBilinear R A) a) p = p.sum fun (n : ℕ) (r : R) => (Polynomial.monomial n) (a * (algebraMap R A) r)

def PolyEquivTensor.toFunLinear (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : TensorProduct R A (Polynomial R) →ₗ[R] Polynomial A

(Implementation detail). The function underlying A ⊗[R] R[X] →ₐ[R] A[X], as a linear map.

@[simp]

theorem PolyEquivTensor.toFunLinear_tmul_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : (toFunLinear R A) (a ⊗ₜ[R] p) = ((toFunBilinear R A) a) p

theorem PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_1 (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial R) (k : ℕ) (h : Decidable ¬p.coeff k = 0) (a : A) : (if ¬p.coeff k = 0 then a * (algebraMap R A) (p.coeff k) else 0) = a * (algebraMap R A) (p.coeff k)

theorem PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_2 (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (k : ℕ) (a₁ a₂ : A) (p₁ p₂ : Polynomial R) : a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) = ∑ x ∈ Finset.antidiagonal k, a₁ * (algebraMap R A) (p₁.coeff x.1) * (a₂ * (algebraMap R A) (p₂.coeff x.2))

theorem PolyEquivTensor.toFunLinear_mul_tmul_mul (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a₁ a₂ : A) (p₁ p₂ : Polynomial R) : (toFunLinear R A) ((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) = (toFunLinear R A) (a₁ ⊗ₜ[R] p₁) * (toFunLinear R A) (a₂ ⊗ₜ[R] p₂)

theorem PolyEquivTensor.toFunLinear_one_tmul_one (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : (toFunLinear R A) (1 ⊗ₜ[R] 1) = 1

def PolyEquivTensor.toFunAlgHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : TensorProduct R A (Polynomial R) →ₐ[R] Polynomial A

(Implementation detail). The algebra homomorphism A ⊗[R] R[X] →ₐ[R] A[X].

@[simp]

theorem PolyEquivTensor.toFunAlgHom_apply_tmul_eq_smul (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : (toFunAlgHom R A) (a ⊗ₜ[R] p) = a • Polynomial.map (algebraMap R A) p

theorem PolyEquivTensor.toFunAlgHom_apply_tmul (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : (toFunAlgHom R A) (a ⊗ₜ[R] p) = p.sum fun (n : ℕ) (r : R) => (Polynomial.monomial n) (a * (algebraMap R A) r)

def PolyEquivTensor.invFun (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial A) : TensorProduct R A (Polynomial R)

(Implementation detail.)

The bare function A[X] → A ⊗[R] R[X]. (We don't need to show that it's an algebra map, thankfully --- just that it's an inverse.)

@[simp]

theorem PolyEquivTensor.invFun_add (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] {p q : Polynomial A} : invFun R A (p + q) = invFun R A p + invFun R A q

theorem PolyEquivTensor.invFun_monomial (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (n : ℕ) (a : A) : invFun R A ((Polynomial.monomial n) a) = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] Polynomial.X ^ n

theorem PolyEquivTensor.left_inv (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (x : TensorProduct R A (Polynomial R)) : invFun R A ((toFunAlgHom R A) x) = x

theorem PolyEquivTensor.right_inv (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (x : Polynomial A) : (toFunAlgHom R A) (invFun R A x) = x

def PolyEquivTensor.equiv (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : TensorProduct R A (Polynomial R) ≃ Polynomial A

(Implementation detail)

The equivalence, ignoring the algebra structure, (A ⊗[R] R[X]) ≃ A[X].

def polyEquivTensor (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : Polynomial A ≃ₐ[R] TensorProduct R A (Polynomial R)

The R-algebra isomorphism A[X] ≃ₐ[R] (A ⊗[R] R[X]).

@[simp]

theorem polyEquivTensor_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial A) : (polyEquivTensor R A) p = Polynomial.eval₂ (↑Algebra.TensorProduct.includeLeft) (1 ⊗ₜ[R] Polynomial.X) p

@[simp]

theorem polyEquivTensor_symm_apply_tmul_eq_smul (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : (polyEquivTensor R A).symm (a ⊗ₜ[R] p) = a • Polynomial.map (algebraMap R A) p

theorem polyEquivTensor_symm_apply_tmul (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : (polyEquivTensor R A).symm (a ⊗ₜ[R] p) = p.sum fun (n : ℕ) (r : R) => (Polynomial.monomial n) (a * (algebraMap R A) r)

def polyEquivTensor' (R : Type u_1) [CommSemiring R] (A : Type u_3) [CommSemiring A] [Algebra R A] : Polynomial A ≃ₐ[A] TensorProduct R A (Polynomial R)

The A-algebra isomorphism A[X] ≃ₐ[A] A ⊗[R] R[X] (when A is commutative).

@[simp]

theorem coe_polyEquivTensor' (R : Type u_1) [CommSemiring R] (A : Type u_3) [CommSemiring A] [Algebra R A] : ⇑(polyEquivTensor' R A) = ⇑(polyEquivTensor R A)

polyEquivTensor' R A is the same as polyEquivTensor R A as a function.

@[simp]

theorem coe_polyEquivTensor'_symm (R : Type u_1) [CommSemiring R] (A : Type u_3) [CommSemiring A] [Algebra R A] : ⇑(polyEquivTensor' R A).symm = ⇑(polyEquivTensor R A).symm

@[reducible]

def Polynomial.algebra (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : Algebra (Polynomial R) (Polynomial A)

If A is an R-algebra, then A[X] is an R[X] algebra. This gives a diamond for Algebra R[X] R[X][X], so this is not a global instance.

@[simp]

theorem Polynomial.algebraMap_def (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : algebraMap (Polynomial R) (Polynomial A) = mapRingHom (algebraMap R A)

instance instIsScalarTowerPolynomial (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : IsScalarTower R (Polynomial R) (Polynomial A)

instance instFaithfulSMulPolynomial (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] : FaithfulSMul (Polynomial R) (Polynomial A)

instance instIsPushoutPolynomial (R : Type u_1) [CommSemiring R] {S : Type u_3} [CommSemiring S] [Algebra R S] : Algebra.IsPushout R S (Polynomial R) (Polynomial S)

instance instIsPushoutPolynomial_1 (R : Type u_1) [CommSemiring R] {S : Type u_3} [CommSemiring S] [Algebra R S] : Algebra.IsPushout R (Polynomial R) S (Polynomial S)