Adapted coordinates in which the blow-up is monomial #
[Hau14, Proposition 5.4 (1)–(9)] stated on the predicates IsSncAt, HasSncWith,
IsRegularSystemOfParameters and stalkIdeal and on Z.blowUp, Z.exceptionalDivisor and
strictTransform Z D (Z.exceptionalDivisor is Z.comap (IdealSheafData.blowUpπ Z) and
strictTransform Z D is strictTransformAlong (IdealSheafData.blowUpπ Z) (Z.comap π) D by
definition): a smooth X over a perfect field k, an snc family E having simple normal crossings
with the centre Z, a member V = E v containing Z, a point a of Z and a point a' of the
exceptional divisor over a. The proofs are those of the modules of Hironaka.Snc on the unfolded
data, which hasSncWith_data extracts from E.HasSncWith Z:
- (1)–(4):
exists_coordinates_hypersurface_center,exists_sncAt_coordinates_hypersurface_center(Hauser's positions by reindexing the snc data ata,Hironaka.Scheme.Snc.HypersurfaceCoordinates),exists_prod_stalkIdeal_pow_eq_span_monomial',exists_map_prod_stalkIdeal_pow_eq_span_monomial'; - (5)–(7):
exists_chart_index',mem_maximalIdeal_iff_mem_support_strictTransform,stalkIdeal_strictTransform_hypersurface(Hironaka.Scheme.Snc.ChartIndex), with the centre's index sets = {i | n − k ≤ i}as aFinset; - (6), the coordinate content:
exists_isRegularSystemOfParameters_induced'(Hironaka.Scheme.Snc.InducedCoordinates), with the regularity of𝒪_{B,a'}andπ^* z_j ≠ 0from the chart shape of the total transform (Hironaka.Scheme.Snc.TotalTransformSnc); - (8)–(9):
exists_shiftCoords_chartOrigin',exists_coordinates_chartOrigin(Hironaka.Scheme.Snc.ChartOrigin), the rationality hypothesis read as the bijectivity of the residue field map (bijective_of_isIso_residueFieldMap) and the clause on the strict transform ofVthrough (6); - Hauser's setting of closed points over an algebraically closed field:
isIso_residueFieldMap_of_isClosedofHironaka.Scheme.Snc.ClosedPointRationaldischarges the rationality hypothesis.
The primed names are the forms on the predicates of the correspondingly named lemmas of those
modules; each docstring names its original. [Hau14, Example 4.53] (the positive half) is the
example at the end. This module is the statement of Hauser's proposition in the library's
vocabulary and is not used further.
Sources: [Hau14, Proposition 5.4; Example 4.53]; [Hau03, Appendix C]; [Kol07, Definition 24; Definition 60; Lemma 61].
The centre's ideal at π a' in the Finset form of Hironaka.Scheme.Snc.ChartIndex.
π^* z_j ≠ 0: the exceptional ideal at a' is nonzero, being generated by a member of a
regular system of parameters (TotalTransformData).
The rationality hypothesis — a' rational over κ(a) — in the form the chart-origin lemmas
take: the residue field map is bijective.
[Hau14, Proposition 5.4 (1)–(3)] on the predicates: for an snc family E having simple normal
crossings with Z and a member E v containing Z, at every point a of Z there is a regular
system of parameters z with I_{V,a} = (z_{n-k}) and I_{Z,a} = (z_l : l ≥ n − k), 1 ≤ k ≤ n —
exists_hauser_coordinates of Hironaka.Scheme.Snc.HypersurfaceCoordinates on the data of
hasSncWith_data. The hypothesis E.IsSnc is part of Hauser's setting (D a normal crossings
divisor) and is kept so that the statements of this module share his hypotheses; the proof does not
need it, because clauses (1)–(3) use only the snc data of E.HasSncWith Z at a.
exists_coordinates_hypersurface_center keeping the snc coordinates for E: the regular system
of parameters z at a satisfies E.IsSncAt a z as well as I_{V,a} = (z_{n-k}) and
I_{Z,a} = (z_l : l ≥ n − k). The hypothesis E.IsSnc is part of Hauser's setting and is kept so
that the statements of this module share his hypotheses; the proof does not need it, because only
the snc data of E.HasSncWith Z at a enter.
[Hau14, Proposition 5.4 (4)] in 𝒪_{X,a}, on the predicate IsSncAt: the ideal
∏_{i ≠ v} I_{E^i,a}^{m_i} of the divisor D = ∑_{i ≠ v} m_i E^i is generated by a monomial
∏_j z_j^{q_j} with q_{n-k} = 0. This is exists_prod_stalkIdeal_pow_eq_span_monomial of
Hironaka.Scheme.Snc.HypersurfaceCoordinates with the snc data packed into E.IsSncAt a z; the
hypotheses of Hauser's setting (E snc, E.HasSncWith Z, E v ≤ Z, a ∈ Z) are kept so that the
statement reads as clause (4) of his proposition; the proof does not need them, because the clause
is a statement about the stalk at a given E.IsSncAt a z and I_{V,a} = (z_{n-k}).
[Hau14, Proposition 5.4 (4)] as printed, on the predicate IsSncAt: D ∩ V is defined in V
locally at a — in 𝒪_{V,a} = 𝒪_{X,a} ⧸ I_{V,a} — by the image of a monomial ∏_j z_j^{q_j} with
q_{n-k} = 0. This is exists_map_prod_stalkIdeal_pow_eq_span_monomial of
Hironaka.Scheme.Snc.HypersurfaceCoordinates with the snc data packed into E.IsSncAt a z; the
hypotheses of Hauser's setting (E snc, E.HasSncWith Z, E v ≤ Z, a ∈ Z) are kept so that the
statement reads as clause (4) of his proposition; the proof does not need them, because the clause
is a statement about the stalk at a given E.IsSncAt a z and I_{V,a} = (z_{n-k}).
[Hau14, Proposition 5.4 (5)], with the clause on the strict transform of V from (9), on the
predicates and Z.blowUp: a point a' of the exceptional divisor lies in the chart of
some centre coordinate z_j (F_{a'} = (π^* z_j)), every centre coordinate is a multiple of
π^* z_j there, and j ≠ n − k where a' lies on the strict transform of V. This is
exists_chart_index with ne_of_mem_support_strictTransformAlong of
Hironaka.Scheme.Snc.ChartIndex, the centre's index set being {i | n − k ≤ i}.
[Hau14, Proposition 5.4 (6)] on the predicates: the entry y of a' at the coordinate of a
component E^i = (z_c = 0) containing Z (π^* z_c = y · π^* z_j) lies in 𝔪_{a'} exactly when
the strict transform of E^i passes through a' —
mem_maximalIdeal_iff_mem_support_strictTransformAlong of Hironaka.Scheme.Snc.ChartIndex.
[Hau14, Proposition 5.4 (6)], the coordinate content, on the predicates and
Z.blowUp: the induced coordinates w of the z_j-chart vanishing at a' extend to a
regular system of parameters of 𝒪_{B,a'}. This is exists_isRegularSystemOfParameters_induced of
Hironaka.Scheme.Snc.InducedCoordinates, the regularity of 𝒪_{B,a'} and π^* z_j ≠ 0 supplied
from the snc data (isRegularLocalRing_stalk_blowUp', stalkMap_ne_zero).
[Hau14, Proposition 5.4 (7)] on the predicates: in the chart of z_j, j ≠ n − k, with
π^* z_{n-k} = y · π^* z_j, the strict transform of V = E v at a' is (y) —
stalkIdeal_strictTransformAlong_eq_span_of_eq_mul of Hironaka.Scheme.Snc.ChartIndex.
[Hau14, Proposition 5.4 (8)] on the predicates and Z.blowUp: for a' rational over
κ(a) (IsIso of the residue field map) in the chart of z_j, the coordinates
z'_i = z_i − α_i z_j on the other centre coordinates make a' the origin of the chart and the
local blow-up monomial, preserve I_Z, and leave the coordinate of V unchanged where a' lies on
the strict transform of V. This is exists_shiftCoords_chartOrigin of
Hironaka.Scheme.Snc.ChartOrigin, the last clause obtained through (6).
[Hau14, Proposition 5.4 (9)] on the predicates: 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 a' lies on the strict transform of V, j = n − k otherwise — and the local blow-up is
monomial: the induced coordinates w form a regular system of parameters at a' with
π^* z_i = w_i w_j for the other centre coordinates. This assembles (1)–(3) with
exists_coordinates_chartOrigin' of Hironaka.Scheme.Snc.ChartOrigin.