The birational transform of a marked ideal in the chart: properties

Kollár defines the birational transform of a marked ideal (I, m) with m ≤ ord_Z I as π⁻¹_*(I, m) = (O(mF) · π^* I, m), computed in the chart yᵢ = xᵢ/x_r (i < r), y_r = x_r by π⁻¹_*(f, m) = y_r^{-m} f(y₁ y_r, …, y_{r-1} y_r, y_r, …, yₙ) Kol07, Definition 60, (60.1) and (60.3). The definitions are in Hironaka/Algebra/Local/BirationalTransform.lean; this file proves their properties: the defining equations and uniqueness, the calculus (products, sums, powers), the independence of the chosen generator of the exceptional ideal, the codimension-one case, and the example π⁻¹_*(x₀² + x₁³, 2) = y₀² + x₁.

The one idea. x_r is a unit of the ambient ring R[1/x_r], so multiplication by x_r^m is injective on the chart ring R' (algebraMap_pow_mul_right_injective). Hence the element g with x_r^m g = φ(f) is unique (eq_transformElem_of_pow_mul_eq) and, for I ≤ P^m, the ideal J with x_r^m J = I R' is unique (eq_of_span_pow_mul_eq); transformIdeal x r I m is that ideal (span_pow_mul_transformIdeal: ⊆ because each generator g has x_r^m g ∈ I R', ⊇ because exists_algebraMap_pow_mul_eq produces the quotient of every φ(f)). Every algebraic law then follows from the corresponding law for I R' and the uniqueness: x_r^{m+m'} (J J') = (x_r^m J)(x_r^{m'} J') = (IR')(I'R') = (II')R' gives multiplicativity, x_r^m (J ⊔ J') = IR' ⊔ I'R' gives additivity, x_r^{mc} J^c = (IR')^c gives powers, x_r · R' = P R' gives π⁻¹_*(P^m, m) = R', and the characterization through P R' = x_r R' is the coordinate independence at the level of ideals. Kollár's "as we change coordinates, the result of π⁻¹_* changes by a unit" [Kol07, Definition 60] is the elementwise half of the latter: if d is any other generator of P R', then d = a x_r with a a unit of R' (again by cancellation), and d^m g = φ(f) forces g = a^{-m} · transformElem f.

Codimension one. For r = 0 no coordinate is divided: the chart ring is Algebra.adjoin R ∅ = ⊥, the image of R, so φ is surjective, and bijective when R is a regular local ring with x a regular system of parameters (Hironaka/Algebra/Local/Chart.lean). Transporting x_r^m J = I R' along the bijection gives x_r^m · φ⁻¹(J) = I — Kollár's remark that for a divisor Z "scheme-theoretically there is no change" but the order along Z drops by m [Kol07, Definition 60].

The example. For n = 2, r = 1, f = x₀² + x₁³: x₁² (y₀² + x₁) = (x₁ y₀)² + x₁³ = φ(f), so π⁻¹_*(f, 2) = y₀² + x₁ by uniqueness. It lies in 𝔪' = ⟨y₀, x₁⟩. That it is not in 𝔪'² is seen through the ring map ψ : R[1/x₁] → Frac(R/⟨x₀⟩) (as for 1 ∉ 𝔪' in Hironaka/Algebra/Local/Chart.lean): R/⟨x₀⟩ is a regular local ring of dimension one with maximal ideal ⟨x̄₁⟩ (Hironaka/Algebra/Local/RegularSystem.lean), so a domain in which x̄₁ ≠ 0 and x̄₁ ∉ 𝔪̄²; ψ kills y₀ = x₀/x₁, sends R' into R/⟨x₀⟩ and 𝔪' into 𝔪̄, hence 𝔪'² into 𝔪̄², while ψ(y₀² + x₁) = x̄₁. The order in the local ring R'_{𝔪'} is then 1, because 𝔪'^k R'_{𝔪'} ∩ R' = 𝔪'^k (𝔪'^k is 𝔪'-primary, 𝔪' maximal; mem_pow_of_algebraMap_mem_map_pow).

Cancellation of x_r and the defining equations

theorem IsLocalRing.algebraMap_pow_mul_right_injective {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (m : ℕ) : Function.Injective fun (g : ↥(chartRing x r)) => (algebraMap R ↥(chartRing x r)) (x r) ^ m * g

x_r is a unit of R[1/x_r], so multiplication by x_r^m is injective on the chart ring.

theorem IsLocalRing.algebraMap_pow_mul_transformElem {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {m : ℕ} (f : R) (hf : f ∈ chartCenter x r ^ m) : (algebraMap R ↥(chartRing x r)) (x r) ^ m * transformElem x r f hf = (algebraMap R ↥(chartRing x r)) f

x_r^m · π⁻¹_*(f, m) = φ(f) [Kol07, Definition 60, (60.3)].

theorem IsLocalRing.eq_transformElem_of_pow_mul_eq {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {m : ℕ} {f : R} (hf : f ∈ chartCenter x r ^ m) {g : ↥(chartRing x r)} (h : (algebraMap R ↥(chartRing x r)) (x r) ^ m * g = (algebraMap R ↥(chartRing x r)) f) : g = transformElem x r f hf

Uniqueness of the quotient π⁻¹_*(f, m).

theorem IsLocalRing.transformElem_mem_transformIdeal {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {I : Ideal R} {m : ℕ} {f : R} (hfI : f ∈ I) (hf : f ∈ chartCenter x r ^ m) : transformElem x r f hf ∈ transformIdeal x r I m

theorem IsLocalRing.span_pow_mul_transformIdeal {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) : Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)} ^ m * transformIdeal x r I m = Ideal.map (algebraMap R ↥(chartRing x r)) I

For I ≤ P^m, x_r^m · π⁻¹_*(I, m) = I R' [Kol07, Definition 60, (60.1)].

theorem IsLocalRing.eq_of_span_pow_mul_eq {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {m : ℕ} {J J' : Ideal ↥(chartRing x r)} (h : Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)} ^ m * J = Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)} ^ m * J') : J = J'

Cancellation of x_r^m for ideals of the chart ring.

theorem IsLocalRing.eq_transformIdeal_of_span_pow_mul_eq {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) {J : Ideal ↥(chartRing x r)} (hJ : Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)} ^ m * J = Ideal.map (algebraMap R ↥(chartRing x r)) I) : J = transformIdeal x r I m

For I ≤ P^m, π⁻¹_*(I, m) is the unique ideal J with x_r^m J = I R'.

theorem IsLocalRing.transformIdeal_eq_span_range_transformElem {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) : transformIdeal x r I m = Ideal.span (Set.range fun (f : ↥I) => transformElem x r ↑f ⋯)

π⁻¹_*(I, m) = {x_r^{-m} φ(f) : f ∈ I} R'.

The calculus of the transform

theorem IsLocalRing.transformElem_mul {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {m m' : ℕ} {f g : R} (hf : f ∈ chartCenter x r ^ m) (hg : g ∈ chartCenter x r ^ m') (hfg : f * g ∈ chartCenter x r ^ (m + m')) : transformElem x r (f * g) hfg = transformElem x r f hf * transformElem x r g hg

π⁻¹_*((f, m)(g, m')) = π⁻¹_*(f, m) π⁻¹_*(g, m').

theorem IsLocalRing.mul_le_chartCenter_pow_add {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {I J : Ideal R} {m m' : ℕ} (hI : I ≤ chartCenter x r ^ m) (hJ : J ≤ chartCenter x r ^ m') : I * J ≤ chartCenter x r ^ (m + m')

theorem IsLocalRing.transformIdeal_mul {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {I J : Ideal R} {m m' : ℕ} (hI : I ≤ chartCenter x r ^ m) (hJ : J ≤ chartCenter x r ^ m') : transformIdeal x r (I * J) (m + m') = transformIdeal x r I m * transformIdeal x r J m'

π⁻¹_*(IJ, m + m') = π⁻¹_*(I, m) π⁻¹_*(J, m') (used silently in the proof of [Kol07, Theorem 100]).

theorem IsLocalRing.transformIdeal_sup {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {I J : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) (hJ : J ≤ chartCenter x r ^ m) : transformIdeal x r (I ⊔ J) m = transformIdeal x r I m ⊔ transformIdeal x r J m

π⁻¹_*(I + J, m) = π⁻¹_*(I, m) + π⁻¹_*(J, m) (used silently in the proof of [Kol07, Theorem 100]).

theorem IsLocalRing.transformIdeal_mono {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {I J : Ideal R} {m : ℕ} (h : I ≤ J) : transformIdeal x r I m ≤ transformIdeal x r J m

Monotonicity of the transform in the ideal.

theorem IsLocalRing.transformIdeal_iSup {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {ι : Sort u_1} {I : ι → Ideal R} {m : ℕ} (hI : ∀ (i : ι), I i ≤ chartCenter x r ^ m) : transformIdeal x r (⨆ (i : ι), I i) m = ⨆ (i : ι), transformIdeal x r (I i) m

Additivity for arbitrary sums.

theorem IsLocalRing.pow_le_chartCenter_pow_mul {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) (c : ℕ) : I ^ c ≤ chartCenter x r ^ (m * c)

theorem IsLocalRing.transformIdeal_pow {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) (c : ℕ) : transformIdeal x r (I ^ c) (m * c) = transformIdeal x r I m ^ c

π⁻¹_*(I^c, mc) = π⁻¹_*(I, m)^c (used silently in the proof of [Kol07, Theorem 100]).

theorem IsLocalRing.transformIdeal_chartCenter {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) : transformIdeal x r (chartCenter x r) 1 = ⊤

π⁻¹_*(P, 1) = R': the transform of the ideal of the centre is the unit ideal.

theorem IsLocalRing.transformIdeal_chartCenter_pow {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (m : ℕ) : transformIdeal x r (chartCenter x r ^ m) m = ⊤

π⁻¹_*(P^m, m) = R'.

Coordinate independence

theorem IsLocalRing.eq_transformIdeal_of_map_chartCenter_pow_mul_eq {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) {J : Ideal ↥(chartRing x r)} (hJ : Ideal.map (algebraMap R ↥(chartRing x r)) (chartCenter x r) ^ m * J = Ideal.map (algebraMap R ↥(chartRing x r)) I) : J = transformIdeal x r I m

π⁻¹_*(I, m) is the unique ideal J with (P R')^m J = I R': the characterization independent of the chosen generator of the exceptional ideal.

theorem IsLocalRing.exists_unit_mul_transformElem {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {m : ℕ} {f : R} (hf : f ∈ chartCenter x r ^ m) {d : ↥(chartRing x r)} (hd : Ideal.span {d} = Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)}) {g : ↥(chartRing x r)} (h : d ^ m * g = (algebraMap R ↥(chartRing x r)) f) : ∃ (v : (↥(chartRing x r))ˣ), g = ↑v * transformElem x r f hf

Dividing by another generator of P R' changes π⁻¹_*(f, m) by a unit of R' (Kollár's "as we change coordinates, the result of π⁻¹_* changes by a unit", [Kol07, Definition 60]).

theorem IsLocalRing.mk_mem_chartRingOf_of_mem_chartCenter {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (d : R) (hd : d = x r) {z : R} (hz : z ∈ chartCenter x r) : Localization.mk z ⟨d, ⋯⟩ ∈ chartRingOf x r d

z / d ∈ chartRingOf x r d for z ∈ P and d = x_r.

theorem IsLocalRing.chartRingOf_eq_of_chartCenter_eq {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (x' : Fin n → R) (hr : x' r = x r) (hP : chartCenter x' r = chartCenter x r) : chartRingOf x' r (x r) = chartRing x r

Another family with the same centre and the same dividing element has the same chart ring.

Codimension-one centre

theorem IsLocalRing.chartCenter_eq_span_singleton_of_val_eq_zero {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (hr : ↑r = 0) : chartCenter x r = Ideal.span {x r}

For r = 0 the centre is ⟨x_r⟩ (the divisorial case of [Kol07, Definition 60]).

theorem IsLocalRing.chartRing_eq_bot_of_val_eq_zero {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (hr : ↑r = 0) : chartRing x r = ⊥

For r = 0 the chart ring is the image of R.

theorem IsLocalRing.algebraMap_chartRing_bijective_of_val_eq_zero {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) [IsRegularLocalRing R] (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (hr : ↑r = 0) : Function.Bijective ⇑(algebraMap R ↥(chartRing x r))

For r = 0, φ : R → R' is bijective ("B_Z X ≅ X", [Kol07, Definition 60]).

theorem IsLocalRing.span_pow_mul_comap_transformIdeal_of_val_eq_zero {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) [IsRegularLocalRing R] (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (hr : ↑r = 0) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) : Ideal.span {x r ^ m} * Ideal.comap (algebraMap R ↥(chartRing x r)) (transformIdeal x r I m) = I

For r = 0, x_r^m · φ⁻¹(π⁻¹_*(I, m)) = I ("π⁻¹_*(I, m) = x_r^{-m} I": the order along a divisorial centre drops by m, [Kol07, Definition 60]).

The example π⁻¹_*(x₀² + x₁³, 2) = y₀² + x₁

theorem IsLocalRing.sq_add_cube_mem_chartCenter_sq {R : Type u} [CommRing R] (x : Fin 2 → R) : x 0 ^ 2 + x 1 ^ 3 ∈ chartCenter x 1 ^ 2

x₀² + x₁³ ∈ P².

theorem IsLocalRing.transformElem_sq_add_cube {R : Type u} [CommRing R] (x : Fin 2 → R) (hf : x 0 ^ 2 + x 1 ^ 3 ∈ chartCenter x 1 ^ 2) : transformElem x 1 (x 0 ^ 2 + x 1 ^ 3) hf = chartYR x 1 0 ^ 2 + (algebraMap R ↥(chartRing x 1)) (x 1)

π⁻¹_*(x₀² + x₁³, 2) = y₀² + x₁.

Contraction of powers of a maximal ideal from the localization

theorem IsLocalRing.mem_pow_of_algebraMap_mem_map_pow {A : Type u_1} [CommRing A] (P : Ideal A) [hP : P.IsMaximal] {k : ℕ} (hk : k ≠ 0) {a : A} (h : (algebraMap A (Localization.AtPrime P)) a ∈ Ideal.map (algebraMap A (Localization.AtPrime P)) (P ^ k)) : a ∈ P ^ k

For P maximal, P^k R_P ∩ R = P^k (P^k is P-primary).

The order of the transform at the origin of the chart, in the example

theorem IsLocalRing.transformElem_sq_add_cube_notMem_chartOrigin_sq {R : Type u} [CommRing R] [IsRegularLocalRing R] (x : Fin 2 → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑2 = ringKrullDim R) (hf : x 0 ^ 2 + x 1 ^ 3 ∈ chartCenter x 1 ^ 2) : transformElem x 1 (x 0 ^ 2 + x 1 ^ 3) hf ∉ chartOrigin x 1 ^ 2

The key point of the example: y₀² + x₁ ∉ 𝔪'². Proof: the ring map ψ : R[1/x₁] → Frac(R/⟨x₀⟩) kills y₀, maps R' into R/⟨x₀⟩ and 𝔪' into its maximal ideal 𝔪̄, hence 𝔪'² into 𝔪̄²; but ψ(y₀² + x₁) = x̄₁ ∉ 𝔪̄², since R/⟨x₀⟩ is regular of dimension one with x̄₁ a regular system of parameters (Hironaka/Algebra/Local/RegularSystem.lean).

theorem IsLocalRing.transformElem_sq_add_cube_mem_chartOrigin {R : Type u} [CommRing R] [IsRegularLocalRing R] (x : Fin 2 → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑2 = ringKrullDim R) (hf : x 0 ^ 2 + x 1 ^ 3 ∈ chartCenter x 1 ^ 2) : transformElem x 1 (x 0 ^ 2 + x 1 ^ 3) hf ∈ chartOrigin x 1 ∧ transformElem x 1 (x 0 ^ 2 + x 1 ^ 3) hf ∉ chartOrigin x 1 ^ 2

y₀² + x₁ ∈ 𝔪' ∖ 𝔪'².

theorem IsLocalRing.ordElem_transformElem_sq_add_cube {R : Type u} [CommRing R] [IsRegularLocalRing R] (x : Fin 2 → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑2 = ringKrullDim R) (hf : x 0 ^ 2 + x 1 ^ 3 ∈ chartCenter x 1 ^ 2) [(chartOrigin x 1).IsPrime] : ordElem ((algebraMap (↥(chartRing x 1)) (Localization.AtPrime (chartOrigin x 1))) (transformElem x 1 (x 0 ^ 2 + x 1 ^ 3) hf)) = 1

The transform y₀² + x₁ has order 1 at the origin of the chart.

theorem IsLocalRing.transformElem_X_sq_add_X_cube (hf : MvPowerSeries.X 0 ^ 2 + MvPowerSeries.X 1 ^ 3 ∈ chartCenter MvPowerSeries.X 1 ^ 2) : transformElem MvPowerSeries.X 1 (MvPowerSeries.X 0 ^ 2 + MvPowerSeries.X 1 ^ 3) hf = chartYR MvPowerSeries.X 1 0 ^ 2 + (algebraMap (MvPowerSeries (Fin 2) ℚ) ↥(chartRing MvPowerSeries.X 1)) (MvPowerSeries.X 1)

In ℚ⟦x₀, x₁⟧, π⁻¹_*(x₀² + x₁³, 2) = y₀² + x₁.

instance IsLocalRing.chartOrigin_X_one_isPrime : (chartOrigin MvPowerSeries.X 1).IsPrime

theorem IsLocalRing.ordElem_transformElem_X_sq_add_X_cube (hf : MvPowerSeries.X 0 ^ 2 + MvPowerSeries.X 1 ^ 3 ∈ chartCenter MvPowerSeries.X 1 ^ 2) : ordElem ((algebraMap (↥(chartRing MvPowerSeries.X 1)) (Localization.AtPrime (chartOrigin MvPowerSeries.X 1))) (transformElem MvPowerSeries.X 1 (MvPowerSeries.X 0 ^ 2 + MvPowerSeries.X 1 ^ 3) hf)) = 1

In ℚ⟦x₀, x₁⟧ the transform has order 1 at the origin of the chart.