The strict transform of a smooth hypersurface is a smooth hypersurface #
Under the chart-form hypothesis that the smooth hypersurface H is a coordinate hyperplane of a
chart adapted to the centre Y at every point of H ∩ Y (the form in which simple normal
crossings charts present the boundary), the strict transform H' = closure (π⁻¹(H ∖ Y)) is a
closed submanifold of codimension one of the blow-up
(isClosedSubmanifold_strictTransform_of_charts): [BM97, §3, "The strict transform"], and the
local computation in the proof of [Kol07, Theorem 88]. At a point of H' over the centre, a
blow-up chart of index i over the adapted chart is adapted to H' with the single coordinate
u_k (centre index k ≠ i; strictTransform_inter_source_of_ne) or w_j (off-centre index,
strictTransform_inter_source_off); the chart of index k is excluded because H' misses it
(strictTransform_inter_source_self). Off the exceptional divisor, π is a local diffeomorphism
(IsBlowUp.isLocalDiffeomorphOn_compl) and H' = π⁻¹(H) there (the set forms of
Hironaka.Manifold.BlowUp.Transform.Strict), so an adapted chart of H transports along the
local inverse (transportChart, isAdaptedChart_transportChart) and is restricted to π⁻¹(Yᶜ).
For Y ⊆ H the chart-form hypothesis is supplied by the pair-chart lemma
exists_adaptedChart_pair: at a ∈ Y, a defining function h of H vanishes on Y, so
h = ∑_k g_k z_k near a in the centre coordinates z_k of an adapted chart; its differential
dh(a) = ∑_k g_k(a) dz_k(a) is nonzero (h is a chart coordinate of H), so some
g_{k₀}(a) ≠ 0, the family z with z_{k₀} replaced by h has independent differentials, and
the chart completion exists_chart_extending (through exists_adaptedChart_zeroSet') completes
it to a chart; where g_{k₀} ≠ 0 its zero set is Y and H = {h = 0}: the pair chart. Hence
isClosedSubmanifold_strictTransform.
Codimension-s forms: for a closed submanifold S ⊇ Y of codimension s, the strict transform
S' is a closed submanifold of M' of codimension s (IsClosedSubmanifold.strictTransform;
the identification of the blow-up of S along Y with the birational transform of S is
[Kol07, Definition 30, 30.2]), over the centre by the flag chart (exists_adaptedChart_flag of
Hironaka.Manifold.BlowUp.Transform.StrictFlag, of which the pair lemma is the case s = 1)
and the chart lemmas in flag coordinates, off the centre by the transport
exists_adaptedChart_strictTransform_off'; the hypersurface statements are its instances.
A chart in which a set is the zero set of one coordinate is adapted to the set, with the single index.
In codimension s: off the exceptional divisor the strict
transform of S is π⁻¹(S), and an adapted chart of S at π p transports along the local
inverse of π to an adapted chart of S' at p with the coordinates z ∘ π; the hypersurface
form is exists_adaptedChart_strictTransform_off.
Off the exceptional divisor the strict transform is π⁻¹(H), and an adapted
chart of H at π p transports along the local inverse of π to an adapted chart of H' at p
whose coordinate is h ∘ π, h the coordinate of the chart of H.
If the smooth
hypersurface H is a coordinate hyperplane of an adapted chart of Y at every point of H ∩ Y,
its
strict transform is a smooth hypersurface of M'.
At a point of a closed
submanifold Y contained in a smooth hypersurface H, there is a chart adapted to Y in which H
is a coordinate hyperplane — replace one centre coordinate by a defining function of H and
complete the coordinates (exists_chart_extending); the case s = 1 of the flag lemma
exists_adaptedChart_flag (StrictFlag.lean).
For a blowing-up π of M along a
closed submanifold Y ⊆ S, the strict transform of S is a closed submanifold of M' of the
codimension of S — over the centre by the flag chart, cover and the chart lemmas, off the centre
by the transport exists_adaptedChart_strictTransform_off'.
The strict transform of a smooth
hypersurface containing the centre is a smooth hypersurface of M'.