Polynomial rigidity on simple finite fibers

The generic-fiber step in Rueckert's analytic Nullstellensatz reduces to a pointwise polynomial fact. A polynomial of degree strictly below d which vanishes at every root of a separable monic polynomial of degree d is zero. This file packages that fact for the coefficient-vector convention used by Weierstrass division.

noncomputable def LocalComplexGeometry.remainderPolynomialAt {n d : ℕ} (b : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) : Polynomial ℂ

A degree-< d coefficient vector, evaluated as a polynomial in the last variable at a fixed base point.

Equations

• LocalComplexGeometry.remainderPolynomialAt b z = ∑ i : Fin d, Polynomial.C (b i z) * Polynomial.X ^ ↑i

@[simp]

theorem LocalComplexGeometry.remainderPolynomialAt_eval {n d : ℕ} (b : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) (w : ℂ) : Polynomial.eval w (remainderPolynomialAt b z) = ∑ i : Fin d, b i z * w ^ ↑i

Pointwise evaluation of remainderPolynomialAt.

theorem LocalComplexGeometry.remainderPolynomialAt_natDegree_lt {n d : ℕ} (hd : 0 < d) (b : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) : (remainderPolynomialAt b z).natDegree < d

The assembled remainder polynomial has degree strictly below d.

theorem LocalComplexGeometry.remainderPolynomialAt_coeff_eq_zero {n d : ℕ} (b : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) (hzero : remainderPolynomialAt b z = 0) (i : Fin d) : b i z = 0

A zero assembled remainder polynomial has every displayed coefficient equal to zero.

theorem LocalComplexGeometry.polynomial_eq_zero_of_natDegree_lt_of_vanishes_on_separableRoots {q r : Polynomial ℂ} (hq : q ≠ 0) (hsep : q.Separable) (hdegree : r.natDegree < q.natDegree) (hvanish : ∀ (w : ℂ), Polynomial.eval w q = 0 → Polynomial.eval w r = 0) : r = 0

A polynomial of degree below a nonzero separable complex polynomial which vanishes at every root of that polynomial is zero.

theorem LocalComplexGeometry.remainderPolynomialAt_eq_zero_of_vanishes_on_preparedRoots {n d : ℕ} (hd : 0 < d) (a b : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) (hsep : (preparedPolynomialAt a z).Separable) (hvanish : ∀ (w : ℂ), preparedValue a z w = 0 → ∑ i : Fin d, b i z * w ^ ↑i = 0) : remainderPolynomialAt b z = 0

Fiber rigidity: vanishing at every root of a separable prepared polynomial forces a lower-degree remainder polynomial to be zero.

theorem LocalComplexGeometry.coefficient_eq_zero_of_vanishes_on_preparedRoots {n d : ℕ} (hd : 0 < d) (a b : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) (hsep : (preparedPolynomialAt a z).Separable) (hvanish : ∀ (w : ℂ), preparedValue a z w = 0 → ∑ i : Fin d, b i z * w ^ ↑i = 0) (i : Fin d) : b i z = 0

Coefficient form of fiber rigidity.