The order of the transform at every point of the fibre of the chart

[Kol07, Lemma 61] bounds the order of the birational transform π⁻¹_*(I, m) by m at every point of the blow-up when ord_Z I = max-ord I = m. Kollár's proof computes at the origin of the chart dividing by x_r, where an f ∈ I of order m has the transform x_r^{-m} f(y₁ x_r, …, y_{r−1} x_r, x_r, …), which contains a monomial of degree ≤ m, and reaches the other points by a linear change of coordinates. Such a change exists only for the points of the fibre rational over the residue field κ; Hironaka/Algebra/Local/Lemma61.lean treats exactly those, through the completion. This module obtains the bound at every prime of the fibre, rational or not, by reading the computation in the fibre of the chart over the closed point.

Let R be a regular local ring with regular system of parameters x, r any index, P = (x₀, …, x_r), R' the chart ring dividing by x_r, and 𝔮 a prime of R' lying over 𝔪. For f ∈ Pᵐ of order exactly m, f / x_rᵐ = Q(y) with Q a polynomial of degree ≤ m with a coefficient outside 𝔪 (exists_transformElem_eq_chartPresentation), and modulo 𝔪R', in the fibre R'/𝔪R' ≅ κ[Y] (exists_quotient_map_maximalIdeal_ringEquiv; both from Hironaka/Algebra/Local/ChartGenericFibre.lean), it is the nonzero polynomial Q̄ of degree ≤ m. The quotient map R'_𝔮 → κ[Y]_𝔮̄ is a local homomorphism, along which orders do not decrease, and a nonzero polynomial has order at most its degree at every prime of κ[Y] (ordElem_algebraMap_le_totalDegree, Hironaka/Algebra/Local/PolynomialOrder.lean). Hence

• ord_𝔮 (f / x_rᵐ) ≤ m (ordElem_algebraMap_transformElem_le), and
• for I ≤ Pᵐ with ord I = m, ord_𝔮 π⁻¹_*(I, m) ≤ m (ord_map_transformIdeal_le_of_le_comap).

The argument at the non-rational points is the library's own. Used for Lemma 61 on schemes (Hironaka/Scheme/IdealSheaf/Order/Lemma61.lean), for the order along the centre (Hironaka/Scheme/BlowUpSequence/OrderAlongCenter.lean, Hironaka/Resolution/Algebraic/Hir64/Corollary1.lean) and for the strict transform of a hypersurface of maximal contact (Hironaka/Resolution/Algebraic/MaximalContact/Transform.lean).

theorem IsLocalRing.ordElem_algebraMap_transformElem_le {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (r : Fin n) (𝔮 : Ideal ↥(chartRing x r)) [𝔮.IsPrime] (h𝔮 : maximalIdeal R ≤ Ideal.comap (algebraMap R ↥(chartRing x r)) 𝔮) {m : ℕ} {f : R} (hf : f ∈ chartCenter x r ^ m) (hord : ordElem f = ↑m) : ordElem ((algebraMap (↥(chartRing x r)) (Localization.AtPrime 𝔮)) (transformElem x r f hf)) ≤ ↑m

The order of a transform at every prime of the fibre (the proof of [Kol07, Lemma 61]: "in π⁻¹_* f we get a monomial of degree ≤ m"; at the non-rational primes the argument is the library's own): for f ∈ Pᵐ of order exactly m, the transform f / x_rᵐ has order ≤ m in the localization of the chart ring at every prime 𝔮 lying over 𝔪.

theorem IsLocalRing.ord_map_transformIdeal_le_of_le_comap {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (r : Fin n) (𝔮 : Ideal ↥(chartRing x r)) [𝔮.IsPrime] (h𝔮 : maximalIdeal R ≤ Ideal.comap (algebraMap R ↥(chartRing x r)) 𝔮) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) (hord : ord I = ↑m) : ord (Ideal.map (algebraMap (↥(chartRing x r)) (Localization.AtPrime 𝔮)) (transformIdeal x r I m)) ≤ ↑m

[Kol07, Lemma 61] in local form at every point of the fibre (Hironaka/Algebra/Local/Lemma61.lean is the case of the κ-rational points): if I ≤ Pᵐ and ord I = m, then ord_𝔮 π⁻¹_*(I, m) ≤ m at every prime 𝔮 of the chart ring lying over 𝔪.