Specializing fixed-degree resultants

This file packages the algebraic specialization argument for resultants of polynomial families with analytic coefficients. The fixed Sylvester sizes are part of every definition, so specialization remains valid even when a fiber drops degree.

Fixed-degree polynomial families

noncomputable def LocalComplexGeometry.fixedDegreePolynomial {R : Type u_1} [Semiring R] {d : ℕ} (c : Fin (d + 1) → R) : Polynomial R

Assemble coefficients indexed by Fin (d + 1) into a polynomial of degree at most d.

Equations

• LocalComplexGeometry.fixedDegreePolynomial c = ∑ i : Fin (d + 1), Polynomial.C (c i) * Polynomial.X ^ ↑i

noncomputable def LocalComplexGeometry.fixedDegreePolynomialAt {R : Type u_1} {X : Type u_2} [Semiring R] {d : ℕ} (c : Fin (d + 1) → X → R) (x : X) : Polynomial R

Specialize a fixed-degree polynomial family at a parameter.

Equations

• LocalComplexGeometry.fixedDegreePolynomialAt c x = LocalComplexGeometry.fixedDegreePolynomial fun (i : Fin (d + 1)) => c i x

@[simp]

theorem LocalComplexGeometry.fixedDegreePolynomial_map {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {d : ℕ} (φ : R →+* S) (c : Fin (d + 1) → R) : Polynomial.map φ (fixedDegreePolynomial c) = fixedDegreePolynomial fun (i : Fin (d + 1)) => φ (c i)

@[simp]

theorem LocalComplexGeometry.fixedDegreePolynomialAt_eval {R : Type u_1} {X : Type u_2} [CommSemiring R] {d : ℕ} (c : Fin (d + 1) → X → R) (x : X) (w : R) : Polynomial.eval w (fixedDegreePolynomialAt c x) = ∑ i : Fin (d + 1), c i x * w ^ ↑i

theorem LocalComplexGeometry.fixedDegreePolynomial_natDegree_le {R : Type u_1} [Semiring R] {d : ℕ} (c : Fin (d + 1) → R) : (fixedDegreePolynomial c).natDegree ≤ d

The displayed polynomial has degree at most its fixed degree bound.

@[simp]

theorem LocalComplexGeometry.fixedDegreePolynomial_coeff {R : Type u_1} [Semiring R] {d k : ℕ} (c : Fin (d + 1) → R) : (fixedDegreePolynomial c).coeff k = if h : k < d + 1 then c ⟨k, h⟩ else 0

Every coefficient of the assembled polynomial is the corresponding displayed coefficient inside the fixed range and is zero outside it.

theorem LocalComplexGeometry.fixedDegreePolynomial_coeff_top {R : Type u_1} [Semiring R] {d : ℕ} (c : Fin (d + 1) → R) : (fixedDegreePolynomial c).coeff d = c ⟨d, ⋯⟩

The coefficient at the fixed top degree is the displayed top coefficient.

theorem LocalComplexGeometry.fixedDegreePolynomial_coefficients_eq {R : Type u_1} [Semiring R] {d : ℕ} (p : Polynomial R) (hp : p.natDegree ≤ d) : (fixedDegreePolynomial fun (i : Fin (d + 1)) => p.coeff ↑i) = p

Reassembling all coefficients up to a valid fixed bound recovers the polynomial.

theorem LocalComplexGeometry.fixedDegreePolynomial_natDegree_eq {R : Type u_1} [Semiring R] {d : ℕ} (c : Fin (d + 1) → R) (htop : c ⟨d, ⋯⟩ ≠ 0) : (fixedDegreePolynomial c).natDegree = d

A nonzero displayed top coefficient forces the exact fixed degree.

theorem LocalComplexGeometry.fixedDegreePolynomial_monic {R : Type u_1} [Semiring R] [Nontrivial R] {d : ℕ} (c : Fin (d + 1) → R) (htop : c ⟨d, ⋯⟩ = 1) : (fixedDegreePolynomial c).Monic

A fixed-degree polynomial whose displayed top coefficient is one is monic.

theorem LocalComplexGeometry.fixedDegreePolynomialAt_natDegree_le {R : Type u_1} {X : Type u_2} [Semiring R] {d : ℕ} (c : Fin (d + 1) → X → R) (x : X) : (fixedDegreePolynomialAt c x).natDegree ≤ d

theorem LocalComplexGeometry.fixedDegreePolynomialAt_natDegree_eq {R : Type u_1} {X : Type u_2} [Semiring R] {d : ℕ} (c : Fin (d + 1) → X → R) (x : X) (htop : c ⟨d, ⋯⟩ x ≠ 0) : (fixedDegreePolynomialAt c x).natDegree = d

theorem LocalComplexGeometry.fixedDegreePolynomialAt_monic {R : Type u_1} {X : Type u_2} [Semiring R] [Nontrivial R] {d : ℕ} (c : Fin (d + 1) → X → R) (x : X) (htop : c ⟨d, ⋯⟩ x = 1) : (fixedDegreePolynomialAt c x).Monic

theorem LocalComplexGeometry.fixedDegreePolynomial_map_eval {R : Type u_1} {X : Type u_2} [CommSemiring R] {d : ℕ} (c : Fin (d + 1) → X → R) (x : X) : Polynomial.map (Pi.evalRingHom (fun (x : X) => R) x) (fixedDegreePolynomial c) = fixedDegreePolynomialAt c x

Specializing the coefficient-function polynomial agrees with assembling the specialized coefficients.

Algebraic specialization of resultants

noncomputable def LocalComplexGeometry.fixedDegreeResultantAt {R : Type u_1} {X : Type u_2} [CommRing R] {d e : ℕ} (a : Fin (d + 1) → X → R) (b : Fin (e + 1) → X → R) (x : X) : R

The pointwise fixed-size resultant of two coefficient families.

Equations

• LocalComplexGeometry.fixedDegreeResultantAt a b x = (LocalComplexGeometry.fixedDegreePolynomialAt a x).resultant (LocalComplexGeometry.fixedDegreePolynomialAt b x) d e

theorem LocalComplexGeometry.fixedDegreeResultant_function_apply {R : Type u_1} {X : Type u_2} [CommRing R] {d e : ℕ} (a : Fin (d + 1) → X → R) (b : Fin (e + 1) → X → R) (x : X) : (fixedDegreePolynomial a).resultant (fixedDegreePolynomial b) d e x = fixedDegreeResultantAt a b x

A fixed-size resultant over a function ring specializes pointwise.

theorem LocalComplexGeometry.exists_analytic_fixedDegreeResultantAt_origin {n d e : ℕ} (a : Fin (d + 1) → ComplexEuclidean n → ℂ) (b : Fin (e + 1) → ComplexEuclidean n → ℂ) (ha : ∀ (i : Fin (d + 1)), AnalyticAt ℂ (a i) 0) (hb : ∀ (i : Fin (e + 1)), AnalyticAt ℂ (b i) 0) : ∃ (Δ : ComplexEuclidean n → ℂ), AnalyticAt ℂ Δ 0 ∧ ∀ᶠ (z : ComplexEuclidean n) in nhds 0, Δ z = fixedDegreeResultantAt a b z

Two finite analytic coefficient families have an analytic representative of their fixed-size resultant. Its equality with the pointwise complex resultant is a germ equality, hence holds on a neighborhood of the origin.

theorem LocalComplexGeometry.exists_analytic_fixedDegreeResultantAt {n d e : ℕ} {z₀ : ComplexEuclidean n} (a : Fin (d + 1) → ComplexEuclidean n → ℂ) (b : Fin (e + 1) → ComplexEuclidean n → ℂ) (ha : ∀ (i : Fin (d + 1)), AnalyticAt ℂ (a i) z₀) (hb : ∀ (i : Fin (e + 1)), AnalyticAt ℂ (b i) z₀) : ∃ (Δ : ComplexEuclidean n → ℂ), AnalyticAt ℂ Δ z₀ ∧ ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, Δ z = fixedDegreeResultantAt a b z

Arbitrary-base-point form of analytic resultant specialization.

Nonvanishing derivative resultants and simple fibers

theorem LocalComplexGeometry.separable_of_resultant_derivative_ne_zero {d : ℕ} (_hd : 0 < d) {p : Polynomial ℂ} (hdegree : p.natDegree = d) (hres : p.resultant (Polynomial.derivative p) d (d - 1) ≠ 0) : p.Separable

A complex polynomial of known positive degree is separable when its fixed-size resultant with its derivative is nonzero. No monicity assumption is needed.

theorem LocalComplexGeometry.fixedDegreePolynomialAt_separable_of_top_ne_zero_of_resultant_derivative_ne_zero {X : Type u_1} {d : ℕ} (hd : 0 < d) (a : Fin (d + 1) → X → ℂ) (x : X) (htop : a ⟨d, ⋯⟩ x ≠ 0) (hres : (fixedDegreePolynomialAt a x).resultant (Polynomial.derivative (fixedDegreePolynomialAt a x)) d (d - 1) ≠ 0) : (fixedDegreePolynomialAt a x).Separable

Nonmonic coefficient-family criterion. A nonzero displayed top coefficient prevents degree drop, so the fixed-size resultant detects separability of the specialized fiber.

theorem LocalComplexGeometry.monic_separable_of_resultant_derivative_ne_zero {d : ℕ} (_hd : 0 < d) {p : Polynomial ℂ} (hmonic : p.Monic) (hdegree : p.natDegree = d) (hres : p.resultant (Polynomial.derivative p) d (d - 1) ≠ 0) : p.Separable

For a positive-degree monic complex polynomial, nonvanishing of the fixed-size resultant with its derivative implies separability.

theorem LocalComplexGeometry.fixedDegreePolynomialAt_separable_of_resultant_derivative_ne_zero {X : Type u_1} {d : ℕ} (hd : 0 < d) (a : Fin (d + 1) → X → ℂ) (x : X) (htop : a ⟨d, ⋯⟩ x = 1) (hres : (fixedDegreePolynomialAt a x).resultant (Polynomial.derivative (fixedDegreePolynomialAt a x)) d (d - 1) ≠ 0) : (fixedDegreePolynomialAt a x).Separable

Coefficient-family form of the preceding separability criterion.

theorem LocalComplexGeometry.eventually_separable_of_resultant_derivative_rep {n d : ℕ} {z₀ : ComplexEuclidean n} (hd : 0 < d) (a : Fin (d + 1) → ComplexEuclidean n → ℂ) (Δ : ComplexEuclidean n → ℂ) (htop : ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, a ⟨d, ⋯⟩ z = 1) (hΔ : ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, Δ z = (fixedDegreePolynomialAt a z).resultant (Polynomial.derivative (fixedDegreePolynomialAt a z)) d (d - 1)) : ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, Δ z ≠ 0 → (fixedDegreePolynomialAt a z).Separable

Eventual simple-fiber package: wherever an eventual representative of the derivative resultant is nonzero, the specialized fixed-degree fiber is separable. This is the form consumed by polynomial-fiber rigidity.

theorem LocalComplexGeometry.eventually_separable_of_top_ne_zero_of_resultant_derivative_rep {n d : ℕ} {z₀ : ComplexEuclidean n} (hd : 0 < d) (a : Fin (d + 1) → ComplexEuclidean n → ℂ) (Δ : ComplexEuclidean n → ℂ) (htop : ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, a ⟨d, ⋯⟩ z ≠ 0) (hΔ : ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, Δ z = (fixedDegreePolynomialAt a z).resultant (Polynomial.derivative (fixedDegreePolynomialAt a z)) d (d - 1)) : ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, Δ z ≠ 0 → (fixedDegreePolynomialAt a z).Separable

Eventual nonmonic simple-fiber criterion, retaining the useful pointwise implication from nonvanishing of the resultant representative.

theorem LocalComplexGeometry.eventually_separable_of_top_ne_zero_of_resultant_derivative_ne_zero {n d : ℕ} {z₀ : ComplexEuclidean n} (hd : 0 < d) (a : Fin (d + 1) → ComplexEuclidean n → ℂ) (Δ : ComplexEuclidean n → ℂ) (htop : ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, a ⟨d, ⋯⟩ z ≠ 0) (hΔ : ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, Δ z = (fixedDegreePolynomialAt a z).resultant (Polynomial.derivative (fixedDegreePolynomialAt a z)) d (d - 1)) (hΔne : ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, Δ z ≠ 0) : ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, (fixedDegreePolynomialAt a z).Separable

If both the displayed top coefficient and the derivative-resultant representative are eventually nonzero, all nearby specialized fibers are eventually separable.

Analytic derivative-resultant representatives

noncomputable def LocalComplexGeometry.fixedDegreeDerivativeFamily {X : Type u_1} {d : ℕ} (a : Fin (d + 1) → X → ℂ) : Fin (d - 1 + 1) → X → ℂ

The coefficient family (with fixed degree bound d - 1) of the derivative of a degree-d polynomial family.

Equations

• LocalComplexGeometry.fixedDegreeDerivativeFamily a i x = (Polynomial.derivative (LocalComplexGeometry.fixedDegreePolynomialAt a x)).coeff ↑i

theorem LocalComplexGeometry.analyticAt_fixedDegreeDerivativeFamily {n d : ℕ} {z₀ : ComplexEuclidean n} (hd : 0 < d) (a : Fin (d + 1) → ComplexEuclidean n → ℂ) (ha : ∀ (i : Fin (d + 1)), AnalyticAt ℂ (a i) z₀) (i : Fin (d - 1 + 1)) : AnalyticAt ℂ (fixedDegreeDerivativeFamily a i) z₀

Derivative coefficients of an analytic positive-degree family are analytic.

theorem LocalComplexGeometry.fixedDegreePolynomialAt_derivativeFamily {X : Type u_1} {d : ℕ} (_hd : 0 < d) (a : Fin (d + 1) → X → ℂ) (x : X) : fixedDegreePolynomialAt (fixedDegreeDerivativeFamily a) x = Polynomial.derivative (fixedDegreePolynomialAt a x)

Assembling the displayed derivative coefficients recovers the actual polynomial derivative.

theorem LocalComplexGeometry.exists_analytic_resultant_derivative {n d : ℕ} {z₀ : ComplexEuclidean n} (hd : 0 < d) (a : Fin (d + 1) → ComplexEuclidean n → ℂ) (ha : ∀ (i : Fin (d + 1)), AnalyticAt ℂ (a i) z₀) : ∃ (Δ : ComplexEuclidean n → ℂ), AnalyticAt ℂ Δ z₀ ∧ ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, Δ z = (fixedDegreePolynomialAt a z).resultant (Polynomial.derivative (fixedDegreePolynomialAt a z)) d (d - 1)

A positive-degree analytic coefficient family admits an analytic representative of its fixed-size resultant with its derivative.

theorem LocalComplexGeometry.exists_analytic_resultant_derivative_and_eventually_separable_of_top_ne_zero {n d : ℕ} {z₀ : ComplexEuclidean n} (hd : 0 < d) (a : Fin (d + 1) → ComplexEuclidean n → ℂ) (ha : ∀ (i : Fin (d + 1)), AnalyticAt ℂ (a i) z₀) (htop : ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, a ⟨d, ⋯⟩ z ≠ 0) : ∃ (Δ : ComplexEuclidean n → ℂ), AnalyticAt ℂ Δ z₀ ∧ (∀ᶠ (z : ComplexEuclidean n) in nhds z₀, Δ z = (fixedDegreePolynomialAt a z).resultant (Polynomial.derivative (fixedDegreePolynomialAt a z)) d (d - 1)) ∧ ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, Δ z ≠ 0 → (fixedDegreePolynomialAt a z).Separable

End-to-end analytic resultant package for a locally nonmonic family whose displayed leading coefficient does not vanish.

theorem LocalComplexGeometry.exists_analytic_resultant_derivative_and_eventually_separable {n d : ℕ} {z₀ : ComplexEuclidean n} (hd : 0 < d) (a : Fin (d + 1) → ComplexEuclidean n → ℂ) (ha : ∀ (i : Fin (d + 1)), AnalyticAt ℂ (a i) z₀) (htop : ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, a ⟨d, ⋯⟩ z = 1) : ∃ (Δ : ComplexEuclidean n → ℂ), AnalyticAt ℂ Δ z₀ ∧ (∀ᶠ (z : ComplexEuclidean n) in nhds z₀, Δ z = (fixedDegreePolynomialAt a z).resultant (Polynomial.derivative (fixedDegreePolynomialAt a z)) d (d - 1)) ∧ ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, Δ z ≠ 0 → (fixedDegreePolynomialAt a z).Separable

End-to-end local simple-fiber package for a monic analytic family.

Prepared-polynomial specialization

def LocalComplexGeometry.monicCoefficientCompletion {R : Type u_1} {X : Type u_2} [Semiring R] {d : ℕ} (a : Fin d → X → R) : Fin (d + 1) → X → R

Complete the d lower coefficients of a prepared polynomial by its constant leading coefficient one.

Equations

• LocalComplexGeometry.monicCoefficientCompletion a i x = if h : ↑i < d then a ⟨↑i, h⟩ x else 1

@[simp]

theorem LocalComplexGeometry.monicCoefficientCompletion_castSucc {R : Type u_1} {X : Type u_2} [Semiring R] {d : ℕ} (a : Fin d → X → R) (i : Fin d) (x : X) : monicCoefficientCompletion a i.castSucc x = a i x

@[simp]

theorem LocalComplexGeometry.monicCoefficientCompletion_last {R : Type u_1} {X : Type u_2} [Semiring R] {d : ℕ} (a : Fin d → X → R) (x : X) : monicCoefficientCompletion a (Fin.last d) x = 1

theorem LocalComplexGeometry.analyticAt_monicCoefficientCompletion {n d : ℕ} {z₀ : ComplexEuclidean n} (a : Fin d → ComplexEuclidean n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) z₀) (i : Fin (d + 1)) : AnalyticAt ℂ (monicCoefficientCompletion a i) z₀

Completing analytic lower coefficients by one preserves analyticity.

theorem LocalComplexGeometry.fixedDegreePolynomialAt_monicCoefficientCompletion {n d : ℕ} (a : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) : fixedDegreePolynomialAt (monicCoefficientCompletion a) z = preparedPolynomialAt a z

The completed fixed-degree polynomial is the prepared monic polynomial used by the finite-fiber API.

theorem LocalComplexGeometry.exists_analytic_prepared_resultant_and_eventually_separable {n d : ℕ} {z₀ : ComplexEuclidean n} (hd : 0 < d) (a : Fin d → ComplexEuclidean n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) z₀) : ∃ (Δ : ComplexEuclidean n → ℂ), AnalyticAt ℂ Δ z₀ ∧ (∀ᶠ (z : ComplexEuclidean n) in nhds z₀, Δ z = (preparedPolynomialAt a z).resultant (Polynomial.derivative (preparedPolynomialAt a z)) d (d - 1)) ∧ ∀ᶠ (z : ComplexEuclidean n) in nhds z₀, Δ z ≠ 0 → (preparedPolynomialAt a z).Separable

Direct resultant/simple-root package for prepared polynomial fibers.