Simple normal crossings and the order conditions under smooth pullback #
A smooth blow-up sequence B on X pulled back along a smooth morphism h : Y ⟶ X
([Kol07, 30.1 and 34.1]; [Wlo05, Proposition 2.4.2]) has induced data equal to the inverse images
of the induced data of B (Hironaka/Scheme/BlowUpSequence/PullbackInduced.lean). This module
transports the conditions of [Kol07, Definition 66] along h:
- simple normal crossings [Kol07, Definition 24]: a regular system of parameters at
h yextends along the stalk map to one aty(Hironaka/Scheme/BlowUpSequence/SmoothParameters.lean), and the components ofh⁻¹ Ethroughyare the inverse images of the components ofEthroughh y(exists_isSncAt_comap_of_smooth,isSnc_comap_of_smooth,hasSncWith_comap_of_smooth); - the order predicates:
IsOrderSeq.pullbackandIsOrderGeSeq.pullbackcombine the identifications of the induced data with the transport of simple normal crossings and with the invariance of the order along a center under smooth pullback (ordAlongEq_comap_of_smooth).
Kollár deletes the empty blow-ups of the pullback [Kol07, 34.1]; on the predicates used here an
empty center satisfies the order clause vacuously, so the pullback itself is a smooth blow-up
sequence of order m ([Wlo05, Proposition 2.4.2 (2)]), and the form with the empty blow-ups
deleted follows in Hironaka/Scheme/BlowUpSequence/PullbackEraseEmpty.lean.
Simple normal crossings under smooth pullback #
The pointwise statement: simple normal crossing data of E at h y (a regular system of
parameters z with the components through h y among its coordinate hypersurfaces,
[Kol07, Definition 24]) transport to such data of h⁻¹ E at y: z extends along the stalk map
to a regular system of parameters w (exists_isRegularSystemOfParameters_stalkMap), the
components of h⁻¹ E through y are the inverse images of the components of E through h y
(support_comap), and their stalks are generated by the corresponding w (stalkIdeal_comap).
A simple normal crossing family on a scheme smooth over k pulls back to a simple normal
crossing family along a smooth h [Wlo05, Proposition 2.4.2, proof]. The components' subschemes
are regular because their stalks are the quotients of a regular local ring by a member of a
regular system of parameters.
Simple normal crossings of a closed subscheme with a family [Kol07, Definition 24 (4)] are
preserved by smooth pullback: the coordinates of Z at h y map to coordinates of h⁻¹ Z at
y ("C'_i has simple normal crossings with E'_i", [Wlo05, Proposition 2.4.2, proof]).
The order predicates under smooth pullback #
IsOrderSeq.pullback for a smooth h with equidimensional source: the relative dimension n'
of h ≫ f replaces a relative dimension of h, the form available when the pulled-back triple is
given.
The pullback of a smooth blow-up sequence of order m for (X, I, E) along a smooth h is a
smooth blow-up sequence of order m for (Y, h^* I, h^{-1} E) ([Wlo05, Proposition 2.4.2];
[Kol07, 34.1]), with no deletion of empty blow-ups: an empty pulled-back center satisfies the order
clause vacuously. Stage by stage: the centers are the inverse images of the centers
(center_pullback), the induced families and ideals the inverse images of the induced families
and ideals (Hironaka/Scheme/BlowUpSequence/PullbackInduced.lean), and simple normal crossings and
the order transport along the smooth stage lifts (hasSncWith_comap_of_smooth,
ordAlongEq_comap_of_smooth).
The marked form for any smooth h: the marked transport needs no relative dimension at
all.
The marked form ≥ m of IsOrderSeq.pullback [Wlo05, Proposition 2.4.2].