The order of a polynomial at a point is at most its degree

Kollár's proof of [Kol07, Lemma 61] finds, in the transform π_*^{-1} f of an element of order m, "a monomial of degree ≤ m", and concludes ord ≤ m at the origin of the chart; the points of the fibre that are not κ-rational are reached in the text by a linear change of coordinates, which only exists over an algebraically closed field. This file replaces the linear change by the following elementary fact, valid at every prime of a polynomial ring over any field: a nonzero polynomial P ∈ κ[Y] has order at most deg P in the localization at every prime 𝔮 (ordElem_algebraMap_le_totalDegree); not in the sources. It is applied to the exceptional fibre of the chart of a blow-up in Hironaka/Algebra/Local/ChartFibre.lean.

Why. Let L be the residue field of 𝔮 (the fraction field of κ[Y]/𝔮) and a ∈ L^σ the image of the coordinates — the generic point of V(𝔮). Substituting Y_i ↦ a_i + Y_i gives a ring homomorphism κ[Y] → L⟦Y⟧ whose constant term is evaluation at a; it sends 𝔮 into the maximal ideal and the complement of 𝔮 to units, so it extends to a local homomorphism κ[Y]_𝔮 → L⟦Y⟧. Orders do not decrease along local homomorphisms (ord_le_ord_map), the order in L⟦Y⟧ is Mathlib's MvPowerSeries.order (MvPowerSeries.ordElem_eq_order), and the image of P is the polynomial P(a + Y), nonzero of degree ≤ deg P, whose order is at most the degree of any of its monomials.

theorem IsLocalRing.ord_span_singleton {R : Type u_1} [CommRing R] [IsLocalRing R] (f : R) : ord (Ideal.span {f}) = ordElem f

The order of a principal ideal is the order of its generator.

theorem IsLocalRing.ordElem_le_ordElem_map {R : Type u_1} [CommRing R] [IsLocalRing R] {S : Type u_2} [CommRing S] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (f : R) : ordElem f ≤ ordElem (φ f)

Orders of elements do not decrease along local homomorphisms.

theorem IsLocalRing.order_coe_le_totalDegree {σ : Type u_2} {L : Type u_3} [Field L] {Q : MvPolynomial σ L} (hQ : Q ≠ 0) : (↑Q).order ≤ ↑Q.totalDegree

A nonzero polynomial Q has order at most its total degree in L⟦Y⟧.

theorem IsLocalRing.totalDegree_finset_prod_le {σ : Type u_2} {L : Type u_3} [CommSemiring L] {ι : Type u_4} (s : Finset ι) (g : ι → MvPolynomial σ L) : (∏ i ∈ s, g i).totalDegree ≤ ∑ i ∈ s, (g i).totalDegree

The total degree of a finite product is at most the sum of the total degrees.

theorem IsLocalRing.totalDegree_eval₂Hom_add_le {K : Type u_1} [Field K] {σ : Type u_2} {L : Type u_3} [Field L] (φ : K →+* L) (a : σ → L) (P : MvPolynomial σ K) : ((MvPolynomial.eval₂Hom (MvPolynomial.C.comp φ) fun (i : σ) => MvPolynomial.C (a i) + MvPolynomial.X i) P).totalDegree ≤ P.totalDegree

The substitution Y_i ↦ a_i + Y_i does not raise the total degree.

theorem IsLocalRing.ordElem_algebraMap_le_totalDegree {K : Type u_1} [Field K] {σ : Type u_2} [Finite σ] (𝔮 : Ideal (MvPolynomial σ K)) [𝔮.IsPrime] {P : MvPolynomial σ K} (hP : P ≠ 0) : ordElem ((algebraMap (MvPolynomial σ K) (Localization.AtPrime 𝔮)) P) ≤ ↑P.totalDegree

A nonzero polynomial has order at most its degree at every prime of κ[Y] (in place of the linear change of coordinates in the proof of [Kol07, Lemma 61]; not in the sources).