Coefficientwise application of a linear map to multivariate polynomials, and linear coefficient descent of a polynomial over a field extension: a nonzero polynomial vanishing at base-field points has a nonzero base-field polynomial of no larger degree vanishing at every one of those points.

noncomputable def CCDN.polynomialCoefficientLinear {R : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (φ : A →ₗ[R] B) : MvPolynomial σ A →ₗ[R] MvPolynomial σ B

Apply a linear coefficient map without changing any monomial.

Equations

• CCDN.polynomialCoefficientLinear φ = ↑(AddMonoidAlgebra.coeffLinearEquiv R).symm ∘ₗ Finsupp.mapRange.linearMap φ ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv R)

@[simp]

theorem CCDN.polynomialCoefficientLinear_coeff {R : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (φ : A →ₗ[R] B) (f : MvPolynomial σ A) (e : σ →₀ ℕ) : ((polynomialCoefficientLinear φ) f).coeff e = φ (f.coeff e)

Each coefficient of polynomialCoefficientLinear φ f is the image under φ of the corresponding coefficient of f.

@[simp]

theorem CCDN.polynomialCoefficientLinear_C {R : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (φ : A →ₗ[R] B) (a : A) : (polynomialCoefficientLinear φ) (MvPolynomial.C a) = MvPolynomial.C (φ a)

Applying the linear map φ coefficientwise sends the constant C a to C (φ a).

theorem CCDN.polynomialCoefficientLinear_mul_compatible {R : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (φ : A →ₗ[R] B) (θ : B →+* A) (hφ : ∀ (a : A) (b : B), φ (a * θ b) = φ a * b) (f : MvPolynomial σ A) (g : MvPolynomial σ B) : (polynomialCoefficientLinear φ) (f * (MvPolynomial.map θ) g) = (polynomialCoefficientLinear φ) f * g

If φ (a * θ b) = φ a * b for a ring map θ : B →+* A, then applying φ coefficientwise is linear over polynomials with coefficients in B: it sends f * map θ g to polynomialCoefficientLinear φ f * g.

theorem CCDN.polynomialCoefficientLinear_mul_map {K : Type u_1} {L : Type u_2} {σ : Type u_3} [Field K] [Field L] [Algebra K L] (φ : L →ₗ[K] K) (f : MvPolynomial σ L) (g : MvPolynomial σ K) : (polynomialCoefficientLinear φ) (f * (MvPolynomial.map (algebraMap K L)) g) = (polynomialCoefficientLinear φ) f * g

For a field extension L / K and a K-linear functional φ : L → K, applying φ coefficientwise is linear over polynomials with coefficients in K: it sends f * map (algebraMap K L) g to polynomialCoefficientLinear φ f * g.

theorem CCDN.polynomialCoefficientLinear_mem_scalar_extension {K : Type u_1} {L : Type u_2} {σ : Type u_3} [Field K] [Field L] [Algebra K L] (I : Ideal (MvPolynomial σ K)) (g : MvPolynomial σ L) (hg : g ∈ Ideal.map (MvPolynomial.map (algebraMap K L)) I) (φ : L →ₗ[K] K) : (polynomialCoefficientLinear φ) g ∈ I

Coefficient functionals send elements of an extended ideal into the original ideal, for any variable type.

theorem CCDN.polynomialCoefficientLinear_totalDegree_le {R : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (φ : A →ₗ[R] B) (f : MvPolynomial σ A) : ((polynomialCoefficientLinear φ) f).totalDegree ≤ f.totalDegree

Applying a linear map coefficientwise does not increase the total degree.

theorem CCDN.polynomialCoefficientLinear_eval {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] (φ : K →ₗ[k] k) (f : MvPolynomial σ K) (x : σ → k) : (MvPolynomial.eval x) ((polynomialCoefficientLinear φ) f) = φ ((MvPolynomial.eval (⇑(algebraMap k K) ∘ x)) f)

For a field extension K / k and a k-linear functional φ : K → k, evaluating the coefficientwise image of f under φ at a k-point x gives φ of the value of f at x.

theorem CCDN.exists_nonzero_polynomial_linear_descent {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {n : ℕ} (f : MvPolynomial (Fin n) K) (hf : f ≠ 0) : ∃ (g : MvPolynomial (Fin n) k), g ≠ 0 ∧ g.totalDegree ≤ f.totalDegree ∧ ∀ (x : Fin n → k), (MvPolynomial.eval (⇑(algebraMap k K) ∘ x)) f = 0 → (MvPolynomial.eval x) g = 0

Linear coefficient descent: for a field extension K / k, a nonzero polynomial f over K has a nonzero polynomial over k of total degree at most that of f vanishing at every k-point where f vanishes.