Monic relations of the fibre coordinates as polynomials over the base

Under a finite Noether normalization, every coordinate X_i satisfies a monic relation X_i^D + ∑_k c_k(x_base) X_i^k ∈ P in the coordinates of σ (exists_monic_relation_of_finite of Reexpansion.lean, in its shapeSeries form; the finiteness of [Fre17, Ch. I, 7.2] read as monic relations). The parametrization theorem (FibreDivision.lean) uses the relation as a polynomial Qf ∈ 𝒪_d[T] with Qf(X_i) ∈ comap σ P; this module performs the translation.

noncomputable def Analytic.monicOfCoeffs {d D : ℕ} (c : Fin D → ↥(Conv ℂ d)) : Polynomial ↥(Conv ℂ d)

The monic polynomial T^D + ∑_k C (c k) T^k.

Equations

• Analytic.monicOfCoeffs c = Polynomial.X ^ D + ∑ k : Fin D, Polynomial.C (c k) * Polynomial.X ^ ↑k

theorem Analytic.monicOfCoeffs_monic {d D : ℕ} (c : Fin D → ↥(Conv ℂ d)) : (monicOfCoeffs c).Monic

theorem Analytic.eval_map_monicOfCoeffs {n d : ℕ} (e : Fin d ↪ Fin n) (i : Fin n) {D : ℕ} (c : Fin D → ↥(Conv ℂ d)) : Polynomial.eval (convX ℂ i) (Polynomial.map (convEmbed ℂ e).toRingHom (monicOfCoeffs c)) = shapeSeries ℂ i e 0 c

monicOfCoeffs c evaluated at X_i with coefficients embedded along e is the shapeSeries of Reexpansion.lean with translation 0.

theorem Analytic.exists_monic_eval_map_mem_comap {n d : ℕ} (P : Ideal ↥(Conv ℂ n)) (e : Fin d ↪ Fin n) (L : (Fin n → ℂ) ≃L[ℂ] Fin n → ℂ) (hfin : (↑(normMap ℂ P e L)).Finite) (i : Fin n) : ∃ (Qf : Polynomial ↥(Conv ℂ d)), Qf.Monic ∧ Polynomial.eval (convX ℂ i) (Polynomial.map (convEmbed ℂ e).toRingHom Qf) ∈ Ideal.comap (substEquiv L) P

Under a finite Noether normalization, every coordinate X_i satisfies a monic relation Qf(X_i) ∈ comap σ P with Qf ∈ 𝒪_d[T] (from exists_monic_relation_of_finite).