The order of a transform, through the completion

The proof of [Kol07, Lemma 61] bounds the order of the birational transform π⁻¹_*(f, m) of an element f of order m by m: written as a power series, f has a monomial of degree m; after the chart substitution xᵢ ↦ yᵢ y_r (i < r), xⱼ ↦ yⱼ (j ≥ r) that monomial has degree ≤ 2m, so after division by y_rᵐ the transform has a monomial of degree ≤ m.

This module proves the transfer step of that argument in the abstract form needed later (ordElem_le_of_completionMap_eq_subst). Let R be a regular local ring containing ℚ with a regular system of parameters x, so that R̂ ≅ K⟦x⟧ by the Cohen isomorphism cohenEquiv (Hironaka/Algebra/Local/CohenIso.lean); let φ : R → B be a local homomorphism into a Noetherian local ring, Ψ : K⟦y⟧ ≃ B̂ an isomorphism under which the map R̂ → B̂ induced by φ (completionMap, Hironaka/Algebra/Local/CompletionMap.lean) is the chart substitution chartSubst r (Hironaka/Algebra/Local/ChartSubst.lean), and g ∈ B with φ(x_r)ᵐ g = φ(f), where f ∈ Pᵐ = (x₀, …, x_r)ᵐ has order m. Then ord_B g ≤ m: the series of f has all its monomials of x₀, …, x_r-degree ≥ m (mem_chartCenter_pow_iff_le_weightedOrder', Hironaka/Algebra/Local/SymbolicPower.lean), its substitution is y_rᵐ G' with ord G' ≤ m (exists_X_pow_mul_eq_subst_chartSubst), Ψ(G') is the image of g in B̂ after cancelling φ(x_r)ᵐ in the domain B̂, and orders are preserved by Ψ and by B → B̂ (ordElem_algebraMap_adicCompletion, Hironaka/Algebra/Local/CompletionCoords.lean).

Hironaka/Algebra/Local/ChartCompletion.lean supplies the hypothesis on Ψ for the local ring of the chart ring at its origin, and Hironaka/Algebra/Local/Lemma61.lean derives Kollár's bound at every K-rational point of the chart from it.

Also here: an ideal of order m of a Noetherian local ring contains an element of order m (exists_mem_ordElem_eq_of_ord_eq); the order of the transformed ideal π⁻¹_*(I, m) in a local ring of the chart is bounded by the order of the transform of an element of I of order m (ord_map_transformIdeal_le_of_forall, Kollár's "This shows that ord_{p'} π⁻¹_* I ≤ m"); and the order of an ideal is invariant under isomorphisms of local rings (ord_map_ringEquiv, used throughout Hironaka/Order and Hironaka/Sequence).

theorem IsLocalRing.weight_indicator_filter_le {n : ℕ} (r : Fin n) (d : Fin n →₀ ℕ) : (Finsupp.weight (indicatorWeight {x : Fin n | x ≤ r})) d = ∑ i : Fin n with i ≤ r, d i

The weight of an exponent d for the indicator weight of x₀, …, x_r is ∑_{i ≤ r} dᵢ, the x₀, …, x_r-degree of the monomial x^d.

theorem IsLocalRing.ordElem_le_of_completionMap_eq_subst {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (r : Fin n) {B : Type u_2} [CommRing B] [IsLocalRing B] [IsNoetherianRing B] (φ : R →+* B) [IsLocalHom φ] (Ψ : MvPowerSeries (Fin n) (ResidueField R) ≃+* AdicCompletion (maximalIdeal B) B) (hΨ : ∀ (F : MvPowerSeries (Fin n) (ResidueField R)), (completionMap φ) ((cohenEquiv R x hx hn) F) = Ψ (MvPowerSeries.subst (chartSubst r) F)) {m : ℕ} {f : R} (hf : f ∈ chartCenter x r ^ m) (hord : ordElem f = ↑m) {g : B} (hg : φ (x r) ^ m * g = φ f) : ordElem g ≤ ↑m

The order of a transform through the completion (the proof of [Kol07, Lemma 61]): if the map induced on completions by φ : R → B is the chart substitution under the Cohen isomorphisms (hΨ), f ∈ Pᵐ has order m, and φ(x_r)ᵐ g = φ(f) (so g is the transform π⁻¹_*(f, m)), then ord_B g ≤ m: the series of f has all its monomials of x₀, …, x_r-degree ≥ m, its substitution is y_rᵐ G' with ord G' ≤ m, and Ψ(G') = ι'(g) by cancelling ι'(φ(x_r))ᵐ in the domain B̂ ≅ K⟦y⟧; orders are preserved by Ψ and by ι' : B → B̂.

theorem IsLocalRing.exists_mem_ordElem_eq_of_ord_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {I : Ideal R} {m : ℕ} (hord : ord I = ↑m) : ∃ f ∈ I, ordElem f = ↑m

An ideal of order m contains an element of order m: R is Noetherian, so I is finitely generated, and the order of an ideal is attained on a generator.

theorem IsLocalRing.ord_map_transformIdeal_le_of_forall {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {B : Type u_2} [CommRing B] [IsLocalRing B] {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) (hord : ord I = ↑m) (ψ : ↥(chartRing x r) →+* B) (h : ∀ (f : R) (hf : f ∈ I), ordElem f = ↑m → ordElem (ψ (transformElem x r f ⋯)) ≤ ↑m) : ord (Ideal.map ψ (transformIdeal x r I m)) ≤ ↑m

Kollár's "This shows that ord_{p'} π⁻¹_* I ≤ m" (the proof of [Kol07, Lemma 61]): the order of the transformed ideal π⁻¹_*(I, m) in a local ring B of the chart is bounded by the order of the transform of an element of I of order m.

theorem IsLocalRing.ord_map_ringEquiv {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] (e : A ≃+* B) (K : Ideal A) : ord (Ideal.map (↑e) K) = ord K

The order of an ideal is invariant under isomorphisms of local rings.