The origin of the chart after a linear change of coordinates #
[Hau14, Proposition 5.4 (8)–(9)] ([Hau03, Appendix C (8)–(9)]; the proof of [Kol07, Lemma 61]): for
a point a' of the exceptional divisor over a, in the chart of x_j and rational over
κ(a), the coordinate change x_i ↦ x_i − α_i x_j on the other centre coordinates
(α_i ∈ 𝒪_{X,a} lifting the entries of a') makes a' the origin of the chart and the local
blow-up monomial: the induced coordinates of the new system form a regular system of parameters at
a', with π^* x'_i = w'_i · w'_j (exists_shiftCoords_chartOrigin). The change preserves I_Z
and the coordinate x_p of any hypersurface V = (x_p = 0) through a''s strict transform (its
entry vanishes, so the lift α_p may be taken 0).
The proof lives in Kollár's chart ring (Hironaka.Scheme.Snc.InducedCoordinates): 𝒪_{B,a'} ≅ R'_𝔮
with 𝔮 over 𝔪_a; rationality of a' — the residue map κ(a) → κ(a') bijective — is the
bijectivity of R/𝔪 → R'/𝔮 (bijective_quotientMap_of_residueField), so 𝔮 = 𝔪'_α = chartOriginAt y ρ α for lifts α (exists_eq_chartOriginAt), which can be changed modulo 𝔪
(chartOriginAt_eq_of_sub_mem); chartRingEquivShift and localizationEquivShift of
Hironaka.Algebra.Local.ChartShift identify R'_{𝔪'_α} with the localization of the chart ring of
the shifted coordinates at its origin, whose maximal ideal is generated by the chart functions
(maximalIdeal_localization_chartOrigin), and the chart derivations
(Hironaka.Scheme.Snc.ChartDerivations) show these n generators are a regular system of
parameters (ringKrullDim_eq_of_span_eq_of_derivations).
Hauser's (9) (exists_coordinates_chartOrigin'): if a' lies on the strict transform of
V = (x_{n-k+1} = 0) the chart index is not n − k + 1 and (8) applies, after which the
transposition of the positions j and n makes a' the origin of the x_n-chart; otherwise a'
lies in the chart of x_{n-k+1} itself (the entry of V's coordinate is a unit) and (8) applies
with j = n − k + 1.
Rationality transported to the chart ring: if the residue map of a local homomorphism
π : R → S is bijective and S ≃ R'_𝔮 compatibly with π and R → R' → R'_𝔮, then
R/𝔪 → R'/𝔮 is bijective.
The origin 𝔪'_a of the shifted chart depends only on the lifts a modulo 𝔪.
A family of n generators of the maximal ideal of a regular local ring with dual derivations
is a regular system of parameters: n = dim S.
The induced coordinates at the origin of a chart, abstractly: for y' a regular system of
parameters of R with dual derivations, and S ≃ R'_{𝔪'} (the localization of the chart ring of
y' at the origin of the chart of y'_ρ) compatibly with π : R → S, the chart functions
y'_{σ i} pulled back to S form a regular system of parameters of S, with w'_i = π(y'_{σ i})
for the non-fibre positions and π(y'_{σ i}) = w'_i · w'_{σ⁻¹ ρ} for the fibre positions.
[Hau14, Proposition 5.4 (8)] ([Hau03, Appendix C (8)]; the proof of [Kol07, Lemma 61]): for a'
in the chart of z_j and rational over κ(a), the coordinates z'_i = z_i − α_i z_j (n − k ≤ i,
i ≠ j; z'_i = z_i otherwise) make a' the origin of the chart and the local blow-up monomial:
Z is still cut out by the last k of them, the coordinate z_p of a hypersurface whose induced
entry at a' vanishes is unchanged, and the induced coordinates w' form a regular system of
parameters at a' with π^* z'_i = w'_i w'_j.
[Hau14, Proposition 5.4 (9)] ([Hau03, Appendix C (9)]), with P standing for "a' lies on the
strict transform of V = (z_p = 0)", p = n − k the position of V's coordinate: P excludes the
chart of z_p and the entry of V's coordinate at a' vanishes exactly when P (Hauser's (6)).
For a' rational over κ(a) there are coordinates z'' at a with (1)–(3) in which a' is the
origin of the chart of z''_{j'}, j' = n − 1 when P and j' = p when ¬P, and the local
blow-up is monomial.