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.

Equations

• PolyEquivTensor.toFunBilinear R A = LinearMap.toSpanSingleton A (Polynomial R →ₗ[R] Polynomial A) (Polynomial.aeval Polynomial.X).toLinearMap

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.

Equations

• PolyEquivTensor.toFunLinear R A = TensorProduct.lift (↑R (PolyEquivTensor.toFunBilinear R A))

@[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].

Equations

• PolyEquivTensor.toFunAlgHom R A = Algebra.TensorProduct.algHomOfLinearMapTensorProduct (PolyEquivTensor.toFunLinear R A) ⋯ ⋯

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

Equations

• PolyEquivTensor.invFun R A p = Polynomial.eval₂ (↑Algebra.TensorProduct.includeLeft) (1 ⊗ₜ[R] Polynomial.X) p

@[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].

Equations

• PolyEquivTensor.equiv R A = { toFun := ⇑(PolyEquivTensor.toFunAlgHom R A), invFun := PolyEquivTensor.invFun R A, left_inv := ⋯, right_inv := ⋯ }

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]).

Equations

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

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

Equations

• polyEquivTensor' R A = { toEquiv := (polyEquivTensor R A).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

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

Equations

• Polynomial.algebra R A = (Polynomial.mapRingHom (algebraMap R A)).toAlgebra' ⋯

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