The total transform of an snc divisor under a smooth blow-up #
[Hau14, Proposition 5.3]: the total transform π^{-1}_{tot}(E) = (π_*^{-1} E^i, F)
[Kol07, Definition 25] of a simple normal crossing family E under the blow-up π : B_Z X → X
along a centre Z having simple normal crossings with E is again a simple normal crossing family
(totalTransform_isSnc), and each of its members — the strict transform of a component, the
exceptional divisor — is a smooth divisor (isSmoothDivisor_strictTransform,
isSmoothDivisor_exceptionalDivisor). The proof assembles the three statements of
Hironaka.Scheme.Snc.TotalTransformChartComputation: IsSnc is the regularity of every member (the
regular half of the smooth-divisor statement) together with the pointwise conditions of
[Kol07, Definition 24], obtained by cases on x' ∈ F — Hauser's "computation in local coordinates
for which the blow-up is monomial" at the points of F, and the local isomorphism off F. This is
the theorem that keeps the boundary of a blow-up sequence snc (Hironaka.Sequence;
Hironaka.Resolution.Algebraic.Monomial.Geometric.Realize).
The first section records what is definitional: the members and the order of E.totalTransform Z
(totalTransform_component_inl, totalTransform_component_inr, totalTransform_linearOrder).
The trivial blow-up ([Kol07, Definition 65]: "If π is a trivial blow-up, then
π⁻¹_{tot}(E) = E + Z"). For a trivial blow-up the centre Z is a Cartier divisor and
π : B_Z X ⟶ X is an isomorphism (the universal property applied to 𝟙_X), so the strict transform
of a component D = E^i is the inverse image along π of the saturation D.saturate Z computed on
X, and everything is read on stalks (Hironaka.Scheme.Snc.TrivialTotalTransform). At a point x ∈ Z ∩ D the snc data ([Kol07, Definition 24 (4)]) give a regular system of parameters z with D_x = (z_c) and Z_x = (z_l : l ∈ s); since Z_x is principal, generated by a nonzerodivisor, s = {j}. If c ≠ j — the component is transversal to Z — the prime (z_c) is unchanged by the colon
with powers of (z_j), so the saturation is D and the strict transform is D carried along π
(strictTransform_eq_comap_of_isInvertible). If c = j the component coincides with Z near x
and its saturation has stalk (1) there: it dies, as [Hau14, Definition 6.2] says of the centre
itself. The total transform is snc: every member is regular (a transversal component keeps its
stalks, the exceptional divisor is Z carried along π, and regularity transports along π), and
at x' = π⁻¹(x) the coordinates π♯ z are a regular system of parameters for which the surviving
old components keep their coordinates z_{c(i)} and F takes z_j, a coordinate no surviving
component uses (totalTransform_isSnc_of_isInvertible; Hironaka.Scheme.Snc.TrivialSncData).
The members of the total transform #
The member of the total transform at an old index is the strict transform of that component.
The last member of the total transform is the exceptional divisor [Kol07, Definition 25].
The order of the total transform: the old members in their order, the exceptional divisor last.
The total transform is snc #
[Hau14, Proposition 5.3]: the total transform of a simple normal crossing family E under the
blow-up along a centre Z having simple normal crossings with E is a simple normal crossing
family — Kollár's conditions (1)–(3) at the points of the exceptional divisor
(exists_isSncAt_totalTransform_of_mem_support) and off it
(exists_isSncAt_totalTransform_of_notMem_support), and every member a smooth divisor, hence
regular (isSmoothDivisor_totalTransform_component), all of
Hironaka.Scheme.Snc.TotalTransformChartComputation.
The strict transform of a component of a simple normal crossing family under a blow-up along a
centre having simple normal crossings with it is a smooth divisor
(isSmoothDivisor_totalTransform_component at an old index).
The exceptional divisor of the blow-up along a centre having simple normal crossings with a
simple normal crossing family is a smooth divisor (isSmoothDivisor_totalTransform_component at the
index of F).
The trivial blow-up #
The snc data of a component and the centre at a point of both ([Kol07, Definition 24 (4)]), in
the form of AlgebraicGeometry.SncDataAt.
Under a trivial blow-up, the strict transform of a component E^i that contains the centre near
no point of Z ∩ E^i is E^i carried along the isomorphism π: its saturation along Z is
itself.
The total transform of a simple normal crossing family under a trivial blow-up along a centre
having simple normal crossings with it is a simple normal crossing family — Kollár's
π⁻¹_{tot}(E) = E + Z [Kol07, Definition 65]; see the module docstring for the argument.