The exceptional divisor of the chart at the generic point

Let R be a regular local ring with a regular system of parameters x : Fin n → R (𝔪 = (x), n = dim R), and let r be the last index (r + 1 = n), so that the centre P = (x₀, …, x_r) is 𝔪 itself and the chart ring R' = R[xᵢ/x_r : i < r] is the chart dividing by x_r of the blow-up of the closed point. Geometrically this is the local blow-up of a smooth variety at the generic point of a smooth centre Z, in coordinates adapted to Z. In this chart:

• an element f of order exactly m is ∑_{|α| = m} c_α x^α with some coefficient a unit (exists_leading_form, exists_sum_monomials_unit_coeff); the monomials of degree m span 𝔪ᵐ (span_range_pow_eq_span_monomials), and those in x₀, …, x_r span Pᵐ (span_image_pow_eq_span_monomials);
• R'/(x_r) ≅ κ[Yᵢ : i < r] with κ = R/𝔪 (exists_quotient_span_algebraMap_x_ringEquiv), from the presentation R' = R[Y]/(x_r Yᵢ − xᵢ) of Hironaka/Algebra/Local/ChartPresentation.lean and (x_r Yᵢ − xᵢ, x_r) = 𝔪 R[Y]; so (x_r) is a prime of R' (isPrime_span_algebraMap_x), the generic point of the exceptional divisor of the chart, and for f of order m, f = x_rᵐ (∑ c_α y^{α'} + x_r(…)) in R' does not lie in (x_r)^{m+1} (algebraMap_notMem_span_pow_succ);
• the order of I R' along the prime (x_r), that is, in the discrete valuation ring R'_{(x_r)}, equals ord I (ordAlong_span_algebraMap_x_map). This is the remark after [Kol07, Definition 47] that ord_Z I equals the multiplicity of π^* I along the exceptional divisor, and the definition of the strict transform of an ideal in [Hau14, §6] (following Definition 6.2), where the maximal exponent k in f^* = h^k f^s is the order of f^* along the exceptional divisor.

The computation of the leading form in the divided coordinates is that of the proof of [Kol07, Lemma 61]: for f ∈ Pᵐ of order exactly m, f / x_rᵐ = Q(y) for a polynomial Q of degree ≤ m with a coefficient outside 𝔪 (exists_transformElem_eq_chartPresentation).

Several statements are also proved for a partial centre P = (x₀, …, x_r) with r not the last index: (x_r Yᵢ − xᵢ, x_r) = P R[Y] (chartRelations_sup_span_C_eq_map_C_chartCenter), R'/(x_r) ≅ (R/P)[Yᵢ : i < r] (exists_quotient_span_algebraMap_x_ringEquiv_chartCenter), (x_r) is prime in R' (isPrime_span_algebraMap_x_of_chartCenter) and (x_r) ∩ R = P (comap_span_algebraMap_x_eq_chartCenter); and the fibre of the chart over the closed point is R'/𝔪R' ≅ κ[Yᵢ : i < r] for every r (exists_quotient_map_maximalIdeal_ringEquiv).

Used for the order of the transform at every point of the fibre (Hironaka/Algebra/Local/ChartFibre.lean), for the order along the exceptional divisor (Hironaka/Scheme/IdealSheaf/Order/ExceptionalOrder.lean, Hironaka/Scheme/BlowUpSequence/OrderAlongCenter.lean, Hironaka/Resolution/Algebraic/Wlo05/EmbeddedCP3Exceptional.lean), for the strict transform of a hypersurface of maximal contact (Hironaka/Resolution/Algebraic/MaximalContact/Transform.lean) and on manifolds (Hironaka/Resolution/Analytic/OrderReduction/BMO/Step1Purity.lean).

Leading forms

theorem IsLocalRing.prod_pow_add {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (α β : Fin n →₀ ℕ) : ∏ j : Fin n, x j ^ (α + β) j = (∏ j : Fin n, x j ^ α j) * ∏ j : Fin n, x j ^ β j

Monomials are multiplicative in the exponent.

theorem IsLocalRing.prod_pow_single {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (i : Fin n) : ∏ j : Fin n, x j ^ (Finsupp.single i 1) j = x i

The monomial of the exponent single i 1 is x_i.

theorem IsLocalRing.span_image_pow_eq_span_monomials {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (s : Set (Fin n)) (m : ℕ) : Ideal.span (x '' s) ^ m = Ideal.span {z : R | ∃ (α : Fin n →₀ ℕ), (Finsupp.degree α = m ∧ ∀ i ∉ s, α i = 0) ∧ z = ∏ i : Fin n, x i ^ α i}

The m-th power of the ideal generated by the xᵢ, i ∈ s, is spanned by the monomials of degree m in those xᵢ (applied to the powers of the centre P = (x₀, …, x_r)).

theorem IsLocalRing.span_range_pow_eq_span_monomials {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (m : ℕ) : Ideal.span (Set.range x) ^ m = Ideal.span {z : R | ∃ (α : Fin n →₀ ℕ), Finsupp.degree α = m ∧ z = ∏ i : Fin n, x i ^ α i}

The m-th power of the ideal generated by x is spanned by the monomials of degree m in the x_i.

theorem IsLocalRing.exists_sum_monomials_of_mem_span {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) {p : (Fin n →₀ ℕ) → Prop} {f : R} (hf : f ∈ Ideal.span {z : R | ∃ (α : Fin n →₀ ℕ), p α ∧ z = ∏ i : Fin n, x i ^ α i}) : ∃ (S : Finset (Fin n →₀ ℕ)) (c : (Fin n →₀ ℕ) → R), (∀ α ∈ S, p α) ∧ f = ∑ α ∈ S, c α * ∏ i : Fin n, x i ^ α i

Every element of the span of the monomials with exponents satisfying p is a finite combination of them.

theorem IsLocalRing.exists_coeff_notMem_of_ordElem_eq {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) {m : ℕ} {S : Finset (Fin n →₀ ℕ)} {c : (Fin n →₀ ℕ) → R} (hS : ∀ α ∈ S, Finsupp.degree α = m) {f : R} (hfeq : f = ∑ α ∈ S, c α * ∏ i : Fin n, x i ^ α i) (hf : ordElem f = ↑m) : ∃ α ∈ S, c α ∉ maximalIdeal R

If every coefficient of a combination of degree-m monomials lies in 𝔪, the element lies in 𝔪^{m+1}; so a combination of order exactly m has a coefficient outside 𝔪.

theorem IsLocalRing.exists_sum_monomials_unit_coeff {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (f : R) (m : ℕ) (hf : ordElem f = ↑m) : ∃ (S : Finset (Fin n →₀ ℕ)) (c : (Fin n →₀ ℕ) → R), (∀ α ∈ S, Finsupp.degree α = m) ∧ f = ∑ α ∈ S, c α * ∏ i : Fin n, x i ^ α i ∧ ∃ α ∈ S, c α ∉ maximalIdeal R

An element of order exactly m is a combination of degree-m monomials with some coefficient a unit.

theorem IsLocalRing.exists_sum_monomials_unit_coeff_of_mem_chartCenter_pow {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (r : Fin n) {f : R} {m : ℕ} (hf : f ∈ chartCenter x r ^ m) (hord : ordElem f = ↑m) : ∃ (S : Finset (Fin n →₀ ℕ)) (c : (Fin n →₀ ℕ) → R), (∀ α ∈ S, Finsupp.degree α = m ∧ ∀ (i : Fin n), r < i → α i = 0) ∧ f = ∑ α ∈ S, c α * ∏ i : Fin n, x i ^ α i ∧ ∃ α ∈ S, c α ∉ maximalIdeal R

(The proof of [Kol07, Lemma 61].) An element of Pᵐ = (x₀, …, x_r)ᵐ of order exactly m is a combination of degree-m monomials in x₀, …, x_r with some coefficient a unit.

theorem IsLocalRing.exists_leading_form {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (f : R) (m : ℕ) (hf : ordElem f = ↑m) : ∃ (S : Finset (Fin n →₀ ℕ)) (c : (Fin n →₀ ℕ) → R) (g : R), (∀ α ∈ S, Finsupp.degree α = m) ∧ f = ∑ α ∈ S, c α * ∏ i : Fin n, x i ^ α i + g ∧ g ∈ maximalIdeal R ^ (m + 1) ∧ ∃ α ∈ S, c α ∉ maximalIdeal R

An element f of order exactly m of a regular local ring with regular system of parameters x is ∑_{|α| = m} c_α x^α + g with g ∈ 𝔪^{m+1} (in fact g = 0 here) and some coefficient c_α a unit: its leading form is a nonzero form of degree m.

The exceptional divisor of the chart is affine space over the residue field

theorem IsLocalRing.exists_castLE_eq_of_ne {n : ℕ} (r : Fin n) (hr : ↑r + 1 = n) {j : Fin n} (hj : j ≠ r) : ∃ (i : Fin ↑r), Fin.castLE ⋯ i = j

Every index other than the last one is Fin.castLE of an index below r.

theorem IsLocalRing.chartRelations_sup_span_C_eq_map_C_maximalIdeal {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (r : Fin n) (hr : ↑r + 1 = n) : chartRelations x r ⊔ Ideal.span {MvPolynomial.C (x r)} = Ideal.map MvPolynomial.C (maximalIdeal R)

The relations of the presentation together with x_r generate 𝔪 R[Y]: (x_r Y_i − x_i, x_r) = (x_0, …, x_r) R[Y].

theorem IsLocalRing.exists_quotient_map_ringEquiv_of_sup_eq_map {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (P : Ideal R) (L : Ideal (MvPolynomial (Fin ↑r) R)) (hsup : RingHom.ker (chartPresentation x r) ⊔ L = Ideal.map MvPolynomial.C P) : ∃ (e : ↥(chartRing x r) ⧸ Ideal.map (chartPresentation x r).toRingHom L ≃+* MvPolynomial (Fin ↑r) (R ⧸ P)), (∀ (a : R), e ((Ideal.Quotient.mk (Ideal.map (chartPresentation x r).toRingHom L)) ((algebraMap R ↥(chartRing x r)) a)) = MvPolynomial.C ((Ideal.Quotient.mk P) a)) ∧ ∀ (i : Fin ↑r), e ((Ideal.Quotient.mk (Ideal.map (chartPresentation x r).toRingHom L)) (chartYR x r (Fin.castLE ⋯ i))) = MvPolynomial.X i

For any ideal P of R: the quotient of the chart ring by the image of an ideal L ≤ R[Y] with ker ⊔ L = P R[Y] is (R/P)[Y], with Yᵢ ↦ yᵢ = xᵢ/x_r and the constants the classes of R, from the presentation R' = R[Y]/(x_r Yᵢ − xᵢ) (ker_chartPresentation).

theorem IsLocalRing.exists_quotient_map_ringEquiv {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (L : Ideal (MvPolynomial (Fin ↑r) R)) (hsup : RingHom.ker (chartPresentation x r) ⊔ L = Ideal.map MvPolynomial.C (maximalIdeal R)) : ∃ (e : ↥(chartRing x r) ⧸ Ideal.map (chartPresentation x r).toRingHom L ≃+* MvPolynomial (Fin ↑r) (ResidueField R)), (∀ (a : R), e ((Ideal.Quotient.mk (Ideal.map (chartPresentation x r).toRingHom L)) ((algebraMap R ↥(chartRing x r)) a)) = MvPolynomial.C ((residue R) a)) ∧ ∀ (i : Fin ↑r), e ((Ideal.Quotient.mk (Ideal.map (chartPresentation x r).toRingHom L)) (chartYR x r (Fin.castLE ⋯ i))) = MvPolynomial.X i

The quotient of the chart ring by the image of an ideal L ≤ R[Y] with ker ⊔ L = 𝔪 R[Y] is κ[Y], with Yᵢ ↦ yᵢ = xᵢ/x_r and the constants the residues of R: the case P = 𝔪 of exists_quotient_map_ringEquiv_of_sup_eq_map (κ = R/𝔪, and residue is Ideal.Quotient.mk 𝔪 definitionally).

theorem IsLocalRing.exists_quotient_map_maximalIdeal_ringEquiv {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) : ∃ (e : ↥(chartRing x r) ⧸ Ideal.map (algebraMap R ↥(chartRing x r)) (maximalIdeal R) ≃+* MvPolynomial (Fin ↑r) (ResidueField R)), (∀ (a : R), e ((Ideal.Quotient.mk (Ideal.map (algebraMap R ↥(chartRing x r)) (maximalIdeal R))) ((algebraMap R ↥(chartRing x r)) a)) = MvPolynomial.C ((residue R) a)) ∧ ∀ (i : Fin ↑r), e ((Ideal.Quotient.mk (Ideal.map (algebraMap R ↥(chartRing x r)) (maximalIdeal R))) (chartYR x r (Fin.castLE ⋯ i))) = MvPolynomial.X i

The fibre of the chart dividing by x_r over the closed point of Spec R is affine r-space over the residue field: R'/𝔪R' ≅ κ[Yᵢ : i < r], for every index r. When r is the last index, 𝔪R' = (x_r) and this is exists_quotient_span_algebraMap_x_ringEquiv.

theorem IsLocalRing.exists_quotient_span_algebraMap_x_ringEquiv {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) (hr : ↑r + 1 = n) : ∃ (e : ↥(chartRing x r) ⧸ Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)} ≃+* MvPolynomial (Fin ↑r) (ResidueField R)), (∀ (a : R), e ((Ideal.Quotient.mk (Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)})) ((algebraMap R ↥(chartRing x r)) a)) = MvPolynomial.C ((residue R) a)) ∧ ∀ (i : Fin ↑r), e ((Ideal.Quotient.mk (Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)})) (chartYR x r (Fin.castLE ⋯ i))) = MvPolynomial.X i

The exceptional divisor of the chart dividing by x_r, r the last index, is affine space over the residue field: R'/(x_r) ≅ κ[Yᵢ : i < r] with Yᵢ ↦ yᵢ = xᵢ/x_r and the constants the residues of R, from the presentation R' = R[Y]/(x_r Yᵢ − xᵢ) (ker_chartPresentation).

The partial centre P = (x₀, …, x_r): R'/(x_r) ≅ (R/P)[Y]

theorem IsLocalRing.chartRelations_sup_span_C_eq_map_C_chartCenter {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) : chartRelations x r ⊔ Ideal.span {MvPolynomial.C (x r)} = Ideal.map MvPolynomial.C (chartCenter x r)

The relations of the presentation together with x_r generate P R[Y] for the partial centre P = chartCenter x r = (x₀, …, x_r): (x_r Yᵢ − xᵢ, x_r) = (x₀, …, x_r) R[Y]. No hypothesis on x or r is needed; chartRelations_sup_span_C_eq_map_C_maximalIdeal is the case of the last index, where P = 𝔪.

theorem IsLocalRing.exists_quotient_span_algebraMap_x_ringEquiv_chartCenter {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) : ∃ (e : ↥(chartRing x r) ⧸ Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)} ≃+* MvPolynomial (Fin ↑r) (R ⧸ chartCenter x r)), (∀ (a : R), e ((Ideal.Quotient.mk (Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)})) ((algebraMap R ↥(chartRing x r)) a)) = MvPolynomial.C ((Ideal.Quotient.mk (chartCenter x r)) a)) ∧ ∀ (i : Fin ↑r), e ((Ideal.Quotient.mk (Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)})) (chartYR x r (Fin.castLE ⋯ i))) = MvPolynomial.X i

For a partial centre: the exceptional divisor of the chart dividing by x_r of the blow-up of P = (x₀, …, x_r) is affine r-space over R/P: R'/(x_r) ≅ (R/P)[Yᵢ : i < r] with Yᵢ ↦ yᵢ = xᵢ/x_r and the constants the classes of R, from the presentation R' = R[Y]/(x_r Yᵢ − xᵢ) (ker_chartPresentation) and (x_r Yᵢ − xᵢ, x_r) = P R[Y] (chartRelations_sup_span_C_eq_map_C_chartCenter).

theorem IsLocalRing.isPrime_span_algebraMap_x_of_chartCenter {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.span {(algebraMap R ↥(chartRing x r)) (x r)}).IsPrime

(x_r) is a prime of the chart ring of the partial centre P = (x₀, …, x_r): R'/(x_r) ≅ (R/P)[Y] is a domain, P being prime (isPrime_chartCenter).

theorem IsLocalRing.comap_span_algebraMap_x_eq_chartCenter {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.comap (algebraMap R ↥(chartRing x r)) (Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)}) = chartCenter x r

(x_r) ∩ R = P for the partial centre P = (x₀, …, x_r): the constants killed in R'/(x_r) ≅ (R/P)[Y] are those with class 0 in R/P.

theorem IsLocalRing.isPrime_span_algebraMap_x {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) (hr : ↑r + 1 = n) : (Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)}).IsPrime

(x_r) is a prime of the chart ring when r is the last index: the generic point of the exceptional divisor in the chart dividing by x_r.

The order along the exceptional divisor of the chart

noncomputable def IsLocalRing.restrictExp {n : ℕ} (r : Fin n) (α : Fin n →₀ ℕ) : Fin ↑r →₀ ℕ

The exponents of the divided coordinates: the restriction of α : Fin n →₀ ℕ to the indices below r.

Equations

• IsLocalRing.restrictExp r α = Finsupp.equivFunOnFinite.symm fun (i : Fin ↑r) => α (Fin.castLE ⋯ i)

theorem IsLocalRing.restrictExp_apply {n : ℕ} (r : Fin n) (α : Fin n →₀ ℕ) (i : Fin ↑r) : (restrictExp r α) i = α (Fin.castLE ⋯ i)

theorem IsLocalRing.not_lt_of_succ_eq {n : ℕ} (r : Fin n) (hr : ↑r + 1 = n) (i : Fin n) : ¬r < i

When r is the last index, no index exceeds it.

theorem IsLocalRing.prod_eq_prod_castLE_of_forall_gt {n : ℕ} (r : Fin n) {M : Type u_1} [CommMonoid M] (g : Fin n → M) (hg : ∀ (i : Fin n), r < i → g i = 1) : ∏ j : Fin n, g j = ∏ i : Fin (↑r + 1), g (Fin.castLE ⋯ i)

A product over Fin n of factors that are 1 beyond r is a product over the indices ≤ r.

theorem IsLocalRing.sum_eq_sum_castLE_of_forall_gt {n : ℕ} (r : Fin n) {M : Type u_1} [AddCommMonoid M] (g : Fin n → M) (hg : ∀ (i : Fin n), r < i → g i = 0) : ∑ j : Fin n, g j = ∑ i : Fin (↑r + 1), g (Fin.castLE ⋯ i)

A sum over Fin n of terms that vanish beyond r is a sum over the indices ≤ r.

theorem IsLocalRing.degree_eq_apply_add_sum' {n : ℕ} (r : Fin n) (α : Fin n →₀ ℕ) (hα : ∀ (i : Fin n), r < i → α i = 0) : Finsupp.degree α = α r + ∑ i : Fin ↑r, α (Fin.castLE ⋯ i)

The degree of an exponent supported in x_0, …, x_r is the exponent of x_r plus the degree of its restriction to the divided coordinates.

theorem IsLocalRing.eq_of_restrictExp_eq' {n : ℕ} (r : Fin n) {α β : Fin n →₀ ℕ} {m : ℕ} (hα : Finsupp.degree α = m) (hβ : Finsupp.degree β = m) (hα' : ∀ (i : Fin n), r < i → α i = 0) (hβ' : ∀ (i : Fin n), r < i → β i = 0) (h : restrictExp r α = restrictExp r β) : α = β

Two exponents of the same degree supported in x_0, …, x_r with the same restriction agree.

theorem IsLocalRing.prod_algebraMap_pow_eq' {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (α : Fin n →₀ ℕ) (hα : ∀ (i : Fin n), r < i → α i = 0) : ∏ j : Fin n, (algebraMap R ↥(chartRing x r)) (x j) ^ α j = (algebraMap R ↥(chartRing x r)) (x r) ^ Finsupp.degree α * ∏ i : Fin ↑r, chartYR x r (Fin.castLE ⋯ i) ^ α (Fin.castLE ⋯ i)

Kollár's substitution x_i ↦ y_i x_r on a monomial supported in x_0, …, x_r: φ(x^α) = x_r^{|α|} · y^{α'} with α' the restriction of α to the divided coordinates.

theorem IsLocalRing.univ_erase_eq_map_castLEEmb {n : ℕ} (r : Fin n) (hr : ↑r + 1 = n) : Finset.univ.erase r = Finset.map (Fin.castLEEmb ⋯) Finset.univ

The indices other than the last one are the castLE images of Fin r.

theorem IsLocalRing.degree_eq_apply_add_sum {n : ℕ} (r : Fin n) (hr : ↑r + 1 = n) (α : Fin n →₀ ℕ) : Finsupp.degree α = α r + ∑ i : Fin ↑r, α (Fin.castLE ⋯ i)

The degree of an exponent is the exponent of x_r plus the degree of its restriction.

theorem IsLocalRing.eq_of_restrictExp_eq {n : ℕ} (r : Fin n) (hr : ↑r + 1 = n) {α β : Fin n →₀ ℕ} {m : ℕ} (hα : Finsupp.degree α = m) (hβ : Finsupp.degree β = m) (h : restrictExp r α = restrictExp r β) : α = β

Two exponents of the same degree with the same restriction agree.

theorem IsLocalRing.prod_algebraMap_pow_eq {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (hr : ↑r + 1 = n) (α : Fin n →₀ ℕ) : ∏ j : Fin n, (algebraMap R ↥(chartRing x r)) (x j) ^ α j = (algebraMap R ↥(chartRing x r)) (x r) ^ Finsupp.degree α * ∏ i : Fin ↑r, chartYR x r (Fin.castLE ⋯ i) ^ α (Fin.castLE ⋯ i)

Kollár's substitution x_i ↦ y_i x_r on a monomial of degree m: φ(x^α) = x_r^m · y^{α'} with α' the restriction of α to the divided coordinates.

theorem IsLocalRing.chartCenter_eq_span_range_of_succ_eq {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (hr : ↑r + 1 = n) : chartCenter x r = Ideal.span (Set.range x)

When r is the last index, the centre P = (x_0, …, x_r) is the whole (x).

theorem IsLocalRing.exists_transformElem_eq_chartPresentation {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (r : Fin n) {f : R} {m : ℕ} (hf : f ∈ chartCenter x r ^ m) (hord : ordElem f = ↑m) : ∃ (Q : MvPolynomial (Fin ↑r) R), transformElem x r f hf = (chartPresentation x r) Q ∧ Q.totalDegree ≤ m ∧ ∃ (β : Fin ↑r →₀ ℕ), Q.coeff β ∉ maximalIdeal R

(The proof of [Kol07, Lemma 61].) For f ∈ Pᵐ of order exactly m, the transform f / x_rᵐ is Q(y) for a polynomial Q of degree ≤ m with a coefficient outside 𝔪: the leading form of f read in the divided coordinates.

theorem IsLocalRing.exists_algebraMap_eq_pow_mul_chartPresentation {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (r : Fin n) (hr : ↑r + 1 = n) (f : R) (m : ℕ) (hf : ordElem f = ↑m) : ∃ (Q : MvPolynomial (Fin ↑r) R), (algebraMap R ↥(chartRing x r)) f = (algebraMap R ↥(chartRing x r)) (x r) ^ m * (chartPresentation x r) Q ∧ ∃ (β : Fin ↑r →₀ ℕ), Q.coeff β ∉ maximalIdeal R

(The proof of [Kol07, Lemma 61].) For f of order exactly m and r the last index, f = x_rᵐ · Q(y) in R' for a polynomial Q with a coefficient outside 𝔪, the leading form of f read in the divided coordinates.

theorem IsLocalRing.algebraMap_notMem_span_pow_succ {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) (hr : ↑r + 1 = n) (f : R) (m : ℕ) (hf : ordElem f = ↑m) : (algebraMap R ↥(chartRing x r)) f ∉ Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)} ^ (m + 1)

For f of order exactly m, f = x_rᵐ (∑ c_α y^α + x_r (…)) in R' lies in (x_r)ᵐ but not in (x_r)^{m+1}: modulo x_r the bracket is the nonzero polynomial ∑ c̄_α y^α. This is the maximality of the exponent k in f^* = h^k f^s in the definition of the strict transform of an ideal in [Hau14, §6] (following Definition 6.2).

theorem IsLocalRing.ordAlong_span_algebraMap_x_map {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) (hr : ↑r + 1 = n) (I : Ideal R) : ordAlong (Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)}) (Ideal.map (algebraMap R ↥(chartRing x r)) I) = ord I

The order along the exceptional divisor equals the order at the centre (the remark following [Kol07, Definition 47]; [Hau14, §6], following Definition 6.2), local form: the order of I R' along the prime (x_r), that is, in the discrete valuation ring R'_{(x_r)}, the local ring of the blow-up at the generic point of the exceptional divisor, is the order of I.