The division argument of the parametrization theorem

The division argument of [Fre17, Ch. I, 8.3], simultaneous in the fibre coordinates (see also [GR84, Chapter 3]): with the data of the primitive normalization (ParametrizationPrimitive.lean) in the coordinates of σ = substEquiv L, namely P' = comap σ P, the primitive fibre coordinate X_{i₀} with its monic irreducible Q, Q(X_{i₀}) ∈ P', the denominators A ≠ 0, B_i with A X_i − B_i(X_{i₀}) ∈ P', and monic relations Qf_i(X_i) ∈ P' for every fibre coordinate, a power of A multiplies P' into the ideal J generated by Q(X_{i₀}), the Qf_i(X_i) and the A X_i − B_i(X_{i₀}).

Proof. Let F ∈ P'. By the iterated Weierstrass division (FibreDivision.lean), F ≡ G modulo the relations Qf_i(X_i) (all in J), with G = ∑ a_μ(x_base) x_fibre^μ, μ_i < deg Qf_i. Modulo J, A X_i = B_i(X_{i₀}), so for N := ∑_i deg Qf_i ≥ |μ|, A^N x^μ ≡ A^{N-|μ|} ∏ B_i(X_{i₀})^{μ_i}, and A^N G ≡ H(X_{i₀}) for a polynomial H ∈ 𝒪_d[T]. Since J ⊆ P', H(X_{i₀}) ∈ P', i.e. H vanishes at the class ξ of X_{i₀} in the domain 𝒪_n/P'; the base 𝒪_d is a unique factorization domain (UFD.lean), hence integrally closed, and embeds in 𝒪_n/P' (the Noether normalization is injective), so Q ∣ H (MinpolyDvd.lean) and H(X_{i₀}) ∈ (Q(X_{i₀})) ⊆ J. Hence A^N F ∈ J, with N independent of F.

The reduction A^N F ≡ H(X_{i₀}) mod J holds for every F (not only F ∈ P') and is stated separately as exists_pow_mul_sub_eval_map_mem_span.

theorem Analytic.exists_pow_mul_sub_eval_map_mem_span {n d : ℕ} (e : Fin d ↪ Fin n) (i₀ : Fin n) (Q : Polynomial ↥(Conv ℂ d)) (A : ↥(Conv ℂ d)) (B Qf : Fin n → Polynomial ↥(Conv ℂ d)) (hQf : ∀ i ∉ Set.range ⇑e, (Qf i).Monic) : ∃ (N : ℕ), ∀ (F : ↥(Conv ℂ n)), ∃ (H : Polynomial ↥(Conv ℂ d)), (convEmbed ℂ e) A ^ N * F - Polynomial.eval (convX ℂ i₀) (Polynomial.map (convEmbed ℂ e).toRingHom H) ∈ Ideal.span (({Polynomial.eval (convX ℂ i₀) (Polynomial.map (convEmbed ℂ e).toRingHom Q)} ∪ Set.range fun (i : { i : Fin n // i ∉ Set.range ⇑e }) => Polynomial.eval (convX ℂ ↑i) (Polynomial.map (convEmbed ℂ e).toRingHom (Qf ↑i))) ∪ Set.range fun (i : { i : Fin n // i ∉ Set.range ⇑e }) => (convEmbed ℂ e) A * convX ℂ ↑i - Polynomial.eval (convX ℂ i₀) (Polynomial.map (convEmbed ℂ e).toRingHom (B ↑i)))

The reduction of an arbitrary series: for any F ∈ 𝒪_n, A^N F ≡ H(X_{i₀}) modulo the ideal J generated by Q(X_{i₀}), the monic relations Qf_i(X_i) and the relations A X_i − B_i(X_{i₀}), with H ∈ 𝒪_d[X] and N = ∑_i deg Qf_i independent of F: F is reduced modulo the relations to a polynomial in the fibre coordinates (exists_mem_fibreBox_sub_mem), and there A X_i = B_i(X_{i₀}) clears the fibre coordinates. No ideal P enters.

theorem Analytic.exists_pow_mul_mem_span_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)) (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) (Qf : Fin n → Polynomial ↥(Conv ℂ d)) (hQf : ∀ i ∉ Set.range ⇑e, (Qf i).Monic) (hQfP : ∀ i ∉ Set.range ⇑e, Polynomial.eval (convX ℂ i) (Polynomial.map (convEmbed ℂ e).toRingHom (Qf i)) ∈ Ideal.comap (substEquiv L) P) : ∃ (N : ℕ), ∀ F ∈ Ideal.comap (substEquiv L) P, (convEmbed ℂ e) A ^ N * F ∈ Ideal.span (({Polynomial.eval (convX ℂ i₀) (Polynomial.map (convEmbed ℂ e).toRingHom Q)} ∪ Set.range fun (i : { i : Fin n // i ∉ Set.range ⇑e }) => Polynomial.eval (convX ℂ ↑i) (Polynomial.map (convEmbed ℂ e).toRingHom (Qf ↑i))) ∪ Set.range fun (i : { i : Fin n // i ∉ Set.range ⇑e }) => (convEmbed ℂ e) A * convX ℂ ↑i - Polynomial.eval (convX ℂ i₀) (Polynomial.map (convEmbed ℂ e).toRingHom (B ↑i)))

The division argument of the parametrization theorem ([Fre17, Ch. I, 8.3], simultaneous in the fibre coordinates): for a prime P with the data of the primitive normalization and monic relations for every fibre coordinate, some power of A multiplies comap σ P into the ideal generated by Q(X_{i₀}), the monic relations and the relations A X_i − B_i(X_{i₀}).