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

For a marked ideal (I, m) with m ≤ ord_Z I on a smooth variety X with a smooth centre Z, the birational transform is π⁻¹_*(I, m) := (O_{B_Z X}(mF) · π^* I, m) Kol07, Definition 60, (60.1); in local coordinates x₁, …, xₙ with Z = (x₁ = ⋯ = x_r = 0) and the chart yᵢ = xᵢ/x_r (i < r), y_r = x_r, it is computed as π⁻¹_*(f, m) := (y_r^{-m} f(y₁ y_r, …, y_{r-1} y_r, y_r, …, yₙ), m) [Kol07, Definition 60, (60.3)].

In the local model of Hironaka/Algebra/Local/ChartRing.lean: R is a commutative ring with a family x : Fin n → R and a distinguished index r : Fin n (Kollár's r, zero-based), the centre is P = chartCenter x r = ⟨x₀, …, x_r⟩, the chart ring is R' = chartRing x r ⊆ R[1/x_r] and φ = algebraMap R R'. This file defines

• chartCenter x r, the ideal P of the centre;
• f ∈ P^m ⟹ φ f ∈ (x_r R')^m (algebraMap_mem_span_pow_of_mem_chartCenter_pow), because φ (xᵢ) = x_r · yᵢ for i < r and φ (x_r) = x_r, so P ≤ φ⁻¹(x_r R') and P^m ≤ φ⁻¹((x_r R')^m) (Ideal.le_comap_pow); in particular P R' = x_r R' (map_chartCenter), the ideal of the exceptional divisor in the chart;
• the transform of a marked element, transformElem x r f hf := f / x_r^m (an element of R[1/x_r], which lies in R' by the preceding item), and the transform of an ideal, transformIdeal x r I m := ⟨{g ∈ R' | ∃ f ∈ I, x_r^m g = φ f}⟩ = {x_r^{-m} φ(f) : f ∈ I} R'.

The transform of an ideal is defined without the hypothesis I ≤ P^m; the hypothesis is where Kollár defines it and where its properties hold (Hironaka/Algebra/Local/Transform.lean). Uniqueness of the quotient x_r^{-m} φ(f) needs no domain hypothesis: x_r is a unit of the ambient ring R[1/x_r], so multiplication by x_r^m is injective on R'.

noncomputable def IsLocalRing.chartCenter {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) : Ideal R

The ideal P = ⟨x₀, …, x_r⟩ of the centre Z = (x₁ = ⋯ = x_r = 0) of [Kol07, Definition 60] (zero-based indices, r included).

Equations

• IsLocalRing.chartCenter x r = Ideal.span (x '' {i : Fin n | i ≤ r})

theorem IsLocalRing.x_mem_chartCenter {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {i : Fin n} (hi : i ≤ r) : x i ∈ chartCenter x r

theorem IsLocalRing.chartCenter_le_iff {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {I : Ideal R} : chartCenter x r ≤ I ↔ ∀ i ≤ r, x i ∈ I

theorem IsLocalRing.algebraMap_x_eq_mul_chartYR {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {i : Fin n} (hi : i < r) : (algebraMap R ↥(chartRing x r)) (x i) = (algebraMap R ↥(chartRing x r)) (x r) * chartYR x r i

φ (xᵢ) = x_r · yᵢ in R' for i < r.

theorem IsLocalRing.algebraMap_x_mem_span_of_le {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {i : Fin n} (hi : i ≤ r) : (algebraMap R ↥(chartRing x r)) (x i) ∈ Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)}

For i ≤ r, φ (xᵢ) ∈ x_r R'.

theorem IsLocalRing.chartCenter_le_comap_span {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) : chartCenter x r ≤ Ideal.comap (algebraMap R ↥(chartRing x r)) (Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)})

P ≤ φ⁻¹(x_r R').

theorem IsLocalRing.algebraMap_mem_span_pow_of_mem_chartCenter_pow {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)) f ∈ Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)} ^ m

f ∈ P^m ⟹ φ f ∈ (x_r R')^m: the pull-back of (I, m) with I ≤ P^m is divisible by the m-th power of the exceptional divisor [Kol07, Definition 60].

theorem IsLocalRing.exists_algebraMap_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)), (algebraMap R ↥(chartRing x r)) (x r) ^ m * g = (algebraMap R ↥(chartRing x r)) f

The quotient x_r^{-m} φ(f) exists in R'.

theorem IsLocalRing.map_chartCenter {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) : Ideal.map (algebraMap R ↥(chartRing x r)) (chartCenter x r) = Ideal.span {(algebraMap R ↥(chartRing x r)) (x r)}

P R' = x_r R', the ideal of the exceptional divisor F of [Kol07, Definition 60] in the chart.

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

The transform x_r^{-m} φ(f) of a marked element (f, m) with f ∈ P^m Kol07, Definition 60, (60.3), i.e. f / x_r^m in R[1/x_r], which lies in R' by exists_algebraMap_pow_mul_eq.

Equations

• IsLocalRing.transformElem x r f hf = ⟨Localization.mk f ⟨x r ^ m, ⋯⟩, ⋯⟩

theorem IsLocalRing.coe_transformElem {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {m : ℕ} (f : R) (hf : f ∈ chartCenter x r ^ m) : ↑(transformElem x r f hf) = Localization.mk f ⟨x r ^ m, ⋯⟩

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

The transform of an ideal I with mark m [Kol07, Definition 60, (60.1) and (60.3)]: the ideal {x_r^{-m} φ(f) : f ∈ I} R' of R' generated by the quotients that exist; for I ≤ P^m it is the unique ideal J with x_r^m J = I R' (Hironaka/Algebra/Local/Transform.lean).

Equations

• One or more equations did not get rendered due to their size.