A nonvanishing resultant for the cleared generic minimal polynomial

The denominator-cleared minimal polynomial is generally not monic over the base germ ring. Its leading coefficient and its fixed-size derivative resultant nevertheless stay outside the contracted prime. Consequently, away from one analytic exceptional factor, its complex specializations keep their generic degree and have only simple roots.

noncomputable def LocalComplexGeometry.polynomialCoefficientRepresentatives {n : ℕ} (Q : Polynomial ↥(HolomorphicGerm n)) : Fin (Q.natDegree + 1) → ComplexEuclidean n → ℂ

The chosen representative family of all coefficients of a polynomial up to its exact natural degree.

Equations

• LocalComplexGeometry.polynomialCoefficientRepresentatives Q i = LocalComplexGeometry.HolomorphicGerm.representative (Q.coeff ↑i)

theorem LocalComplexGeometry.analyticAt_polynomialCoefficientRepresentatives {n : ℕ} (Q : Polynomial ↥(HolomorphicGerm n)) (i : Fin (Q.natDegree + 1)) : AnalyticAt ℂ (polynomialCoefficientRepresentatives Q i) 0

theorem LocalComplexGeometry.fixedDegreePolynomial_coeff_polynomial {n : ℕ} (Q : Polynomial ↥(HolomorphicGerm n)) : (fixedDegreePolynomial fun (i : Fin (Q.natDegree + 1)) => Q.coeff ↑i) = Q

Reassembling the coefficient germs used by polynomialCoefficientRepresentatives recovers the original polynomial.

theorem LocalComplexGeometry.eventually_genericMinpolyLift_resultant_representative {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : have c := genericMinpolyLiftCertificate P a ha ha0 hmem; have e := c.polynomial.natDegree; have Δ := c.polynomial.resultant (Polynomial.derivative c.polynomial) e (e - 1); ∀ᶠ (z : ComplexEuclidean n) in nhds 0, HolomorphicGerm.representative Δ z = (fixedDegreePolynomialAt (polynomialCoefficientRepresentatives c.polynomial) z).resultant (Polynomial.derivative (fixedDegreePolynomialAt (polynomialCoefficientRepresentatives c.polynomial) z)) e (e - 1)

The chosen analytic representative of the algebraic derivative resultant agrees near the origin with the pointwise fixed-size resultant of the chosen coefficient representatives.

theorem LocalComplexGeometry.eventually_genericMinpolyLift_resultant_germPolynomialRepresentativeAt {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : have c := genericMinpolyLiftCertificate P a ha ha0 hmem; have e := c.polynomial.natDegree; have Δ := c.polynomial.resultant (Polynomial.derivative c.polynomial) e (e - 1); ∀ᶠ (z : ComplexEuclidean n) in nhds 0, HolomorphicGerm.representative Δ z = (germPolynomialRepresentativeAt e c.polynomial z).resultant (Polynomial.derivative (germPolynomialRepresentativeAt e c.polynomial z)) e (e - 1)

The resultant representative theorem in the common germPolynomialRepresentativeAt notation used by quotient specialization.

theorem LocalComplexGeometry.eventually_genericMinpolyLift_natDegree_eq_and_separable {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : have c := genericMinpolyLiftCertificate P a ha ha0 hmem; have e := c.polynomial.natDegree; have Δ := c.polynomial.resultant (Polynomial.derivative c.polynomial) e (e - 1); ∀ᶠ (z : ComplexEuclidean n) in nhds 0, HolomorphicGerm.representative c.polynomial.leadingCoeff z ≠ 0 → HolomorphicGerm.representative Δ z ≠ 0 → (germPolynomialRepresentativeAt e c.polynomial z).natDegree = e ∧ (germPolynomialRepresentativeAt e c.polynomial z).Separable

Off the leading-coefficient and derivative-resultant exceptional loci, the lifted minimal-polynomial specialization keeps its exact positive degree and is separable.