Warning 63: the chart-level input

[Kol07, Warning 63]: the birational transform of a marked ideal along a blow-up sequence depends on the sequence, not only on the composite morphism. Kollár's example compares two sequences with the same composite Π = Σ; the discrepancy comes from one chart-level fact: blowing up a centre Z₁ ⊂ E₀' contained in the exceptional divisor E₀' of the first blow-up, the pullback of E₀' picks up the new exceptional divisor (σ₁^* 𝒪(E₀') = 𝒪(E₀' + E₁')), whereas the marked transform π⁻¹_*(𝒪(E₀'), 1) is the strict transform, so Σ⁻¹_*(I, 1) = 𝒪(E₀' + 2E₁') Σ^* I ≠ 𝒪(E₀ + E₁) Π^* I = Π⁻¹_*(I, 1).

Locally (zero-based indices): E₀' = V(x₀), centre Z₁ = V(x₀, x₁) (chartCenter x 1), chart y₀ = x₀/x₁, y₁ = x₁ (dividing by x₁). Then ⟨x₀⟩ R' = ⟨y₀ y₁⟩ (the total transform E₀'' + E₁', map_span_x_zero), while π⁻¹_*(⟨x₀⟩, 1) = ⟨y₀⟩ (the strict transform E₀'', transformIdeal_span_x_zero), and the two ideals differ (transformIdeal_span_x_zero_ne_map): y₁ = x₁ is not a unit of R', lying in the origin ideal of the chart, and R' is a domain. The statement for blow-up sequences, on Kollár's example, is Hironaka/Resolution/Algebraic/Kol07/Warning63.lean; nothing else depends on this module.

theorem Hironaka.Local.fin_zero_lt_one {n : ℕ} : 0 < 1

theorem Hironaka.Local.fin_zero_le_one {n : ℕ} : 0 ≤ 1

theorem Hironaka.Local.chartYR_self {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin (n + 2) → R) (r : Fin (n + 2)) : IsLocalRing.chartYR x r r = (algebraMap R ↥(IsLocalRing.chartRing x r)) (x r)

y₁ = x₁ in the chart dividing by x₁.

theorem Hironaka.Local.map_span_x_zero {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin (n + 2) → R) : Ideal.map (algebraMap R ↥(IsLocalRing.chartRing x 1)) (Ideal.span {x 0}) = Ideal.span {IsLocalRing.chartYR x 1 0 * IsLocalRing.chartYR x 1 1}

Kollár's "σ₁^* 𝒪(E₀') = 𝒪(E₀' + E₁')" ([Kol07, Warning 63]): the pullback of E₀' = V(x₀) to the chart y₀ = x₀/x₁, y₁ = x₁ is ⟨y₀ y₁⟩, the total transform.

theorem Hironaka.Local.transformElem_x_zero {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin (n + 2) → R) : IsLocalRing.transformElem x 1 (x 0) ⋯ = IsLocalRing.chartYR x 1 0

The transform of the element x₀ with mark 1 is y₀.

theorem Hironaka.Local.transformIdeal_span_x_zero {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin (n + 2) → R) : IsLocalRing.transformIdeal x 1 (Ideal.span {x 0}) 1 = Ideal.span {IsLocalRing.chartYR x 1 0}

The marked transform π⁻¹_*(⟨x₀⟩, 1) is ⟨y₀⟩, the strict transform of E₀' ([Kol07, Warning 63]).

theorem Hironaka.Local.transformIdeal_span_x_zero_ne_map {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin (n + 2) → R) [IsRegularLocalRing R] (hx : IsLocalRing.maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑(n + 2) = ringKrullDim R) : IsLocalRing.transformIdeal x 1 (Ideal.span {x 0}) 1 ≠ Ideal.map (algebraMap R ↥(IsLocalRing.chartRing x 1)) (Ideal.span {x 0})

The discrepancy of [Kol07, Warning 63], "Π⁻¹_*(I, 1) ≠ Σ⁻¹_*(I, 1)", at the chart level: for a regular system of parameters, the marked transform of E₀' = V(x₀) is not its pullback, ⟨y₀⟩ ≠ ⟨y₀ y₁⟩, because y₁ = x₁ lies in the origin ideal of the chart and R' is a domain.