The x_r-saturation of an ideal in the chart ring is generated by the transforms

The algebraic half of Bierstone–Milman's description of the ideal of the strict transform, I_{X'} = ⋃_k (I_{π⁻¹(X)} : y_exc^k) [BM97, Proposition 3.13]: in the chart ring R' = R[x_i/x_r : i < r] ⊆ R[1/x_r] of Kollár's chart (60.2) [Kol07, Definition 60] (IsLocalRing.chartRing x r), the x_r-saturation ⋃_k (I R' : x_r^k) of the extension of an ideal I ⊆ R is the ideal generated by the transforms x_r^{-m} φ(f) of the elements f ∈ I (transformIdeal x r I m of Hironaka/Algebra/Local/BirationalTransform.lean, all m). The argument is elementary: every element of R' is φ(c)/x_r^M (R' is generated over R by the x_i/x_r), so x_r^k g ∈ I R' gives x_r^{k+M} g = φ(f) with f ∈ I, i.e. g is a transform; conversely a transform g = x_r^{-m} φ(f) satisfies x_r^m g ∈ I R'. This is the Rees-algebra picture of the strict transform of a subscheme under a blow-up ([Kol07, Definition 25]; Hironaka's definition through the monoidal transformation of the ambient space, [Hir64, Chapter 0, §2]). The analytic statement follows by transporting this along the chart-ring homomorphism into the stalk 𝒪_{M',a'} in Hironaka/Manifold/BlowUp/Transform/StrictSubspaceProp313.lean.

theorem IsLocalRing.exists_pow_mul_eq_algebraMap {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (g : ↥(chartRing x r)) : ∃ (M : ℕ) (c : R), (algebraMap R ↥(chartRing x r)) (x r) ^ M * g = (algebraMap R ↥(chartRing x r)) c

Every element of the chart ring is a quotient φ(c)/x_r^M: the generators x_i/x_r are, and sums and products of such quotients are (the Rees-algebra form of the chart ring of [Kol07, Definition 60, (60.2)]).

def IsLocalRing.IsTransformOf {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (I : Ideal R) (g : ↥(chartRing x r)) : Prop

The transforms of the elements of I: the g ∈ R' with x_r^M g = φ(f) for some f ∈ I.

Equations

• IsLocalRing.IsTransformOf x r I g = ∃ (M : ℕ), ∃ f ∈ I, (algebraMap R ↥(IsLocalRing.chartRing x r)) (x r) ^ M * g = (algebraMap R ↥(IsLocalRing.chartRing x r)) f

theorem IsLocalRing.IsTransformOf.zero {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (I : Ideal R) : IsTransformOf x r I 0

theorem IsLocalRing.IsTransformOf.add {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (I : Ideal R) {g₁ g₂ : ↥(chartRing x r)} (h₁ : IsTransformOf x r I g₁) (h₂ : IsTransformOf x r I g₂) : IsTransformOf x r I (g₁ + g₂)

theorem IsLocalRing.IsTransformOf.mul {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (I : Ideal R) (a : ↥(chartRing x r)) {g : ↥(chartRing x r)} (h : IsTransformOf x r I g) : IsTransformOf x r I (a * g)

theorem IsLocalRing.IsTransformOf.of_pow_mul {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (I : Ideal R) {k : ℕ} {g : ↥(chartRing x r)} (h : IsTransformOf x r I ((algebraMap R ↥(chartRing x r)) (x r) ^ k * g)) : IsTransformOf x r I g

A transform is saturated: if x_r^k g is a transform then so is g.

def IsLocalRing.transformsIdeal {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (I : Ideal R) : Ideal ↥(chartRing x r)

The transforms of the elements of I form an ideal of the chart ring.

Equations

• IsLocalRing.transformsIdeal x r I = { carrier := {g : ↥(IsLocalRing.chartRing x r) | IsLocalRing.IsTransformOf x r I g}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem IsLocalRing.mem_transformsIdeal {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (I : Ideal R) {g : ↥(chartRing x r)} : g ∈ transformsIdeal x r I ↔ IsTransformOf x r I g

theorem IsLocalRing.map_le_transformsIdeal {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (I : Ideal R) : Ideal.map (algebraMap R ↥(chartRing x r)) I ≤ transformsIdeal x r I

Every element of I R' is a transform (with M = 0).

theorem IsLocalRing.transformsIdeal_eq_iSup_transformIdeal {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (I : Ideal R) : transformsIdeal x r I = ⨆ (m : ℕ), transformIdeal x r I m

The ideal of transforms is the union of the transformIdeal x r I m of Hironaka/Algebra/Local/BirationalTransform.lean.

theorem IsLocalRing.iSup_colon_pow_map_eq_transformsIdeal {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (I : Ideal R) : ⨆ (k : ℕ), Submodule.colon (Ideal.map (algebraMap R ↥(chartRing x r)) I) ↑(Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)} ^ k) = transformsIdeal x r I

The x_r-saturation of I R' is the ideal of the transforms of the elements of I, ⋃_k (I R' : x_r^k) = {x_r^{-M} φ(f) : f ∈ I}: [BM97, Proposition 3.13] in the chart ring (the strict transform of [Kol07, Definition 25] and the transform (60.1) of [Kol07, Definition 60]).

theorem IsLocalRing.iSup_colon_pow_singleton_map_eq_transformsIdeal {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (I : Ideal R) : ⨆ (k : ℕ), Submodule.colon (Ideal.map (algebraMap R ↥(chartRing x r)) I) {(algebraMap R ↥(chartRing x r)) (x r) ^ k} = transformsIdeal x r I

The saturation theorem with the colons by the elements x_r^k (the form the transport lemma of Hironaka.Algebra.SaturationDescent produces).

theorem IsLocalRing.iSup_colon_pow_map_eq_iSup_transformIdeal {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (I : Ideal R) : ⨆ (k : ℕ), Submodule.colon (Ideal.map (algebraMap R ↥(chartRing x r)) I) ↑(Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)} ^ k) = ⨆ (m : ℕ), transformIdeal x r I m

The saturation in the form of the union of the transformIdeal x r I m.