The chart ring of the blow-up along the first r coordinates #
Two descriptions of the chart of a blow-up along I = (x_0, …, x_r) at a = x_r coincide. The
affine blow-up algebra R[I/a] = {z/aᵐ : z ∈ Iᵐ} ⊆ R[1/a] (Hauser's local blow-up,
[Hau14, Definition 4.16]) is the ring that glues to the blow-up; Kollár's chart ring
R' = R[x_i/x_r : i < r] ⊆ R[1/x_r] is the ring of the coordinates (60.2) of
[Kol07, Definition 60] (chartRing of Hironaka/Algebra/Local/Chart.lean). They are the same
subalgebra (affineBlowUpAlgebra_span_eq_chartRing): a fraction z/x_rᵐ with z a product of m
generators is a monomial in the x_i/x_r. Through this identification the standard chart of
x_r of B_Z X is the ring map R → R', and the theorems about R' and its origin
𝔪' = (y_1, …, y_n) of Hironaka/Algebra/Local/ChartLocal.lean are statements about the local ring
of B_Z X at the origin of the chart.
At the ring level the file also shows: in adapted coordinates the chart ring of the local blow-up
B_{I_x} Spec 𝒪_{X,x} is chartRing y ρ (affineBlowUpAlgebra_stalkIdeal_eq_chartRing); the
y_i are a regular system of parameters of R'_𝔮 exactly when 𝔮 = 𝔪'
(maximalIdeal_localization_eq_span_iff); and every κ-rational point of the fibre in the chart
is the origin after a linear change of the first r coordinates (exists_eq_chartOriginAt,
chartOriginAt), as in the proof of [Kol07, Lemma 61]: "every preimage of p appears as the
origin after a suitable linear change". Used for the local blow-up
(Hironaka/Scheme/Smooth/LocalBlowUp.lean) and for the order of an ideal along the exceptional
divisor (Hironaka/Scheme/IdealSheaf/Order/ExceptionalOrder.lean).
The affine blow-up algebra R[I/x_r] for I = (x_i : i ≤ r) ([Hau14, Definition 4.16]) is
Kollár's chart ring R' = R[x_i/x_r : i < r] ([Kol07, Definition 60, (60.2)]), as subalgebras of
R[1/x_r].
In adapted coordinates y at x (I_x = (y_0, …, y_{r-1})), the chart ring of y_ρ
(ρ = r − 1) of the local blow-up B_{I_x} Spec 𝒪_{X,x} is the chart ring chartRing y ρ of
Kollár's coordinates (60.2) ([Kol07, Definition 60]).
At a prime 𝔮 of the chart ring R', the chart functions y_i form a regular system of
parameters of R'_𝔮 exactly when 𝔮 is the origin 𝔪' = (y_1, …, y_n) of the chart; the "if" is
maximalIdeal_localization_chartOrigin of Hironaka/Algebra/Local/ChartLocal.lean.
Every κ-rational point of the fibre in the chart of x_r (a prime 𝔮 of R' over 𝔪 with
R/𝔪 → R'/𝔮 bijective) is chartOriginAt x r a for some a: the origin of the chart after the
linear change x_i ↦ x_i − a_i x_r of the first r coordinates. This is the remark in the proof
of [Kol07, Lemma 61] that "every preimage of p appears as the origin after a suitable linear
change", and item (9) of [Hau03, Appendix C].