Deleting the empty blow-ups of a pullback, and the pulled-back triple #
Kollár's functoriality for smooth morphisms [Kol07, 34.1] pulls a smooth blow-up sequence
B(X, I, E) back along a smooth h : Y ⟶ X and then deletes every blow-up whose center
h^{-1} Z_i is empty (the empty blow-up convention [Kol07, 32]). The deletion eraseEmpty
carries the tail of an empty blow-up back along the isomorphism blowUpπ X ⊤ [Kol07, Warning 20],
a pullback along an isomorphism; this module shows that the order predicates of
[Kol07, Definition 66] survive it.
The one subtlety is bookkeeping. Kollár's divisor families are sets of divisors, on which the
empty exceptional divisor of an empty blow-up is invisible; a DivisorFamily indexes components,
so the empty blow-up adds an empty component to the induced family. The relation
ExtendsByEmpty E₁ E₂ (E₂ is E₁ with extra empty components) is preserved by inverse images
and total transforms and is invisible to IsSncAt, HasSncWith and hence to the order predicates
(ExtendsByEmpty.isOrderSeq); under the empty blow-up the induced ideal returns to I
(weakTransform_top_left, markedTransform_top_left) and the induced family to E extended by
one empty component (extendsByEmpty_totalTransform_top_comap_inv). IsOrderSeq.eraseEmpty then
follows from IsOrderSeq.pullback (Hironaka/Scheme/BlowUpSequence/PullbackSnc.lean) with d = 0,
and Kollár's conclusion for a general smooth h (isOrderSeq_eraseEmpty_pullback) is the
composite.
The module also defines the pulled-back triple Triple.pullback and marked triple
MarkedTriple.pullback, the triple (Y, h^* I, h^{-1}(E)) of [Kol07, 34.1 and Notation 64], used
in the statement of the functoriality clauses of the blow-up sequence functors; see also
[Wlo05, Proposition 2.4.2].
The empty blow-up #
The exceptional divisor of the empty blow-up is empty (the unit ideal sheaf) [Kol07, Warning 20].
The saturation by the unit ideal sheaf is the identity (colon_top).
The strict transform under the empty blow-up is the total transform.
The strict transform of the empty subscheme is empty.
The marked transform under the empty blow-up is the total transform (colon_top).
The exceptional order with respect to the unit ideal sheaf is 0 (the convention for an
unbounded set of controls, sSup ℕ = 0).
Under the empty blow-up the weak transform is the total transform [Kol07, Warning 20].
Families that differ by empty components #
E₂ extends E₁ by empty components: an injection of index sets carrying the components of
E₁ to those of E₂, every other component of E₂ being the unit ideal sheaf (the empty
divisor). Kollár's divisor families are sets of divisors, on which the empty divisor is invisible;
a DivisorFamily indexes components, so the exceptional divisor of an empty blow-up appears as an
empty component of the induced family, and the order predicates must be shown insensitive to it
(the deletion of empty blow-ups, [Kol07, 32]).
Equations
Instances For
Snc data restrict along an extension by empty components: the components through x are the
same (the unit ideal sheaf has empty support).
Simple normal crossings with a subscheme restrict along an extension by empty components.
Extension by empty components is preserved by inverse image.
Extension by empty components is preserved by the total transform (the strict transform of the
empty subscheme is empty, strictTransform_top_right).
The order condition of [Kol07, Definition 66] is insensitive to empty components of E: by
induction along the sequence with isOrderSeq_cons_iff, ExtendsByEmpty.hasSncWith and
ExtendsByEmpty.totalTransform.
The marked form of ExtendsByEmpty.isOrderSeq.
Under the empty blow-up (an isomorphism, [Kol07, Warning 20]) the total transform of E,
carried back along the inverse, is E extended by the empty exceptional component.
Deleting the empty blow-ups; the surjective forms #
Deleting the empty blow-ups of a smooth blow-up sequence of order m gives a smooth blow-up
sequence of order m for the same triple ([Kol07, 32 and 34.1], read on the order predicate):
each deletion carries the tail back along the isomorphism of the empty blow-up (eraseEmpty), a
pullback along an isomorphism, under which the induced data and the order conditions are
transported (IsOrderSeq.pullback with d = 0; the induced ideal and family return to I and to
E extended by an empty component, weakTransform_top_left,
extendsByEmpty_totalTransform_top_comap_inv).
The marked form of IsOrderSeq.eraseEmpty [Kol07, 32 and 34.1].
The surjective case of [Kol07, 34.1], where no deletion is needed. The surjectivity hypothesis
_hs is present because the first bullet of [Kol07, 34.1] is stated for smooth surjections, the
case in which the pull-back has no empty blow-up to delete; the proof does not need it, because
the pull-back along any smooth morphism is a smooth blow-up sequence of the same order
(IsOrderSeq.pullback), surjectivity mattering only for h^* B to determine B [Kol07, 30.1].
The marked form of the surjective case of [Kol07, 34.1]. As for
IsOrderSeq.pullback_of_surjective, the surjectivity hypothesis _hs is present because the
first bullet of [Kol07, 34.1] is stated for smooth surjections; the proof does not need it
(IsOrderGeSeq.pullback).
For a smooth h with equidimensional source, the pullback with its empty blow-ups deleted is
a smooth blow-up sequence of order m for (Y, h^* I, h^{-1} E); no relative dimension of h is
needed.
The marked form of isOrderSeq_eraseEmpty_pullback_of_equidim.
The functoriality clause of [Kol07, 34.1] for a general smooth h: the sequence obtained from
the pull-back h^* B(X, I, E) "by deleting every blow-up h^* π_i whose center is empty" and
reindexing is a smooth blow-up sequence of order m for (Y, h^* I, h^{-1} E).
The marked form of isOrderSeq_eraseEmpty_pullback [Kol07, 34.1].
The pulled-back triple #
The pullback of a triple along a smooth morphism h : Y ⟶ T.X.left: the triple
(Y, h^* I, h^{-1}(E)) of [Kol07, 34.1], for Y of finite type, quasi-compact, separated and
equidimensional over k as in [Kol07, Notation 64]. Its data are Y, T.I.comap h,
T.E.comap h; nonvanishing on the components is isNonzeroEverywhere_comap_of_flat and simple
normal crossings is isSnc_comap_of_smooth.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pullback of a marked triple along a smooth h, the mark unchanged [Kol07, 34.1].
Instances For
The ambient scheme of the pulled-back triple is Y.
The ideal of the pulled-back triple is h^* I.
The divisor family of the pulled-back triple is h^{-1} E.
The mark of the pulled-back marked triple is the mark of T.
The underlying triple of the pulled-back marked triple is the pulled-back triple.