The primitive normalization of a prime germ

The first step of the local parametrization theorem [GR84, Chapter 3, §1] (the second alternative of [Fre17, Ch. I, 8.2] together with the Noether normalization 7.2, generalized to a d-dimensional base): a nonzero prime P ⊆ 𝒪_n = Conv ℂ n has a Noether normalization normMap ℂ P e L (NoetherNormalization.lean, finite and injective) with a fibre coordinate X_{i₀} (i₀ ∉ range e) that is a primitive element of Frac(𝒪_n/P) over Frac(𝒪_d); in the coordinates of σ = substEquiv L, for the ideal P' = comap σ P, its minimal polynomial Q ∈ 𝒪_d[T] is monic irreducible with Q(X_{i₀}) ∈ P', and some A ∈ 𝒪_d ∖ 0, B_i ∈ 𝒪_d[T] have A · X_i − B_i(X_{i₀}) ∈ P' for every fibre coordinate i.

The proof assembles three pieces. (1) Noether normalization exists_noetherNormalization_analytic gives d, e, L₀; since P ≠ ⊥, e is not onto (exists_notMem_range_of_ne_bot: were every coordinate a base coordinate, convEmbed e would be onto 𝒪_n and the injectivity of the normalization would force P = ⊥), so a fibre index i₁ exists. (2) The algebraic core PrimitiveRelations.lean (exists_linear_primitive_relations), applied to R = 𝒪_d, S = 𝒪_n / P with f = normMap ℂ P e L₀ and the fibre classes ξ_i = [σ₀ X_i], returns constants c ∈ ℂ with c_{i₁} = 1, the primitive element γ = ∑ c_j ξ_j, its minimal polynomial Q, and the denominators A, B_i. (3) The coordinate mix L₁ = mixLinear i₁ c (LinearMix.lean) turns the linear form into the coordinate X_{i₁}: with L = L₀.trans L₁, substEquiv L = σ₀ ∘ σ₁, σ₁ fixes the base and the other fibre coordinates and sends X_{i₁} to ∑ c_j X_j, so the normalization is unchanged and the relations of (2) read exactly as the statement demands.

theorem Analytic.convEmbed_surjective_of_surjective {n d : ℕ} (e : Fin d ↪ Fin n) (hsurj : Function.Surjective ⇑e) : Function.Surjective ⇑(convEmbed ℂ e)

If the injection e : Fin d ↪ Fin n is onto, the base embedding convEmbed ℂ e : 𝒪_d → 𝒪_n is onto (rename along the inverse bijection stays convergent).

theorem Analytic.exists_notMem_range_of_ne_bot {n d : ℕ} (P : Ideal ↥(Conv ℂ n)) (hP : P ≠ ⊥) (e : Fin d ↪ Fin n) (L : (Fin n → ℂ) ≃L[ℂ] Fin n → ℂ) (hinj : Function.Injective ⇑(normMap ℂ P e L)) : ∃ (i : Fin n), i ∉ Set.range ⇑e

A Noether normalization normMap ℂ P e L of a nonzero prime P has a fibre coordinate: some index is outside the range of e. Otherwise convEmbed ℂ e is onto 𝒪_n, and the injectivity of mk_P ∘ σ ∘ convEmbed e makes mk_P injective, i.e. P = ⊥.

theorem Analytic.mk_substEquiv_eval_map {n d : ℕ} (P : Ideal ↥(Conv ℂ n)) (e : Fin d ↪ Fin n) (σ : ↥(Conv ℂ n) ≃ₐ[ℂ] ↥(Conv ℂ n)) (Q : Polynomial ↥(Conv ℂ d)) (x : ↥(Conv ℂ n)) : (Ideal.Quotient.mk P) (σ (Polynomial.eval x (Polynomial.map (convEmbed ℂ e).toRingHom Q))) = Polynomial.eval₂ ((Ideal.Quotient.mk P).comp ((↑σ).comp (convEmbed ℂ e).toRingHom)) ((Ideal.Quotient.mk P) (σ x)) Q

The class in 𝒪_n / P of a polynomial in X_{i₀} with coefficients embedded from the base, read in the coordinates of σ, is the polynomial evaluated through mk_P ∘ σ ∘ convEmbed e at the class of σ X_{i₀}.

theorem Analytic.exists_primitive_normalization {n : ℕ} (P : Ideal ↥(Conv ℂ n)) [P.IsPrime] (hP : P ≠ ⊥) : ∃ (d : ℕ) (e : Fin d ↪ Fin n) (L : (Fin n → ℂ) ≃L[ℂ] Fin n → ℂ), Function.Injective ⇑(normMap ℂ P e L) ∧ (↑(normMap ℂ P e L)).Finite ∧ ∃ (i₀ : Fin n) (_ : i₀ ∉ Set.range ⇑e) (Q : Polynomial ↥(Conv ℂ d)) (A : ↥(Conv ℂ d)), Q.Monic ∧ Irreducible Q ∧ A ≠ 0 ∧ Polynomial.eval (convX ℂ i₀) (Polynomial.map (convEmbed ℂ e).toRingHom Q) ∈ Ideal.comap (substEquiv L) P ∧ ∀ i ∉ Set.range ⇑e, ∃ (B : Polynomial ↥(Conv ℂ d)), (convEmbed ℂ e) A * convX ℂ i - Polynomial.eval (convX ℂ i₀) (Polynomial.map (convEmbed ℂ e).toRingHom B) ∈ Ideal.comap (substEquiv L) P

The primitive normalization of a nonzero prime germ ([GR84, Chapter 3, §1]; the second alternative of [Fre17, Ch. I, 8.2] with the Noether normalization 7.2, over a d-dimensional base): a Noether normalization with a fibre coordinate X_{i₀} whose class is a primitive element, its monic irreducible minimal polynomial Q with Q(X_{i₀}) ∈ comap σ P, and denominators A ≠ 0, B_i with A · X_i − B_i(X_{i₀}) ∈ comap σ P for every fibre coordinate.