The chart of a point of the exceptional divisor #
[Hau14, Proposition 5.4 (5)–(7)] at a point a' of the exceptional divisor F over a, in
coordinates z at a with I_{Z,a} = (z_l : l ∈ s), stated on the stalk 𝒪_{B,a'} through
π^* : 𝒪_{X,a} → 𝒪_{B,a'} as in Hironaka.Scheme.Snc.TotalTransformOnCentre.
(5), the chart index. The exceptional ideal at a' is F_{a'} = I_{Z,a} · 𝒪_{B,a'}, generated
by the π^* z_l, l ∈ s; it is principal and nonzero (F_{a'} = (z'_j) for a regular system of
parameters z' at a', TotalTransformData). In a local domain a nonzero principal ideal
generated by finitely many elements is generated by one of them
(exists_span_singleton_eq_of_span_range_eq: writing e = ∑ c_l g_l and g_l = d_l e gives
∑ c_l d_l = 1, so some c_l d_l is a unit and (g_l) = (e)). Hence F_{a'} = (π^* z_j) for some
j ∈ s — "a' lies in the x_j-chart" — and every π^* z_l, l ∈ s, is a multiple
y_l · π^* z_j (exists_chart_index): Hauser's chart expression x_l ↦ x_l x_j. Where a' lies
on the strict transform of a component E^i = (z_c = 0) through Z, the chart index is not c
(ne_of_mem_support_strictTransformAlong): this is the clause on the strict transform of V in
[Hau14, Proposition 5.4 (9)].
(6)–(7), the strict transforms in the induced coordinates. For a component E^i = (z_c = 0)
containing Z near a (c ∈ s) with π^* z_c = y · π^* z_j, the chart computation gives
π^* z_c = u · π^* z_j with the strict transform of E^i equal to (u) at a'; cancelling the
nonzero π^* z_j in the domain 𝒪_{B,a'} gives u = y, so the strict transform is (y)
(stalkIdeal_strictTransformAlong_eq_span_of_eq_mul; Hauser's (7) for V = (z_{n-k+1} = 0)) and it
passes through a' exactly when y ∈ 𝔪_{a'} — the entry of a' at the coordinate y is zero
(mem_maximalIdeal_iff_mem_support_strictTransformAlong; Hauser's (6)).
Sources: [Hau14, Proposition 5.4 (5)–(7); Definition 6.2], [Hau03, Appendix C (5), (7) and its proof], [Kol07, Definition 60].
In a local domain, a nonzero principal ideal generated by finitely many elements is generated by one of them.
The clause on the strict transform: where x' lies on the strict transform of a component
E^i = (z_c = 0), the chart index j (with F_{x'} = (π^* z_j)) is not c.
The exceptional ideal at a point x' of the exceptional divisor is nonzero: it is generated by
a member of a regular system of parameters (TotalTransformData).
[Hau14, Proposition 5.4 (5)]: a point x' of the exceptional divisor over x lies in the chart
of one of the coordinates z_j, j ∈ s, cutting out the centre — F_{x'} = (π^* z_j) — and there
every π^* z_l, l ∈ s, is a multiple of π^* z_j: the chart expression x_l ↦ x_l x_j of the
blow-up.
[Hau14, Proposition 5.4 (7)]: for a component E^i = (z_c = 0) containing Z near x
(c ∈ s), in the chart of z_j with π^* z_c = y · π^* z_j, the strict transform of E^i at x'
is (y) — for V = (z_{n-k+1} = 0), "V^s is given in the induced coordinates by
x_{n-k+1} = 0".
[Hau14, Proposition 5.4 (6)]: the entry y of x' at the coordinate of a component
E^i = (z_c = 0) containing Z near x (π^* z_c = y · π^* z_j) vanishes at x' exactly when
the strict transform of E^i passes through x'.