Specializing denominator-cleared generic divisibility

A GenericMinpolyDivisibilityLiftCertificate is a polynomial identity over base germs up to a coefficientwise contraction error. On the contracted prime's local zero set that error disappears. Away from the explicit denominator, every root of the lifted minimal polynomial is therefore a root of the certified divisible polynomial.

noncomputable def LocalComplexGeometry.remainderGermPolynomialRepresentativeFunctions {n e : ℕ} (b : Fin e → ↥(HolomorphicGerm n)) : Polynomial (ComplexEuclidean n → ℂ)

The polynomial of chosen coefficient representatives attached to a WPT remainder vector, before specialization at a base point.

Equations

• LocalComplexGeometry.remainderGermPolynomialRepresentativeFunctions b = ∑ i : Fin e, Polynomial.C (LocalComplexGeometry.HolomorphicGerm.representative (b i)) * Polynomial.X ^ ↑i

@[simp]

theorem LocalComplexGeometry.remainderGermPolynomialRepresentativeFunctions_map_eval {n e : ℕ} (b : Fin e → ↥(HolomorphicGerm n)) (z : ComplexEuclidean n) : Polynomial.map (Pi.evalRingHom (fun (x : ComplexEuclidean n) => ℂ) z) (remainderGermPolynomialRepresentativeFunctions b) = remainderPolynomialAt (HolomorphicGerm.coefficientRepresentatives b) z

theorem LocalComplexGeometry.remainderGermPolynomialRepresentativeFunctions_map_germ {n e : ℕ} (b : Fin e → ↥(HolomorphicGerm n)) : Polynomial.map (functionToGermRingHom n) (remainderGermPolynomialRepresentativeFunctions b) = Polynomial.map (holomorphicGermSubring n).subtype (remainderGermPolynomial b)

Mapping the representative-function polynomial to raw function germs recovers the polynomial assembled from the original coefficient germs.

theorem LocalComplexGeometry.eventually_germPolynomialRepresentativeAt_eq_remainderPolynomialAt {n e m : ℕ} (b : Fin e → ↥(HolomorphicGerm n)) (hB : (remainderGermPolynomial b).natDegree ≤ m) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, germPolynomialRepresentativeAt m (remainderGermPolynomial b) z = remainderPolynomialAt (HolomorphicGerm.coefficientRepresentatives b) z

Any sufficiently large fixed-degree display of a WPT remainder agrees near the origin with its direct coefficient-vector specialization.

theorem LocalComplexGeometry.eventually_eval_eq_zero_of_genericMinpolyDivisibilityLiftCertificate {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) {Q R : Polynomial ↥(HolomorphicGerm n)} (C : GenericMinpolyDivisibilityLiftCertificate P Q R) {e k : ℕ} (hQ : Q.natDegree ≤ e) (hR : R.natDegree ≤ k) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, idealGeneratorZeroPredicate (lowerDimensionalContraction P) z → HolomorphicGerm.representative C.denominator z ≠ 0 → ∀ (w : ℂ), Polynomial.eval w (germPolynomialRepresentativeAt e Q z) = 0 → Polynomial.eval w (germPolynomialRepresentativeAt k R z) = 0

A denominator-cleared generic divisibility certificate specializes to the expected root implication on the contracted analytic zero set.

theorem LocalComplexGeometry.eventually_remainder_eval_eq_denominator_mul_of_genericRemainderModMinpolyLiftCertificate {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {Q R : Polynomial ↥(HolomorphicGerm n)} (C : GenericRemainderModMinpolyLiftCertificate P Q R) {e k : ℕ} (hQ : Q.natDegree ≤ e) (hR : R.natDegree ≤ k) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, idealGeneratorZeroPredicate (lowerDimensionalContraction P) z → ∀ (w : ℂ), Polynomial.eval w (germPolynomialRepresentativeAt e Q z) = 0 → Polynomial.eval w (remainderPolynomialAt (HolomorphicGerm.coefficientRepresentatives C.coefficients) z) = HolomorphicGerm.representative C.denominator z * Polynomial.eval w (germPolynomialRepresentativeAt k R z)

The strict Euclidean remainder in an arbitrary-target certificate specializes, at every root of the lifted minimal polynomial, to the explicit denominator times the certified target polynomial.