The graph structure of a prime germ off the discriminant

The local parametrization theorem [GR84, Chapter 3, §1] (the graph structure off the discriminant; [Fre17, Ch. I, 8.2] for a hypersurface): in the coordinates of σ = substEquiv L, with S generating P' = comap σ P, near every point x of the zero-set germ V(P') with (A · Res(Q, Q'))(x ∘ e) ≠ 0 the zero set is the graph of a map φ analytic at x ∘ e, a section of the base projection through x.

Proof. Write u₀ = x ∘ e, t₀ = x_{i₀}. Q(X_{i₀}) ∈ P' vanishes on V(P') (VanishesOn, ZeroSet.lean), so t₀ is a root of the specialized polynomial Q(u₀, ·); where the resultant does not vanish the roots are simple (eventually_isCoprime_specialize, a Bezout identity), so ∂_t Q(u₀, t₀) ≠ 0 and the analytic root branch τ through (u₀, t₀) exists (RootBranch.lean). The graph map is φ(u) = (u on the base, τ(u) at i₀, B_i(u, τ(u)) / A(u) at the other fibre coordinates). Zero set ⊆ graph: Q(X_{i₀}) and the relations A X_i − B_i(X_{i₀}) vanish on V(P'), and the root branch is the unique zero near (u₀, t₀). Graph ⊆ zero set: the generators of the ideal J of ParametrizationDivision.lean vanish on the graph, Q(X_{i₀}) and the relations by construction, the relation of X_{i₀} and the monic relations Qf_i(X_i) (MonicRelation.lean) because their "clearing polynomials" A·T − B_{i₀}(T) and ∑_k Qf_{i,k} A^{D-k} B_i(T)^k vanish at the class of X_{i₀} in 𝒪_n/P', hence are multiples of Q (MinpolyDvd.lean); then the division argument, A^N F ∈ J for F ∈ P', gives the vanishing of every generator of P' where A ≠ 0. All function-level identities are the evalSeries_conv_*_eventually lemmas and PolyEvalFunction.lean. This is the graph structure that makes the regular points of a prime germ dense (Hironaka/Space).

noncomputable def Analytic.clearPoly {d : ℕ} (Qf B : Polynomial ↥(Conv ℂ d)) (A : ↥(Conv ℂ d)) : Polynomial ↥(Conv ℂ d)

The clearing polynomial ∑_{k ≤ D} Qf_k A^{D-k} B^k of a monic relation Qf of degree D along A · X = B(X_{i₀}).

Equations

• Analytic.clearPoly Qf B A = ∑ k ∈ Finset.range (Qf.natDegree + 1), Polynomial.C (Qf.coeff k * A ^ (Qf.natDegree - k)) * B ^ k

theorem Analytic.eval₂_clearPoly_eq {d : ℕ} {S : Type u_1} [CommRing S] (f : ↥(Conv ℂ d) →+* S) (Qf B : Polynomial ↥(Conv ℂ d)) (A : ↥(Conv ℂ d)) {ξ ξi : S} (hrel : f A * ξi = Polynomial.eval₂ f ξ B) : Polynomial.eval₂ f ξ (clearPoly Qf B A) = f A ^ Qf.natDegree * Polynomial.eval₂ f ξi Qf

Where f(A) ξᵢ = B(ξ), the clearing polynomial evaluates to f(A)^D Qf(ξᵢ).

theorem Analytic.mk_eval_map_eq_eval₂ {n d : ℕ} (I : Ideal ↥(Conv ℂ n)) (e : Fin d ↪ Fin n) (i : Fin n) (W : Polynomial ↥(Conv ℂ d)) : (Ideal.Quotient.mk I) (Polynomial.eval (convX ℂ i) (Polynomial.map (convEmbed ℂ e).toRingHom W)) = Polynomial.eval₂ ((Ideal.Quotient.mk I).comp (convEmbed ℂ e).toRingHom) ((Ideal.Quotient.mk I) (convX ℂ i)) W

The class of W(X_i) in a quotient of 𝒪_n is W evaluated through mk ∘ convEmbed e at the class of X_i.

theorem Analytic.pow_mul_eval_sub_clearPoly_mem_span {n d : ℕ} (e : Fin d ↪ Fin n) (i i₀ : Fin n) (Qf B : Polynomial ↥(Conv ℂ d)) (A : ↥(Conv ℂ d)) : (convEmbed ℂ e) A ^ Qf.natDegree * Polynomial.eval (convX ℂ i) (Polynomial.map (convEmbed ℂ e).toRingHom Qf) - Polynomial.eval (convX ℂ i₀) (Polynomial.map (convEmbed ℂ e).toRingHom (clearPoly Qf B A)) ∈ Ideal.span {(convEmbed ℂ e) A * convX ℂ i - Polynomial.eval (convX ℂ i₀) (Polynomial.map (convEmbed ℂ e).toRingHom B)}

A^D Qf(X_i) − G(X_{i₀}) lies in the ideal of the single relation A X_i − B(X_{i₀}), G the clearing polynomial.

theorem Analytic.eval_derivative_ne_zero_of_isCoprime {p : Polynomial ℂ} {t : ℂ} (hcop : IsCoprime p (Polynomial.derivative p)) (ht : Polynomial.eval t p = 0) : Polynomial.eval t (Polynomial.derivative p) ≠ 0

At a root of p, if p is coprime to its derivative then the derivative does not vanish (the Bezout identity).

The elements of 𝒪_n attached to the data, and the function-level facts

noncomputable def Analytic.polyElt {n d : ℕ} (e : Fin d ↪ Fin n) (i₀ : Fin n) (W : Polynomial ↥(Conv ℂ d)) : ↥(Conv ℂ n)

W(X_{i₀}) with coefficients embedded along e.

Equations

• Analytic.polyElt e i₀ W = Polynomial.eval (Analytic.convX ℂ i₀) (Polynomial.map (Analytic.convEmbed ℂ e).toRingHom W)

noncomputable def Analytic.relElt {n d : ℕ} (e : Fin d ↪ Fin n) (i₀ : Fin n) (A : ↥(Conv ℂ d)) (B : Fin n → Polynomial ↥(Conv ℂ d)) (i : Fin n) : ↥(Conv ℂ n)

The relation A X_i − B_i(X_{i₀}).

Equations

• Analytic.relElt e i₀ A B i = (Analytic.convEmbed ℂ e) A * Analytic.convX ℂ i - Analytic.polyElt e i₀ (B i)

noncomputable def Analytic.clearElt {n d : ℕ} (e : Fin d ↪ Fin n) (i₀ : Fin n) (A : ↥(Conv ℂ d)) (B Qf : Fin n → Polynomial ↥(Conv ℂ d)) (i : Fin n) : ↥(Conv ℂ n)

A^{D_i} Qf_i(X_i) − G_i(X_{i₀}), G_i the clearing polynomial.

Equations

• Analytic.clearElt e i₀ A B Qf i = (Analytic.convEmbed ℂ e) A ^ (Qf i).natDegree * Analytic.polyElt e i (Qf i) - Analytic.polyElt e i₀ (Analytic.clearPoly (Qf i) (B i) A)

def Analytic.gensSet {n d : ℕ} (e : Fin d ↪ Fin n) (i₀ : Fin n) (Q : Polynomial ↥(Conv ℂ d)) (A : ↥(Conv ℂ d)) (B Qf : Fin n → Polynomial ↥(Conv ℂ d)) : Set ↥(Conv ℂ n)

The generating set of the ideal J of ParametrizationDivision.lean.

Equations

• One or more equations did not get rendered due to their size.

theorem Analytic.gensSet_finite {n d : ℕ} (e : Fin d ↪ Fin n) (i₀ : Fin n) (Q : Polynomial ↥(Conv ℂ d)) (A : ↥(Conv ℂ d)) (B Qf : Fin n → Polynomial ↥(Conv ℂ d)) : (gensSet e i₀ Q A B Qf).Finite

noncomputable def Analytic.gensFinset {n d : ℕ} (e : Fin d ↪ Fin n) (i₀ : Fin n) (Q : Polynomial ↥(Conv ℂ d)) (A : ↥(Conv ℂ d)) (B Qf : Fin n → Polynomial ↥(Conv ℂ d)) : Finset ↥(Conv ℂ n)

The same generating set as a finset.

Equations

• Analytic.gensFinset e i₀ Q A B Qf = ⋯.toFinset

theorem Analytic.coe_gensFinset {n d : ℕ} (e : Fin d ↪ Fin n) (i₀ : Fin n) (Q : Polynomial ↥(Conv ℂ d)) (A : ↥(Conv ℂ d)) (B Qf : Fin n → Polynomial ↥(Conv ℂ d)) : ↑(gensFinset e i₀ Q A B Qf) = gensSet e i₀ Q A B Qf

noncomputable def Analytic.coeffFinset {n d : ℕ} (Q : Polynomial ↥(Conv ℂ d)) (A : ↥(Conv ℂ d)) (B : Fin n → Polynomial ↥(Conv ℂ d)) : Finset ↥(Conv ℂ d)

The base coefficient series whose functions must be analytic.

Equations

• One or more equations did not get rendered due to their size.

theorem Analytic.mem_coeffFinset_A {n d : ℕ} (Q : Polynomial ↥(Conv ℂ d)) (A : ↥(Conv ℂ d)) (B : Fin n → Polynomial ↥(Conv ℂ d)) : A ∈ coeffFinset Q A B

theorem Analytic.mem_coeffFinset_Q {n d : ℕ} (Q : Polynomial ↥(Conv ℂ d)) (A : ↥(Conv ℂ d)) (B : Fin n → Polynomial ↥(Conv ℂ d)) {k : ℕ} (hk : k ∈ Finset.range (Q.natDegree + 1)) : Q.coeff k ∈ coeffFinset Q A B

theorem Analytic.mem_coeffFinset_B {n d : ℕ} (Q : Polynomial ↥(Conv ℂ d)) (A : ↥(Conv ℂ d)) (B : Fin n → Polynomial ↥(Conv ℂ d)) (i : Fin n) {k : ℕ} (hk : k ∈ Finset.range ((B i).natDegree + 1)) : (B i).coeff k ∈ coeffFinset Q A B

structure Analytic.GraphFacts {n d : ℕ} (e : Fin d ↪ Fin n) (i₀ : Fin n) (Q : Polynomial ↥(Conv ℂ d)) (A : ↥(Conv ℂ d)) (B Qf Hp : Fin n → Polynomial ↥(Conv ℂ d)) (H₀ : Polynomial ↥(Conv ℂ d)) (N : ℕ) (S : Finset ↥(Conv ℂ n)) (x : Fin n → ℂ) : Prop

The facts about a point x near 0 used by the graph argument: the vanishing statements on the zero-set germs, the function-level identities for the elements attached to the data, the analyticity of the base coefficient functions at x ∘ e, and the coprimality of the specialized Q with its derivative off the resultant.

• vq : x ∈ zeroSet S → evalSeries (↑(polyElt e i₀ Q)) x = 0
• vrel (i : { i : Fin n // i ∉ Set.range ⇑e }) : x ∈ zeroSet S → evalSeries (↑(relElt e i₀ A B ↑i)) x = 0
• vAN (g : ↥(Conv ℂ n)) : g ∈ S → x ∈ zeroSet (gensFinset e i₀ Q A B Qf) → evalSeries (↑((convEmbed ℂ e) A ^ N * g)) x = 0
• vcl (i : { i : Fin n // i ∉ Set.range ⇑e }) : x ∈ zeroSet {relElt e i₀ A B ↑i} → evalSeries (↑(clearElt e i₀ A B Qf ↑i)) x = 0
• eq_q : evalSeries (↑(polyElt e i₀ Q)) x = Polynomial.eval (x i₀) (specialize Q (x ∘ ⇑e))
• eq_rel (i : Fin n) : evalSeries (↑(relElt e i₀ A B i)) x = evalSeries (↑A) (x ∘ ⇑e) * x i - Polynomial.eval (x i₀) (specialize (B i) (x ∘ ⇑e))
• eq_AN (g : ↥(Conv ℂ n)) : g ∈ S → evalSeries (↑((convEmbed ℂ e) A ^ N * g)) x = evalSeries (↑A) (x ∘ ⇑e) ^ N * evalSeries (↑g) x
• eq_cl (i : Fin n) : evalSeries (↑(clearElt e i₀ A B Qf i)) x = evalSeries (↑A) (x ∘ ⇑e) ^ (Qf i).natDegree * evalSeries (↑(polyElt e i (Qf i))) x - evalSeries (↑(polyElt e i₀ (clearPoly (Qf i) (B i) A))) x
• eq_g (i : { i : Fin n // i ∉ Set.range ⇑e }) : evalSeries (↑(polyElt e i₀ (clearPoly (Qf ↑i) (B ↑i) A))) x = evalSeries (↑(polyElt e i₀ Q)) x * evalSeries (↑(polyElt e i₀ (Hp ↑i))) x
• eq_rel0 : evalSeries (↑(relElt e i₀ A B i₀)) x = evalSeries (↑(polyElt e i₀ Q)) x * evalSeries (↑(polyElt e i₀ H₀)) x
• an (c : ↥(Conv ℂ d)) : c ∈ coeffFinset Q A B → AnalyticAt ℂ (evalSeries ↑c) (x ∘ ⇑e)
• cop : evalSeries (↑(Q.resultant (Polynomial.derivative Q))) (x ∘ ⇑e) ≠ 0 → IsCoprime (specialize Q (x ∘ ⇑e)) (Polynomial.derivative (specialize Q (x ∘ ⇑e)))
• eq_ARes : evalSeries (↑(A * Q.resultant (Polynomial.derivative Q))) (x ∘ ⇑e) = evalSeries (↑A) (x ∘ ⇑e) * evalSeries (↑(Q.resultant (Polynomial.derivative Q))) (x ∘ ⇑e)

theorem Analytic.evalSeries_conv_neg_eventually' {n : ℕ} (g : ↥(Conv ℂ n)) : evalSeries ↑(-g) =ᶠ[nhds 0] fun (x : Fin n → ℂ) => -evalSeries (↑g) x

The function of −g near 0.

theorem Analytic.evalSeries_relElt_eventually {n d : ℕ} {e : Fin d ↪ Fin n} {i₀ : Fin n} (A : ↥(Conv ℂ d)) (B : Fin n → Polynomial ↥(Conv ℂ d)) (i : Fin n) : evalSeries ↑(relElt e i₀ A B i) =ᶠ[nhds 0] fun (x : Fin n → ℂ) => evalSeries (↑A) (x ∘ ⇑e) * x i - Polynomial.eval (x i₀) (specialize (B i) (x ∘ ⇑e))

The function of the relation A X_i − B_i(X_{i₀}) near 0.

theorem Analytic.eventually_graphFacts {n d : ℕ} {e : Fin d ↪ Fin n} {i₀ : Fin n} (Q : Polynomial ↥(Conv ℂ d)) (hQdeg : 0 < Q.natDegree) (A : ↥(Conv ℂ d)) (B Qf Hp : Fin n → Polynomial ↥(Conv ℂ d)) (H₀ : Polynomial ↥(Conv ℂ d)) (N : ℕ) (S : Finset ↥(Conv ℂ n)) (P' : Ideal ↥(Conv ℂ n)) (hS : Ideal.span ↑S = P') (hQP : polyElt e i₀ Q ∈ P') (hB : ∀ i ∉ Set.range ⇑e, relElt e i₀ A B i ∈ P') (hN : ∀ F ∈ P', (convEmbed ℂ e) A ^ N * F ∈ Ideal.span (gensSet e i₀ Q A B Qf)) (hHp : ∀ i ∉ Set.range ⇑e, clearPoly (Qf i) (B i) A = Q * Hp i) (hH₀ : Polynomial.C A * Polynomial.X - B i₀ = Q * H₀) : ∀ᶠ (x : Fin n → ℂ) in nhds 0, GraphFacts e i₀ Q A B Qf Hp H₀ N S x

All the facts hold on a neighbourhood of 0.

theorem Analytic.exists_graph_of_isPrime {n : ℕ} (P : Ideal ↥(Conv ℂ n)) [P.IsPrime] {d : ℕ} (e : Fin d ↪ Fin n) (L : (Fin n → ℂ) ≃L[ℂ] Fin n → ℂ) (hinj : Function.Injective ⇑(normMap ℂ P e L)) (hfin : (↑(normMap ℂ P e L)).Finite) (i₀ : Fin n) (hi₀ : i₀ ∉ Set.range ⇑e) (Q : Polynomial ↥(Conv ℂ d)) (hQ : Q.Monic) (hQirr : Irreducible Q) (hQP : Polynomial.eval (convX ℂ i₀) (Polynomial.map (convEmbed ℂ e).toRingHom Q) ∈ Ideal.comap (substEquiv L) P) (A : ↥(Conv ℂ d)) (hA : A ≠ 0) (B : Fin n → Polynomial ↥(Conv ℂ d)) (hB : ∀ i ∉ Set.range ⇑e, (convEmbed ℂ e) A * convX ℂ i - Polynomial.eval (convX ℂ i₀) (Polynomial.map (convEmbed ℂ e).toRingHom (B i)) ∈ Ideal.comap (substEquiv L) P) {S : Finset ↥(Conv ℂ n)} (hS : Ideal.span ↑S = Ideal.comap (substEquiv L) P) : ∀ᶠ (x : Fin n → ℂ) in nhds 0, x ∈ zeroSet S → evalSeries (↑(A * Q.resultant (Polynomial.derivative Q))) (x ∘ ⇑e) ≠ 0 → ∃ (φ : (Fin d → ℂ) → Fin n → ℂ), AnalyticAt ℂ φ (x ∘ ⇑e) ∧ φ (x ∘ ⇑e) = x ∧ (∀ (u : Fin d → ℂ), φ u ∘ ⇑e = u) ∧ ∀ᶠ (y : Fin n → ℂ) in nhds x, y ∈ zeroSet S ↔ y = φ (y ∘ ⇑e)

The local parametrization theorem [GR84, Chapter 3, §1], the graph structure off the discriminant: for a prime P with the data of the primitive normalization, near every point x of the zero-set germ of comap σ P with (A · Res(Q, Q'))(x ∘ e) ≠ 0 the zero set is the graph of a map analytic at x ∘ e, a section of the base projection through x.