The ideals and divisors induced along a blow-up sequence #
[Kol07, Definition 66] attaches to a smooth blow-up sequence S starting with a triple (X, I, E)
the induced data (X_i, I_i, E_i): X_i = S.stage i, I_i = S.weakTransformSeq I i (the
unmarked birational transforms of condition (1)) or S.markedTransformSeq I m i (the marked ones
of condition (1′), [Kol07, Warning 63]), and E_i = S.totalTransformSeq E i. This module proves
their recursion equations, the description of the marked transform as a colon ideal, the recursion
of the order predicates, and the nonvanishing of the induced ideals on the components of the
stages.
The recursion. The three sequences are defined by the same structural recursion on the list
of centers: at nil X everything is the initial datum; on cons X D rest the index 0 returns
the initial datum and the index j + 1 recurses into the tail with the datum transformed once
along the first blow-up (weakTransform D, markedTransform D · m,
DivisorFamily.totalTransform · D). So the equations on the constructor shapes are rfl.
Kollár's formula on a variable sequence, I_{i+1} = (π_i)_*^{-1} I_i, needs the stage-i+1
data expressed through π_i = S.step i and F_{i+1} = S.exceptionalAt i, whose types are the
stages; it is proved by induction on the sequence with the index in the form ⟨j, h⟩, and at
index 0 on the cons shape by a case split on the tail's constructor, after which the cast
eqToHom (stage_zero rest) in step_cons_zero is eqToHom rfl = 𝟙 and the two sides agree
definitionally (the total transform along a morphism DivisorFamily.totalTransformAlong being
the shape of the recursion step).
The marked transform. markedTransform Z I m = (π^* I : F^m) is Kollár's 𝒪(mF) · π^* I
[Kol07, Definition 60]: when F^m divides π^* I, F^m · (π^* I : F^m) = π^* I, and this
determines the quotient because F is invertible (blowUp.isInvertible_comap_π).
The order predicates. IsOrderSeq and IsOrderGeSeq are ∀ i over the recursions together
with IsSmooth; their recursion on the cons shape is read off index by index, exactly as
isSmooth_cons_iff is proved in Hironaka/Scheme/BlowUpSequence/Basic.lean.
Nonvanishing on components. IsNonzeroEverywhere (nonzero stalks) is Kollár's "nonzero on
every irreducible component" [Kol07, Notation 64 (2)]: a stalk vanishes at a point only if it
vanishes at the generic point of a component through it. Along a smooth blow-up sequence of order
m (or ≥ m) the induced ideals stay nonzero on every component, and for m ≥ 1 no center
contains a component of its stage.
π_0 on the cons shape with a constructor-shaped tail: no cast #
π_0 = D.blowUpπ on cons X D (nil _) (the cast of step_cons_zero is eqToHom rfl).
π_0 = D.blowUpπ on cons X D (cons _ D' rest').
On the cons shape the first exceptional divisor is D.exceptionalDivisor carried along the
cast X_1 = D.blowUp; it is not rfl on a variable tail.
The recursion equations of the induced data #
I_{j+1} = (π_j)_*^{-1} I_j [Kol07, Definition 66 (1)], in the ⟨j, h⟩ form of the indices:
by induction on the sequence, the first step being a case split on the tail's constructor.
(I_{j+1}, m) = (π_j)_*^{-1}(I_j, m) [Kol07, Warning 63 (2) and Definition 66 (1′)], in the
⟨j, h⟩ form of the indices.
E_{j+1} = (π_j)_tot^{-1} E_j [Kol07, Definition 66 (1)], in the ⟨j, h⟩ form of the
indices.
I_{i+1} = (π_i)_*^{-1} I_i [Kol07, Definition 66 (1)].
(I_{i+1}, m) = (π_i)_*^{-1}(I_i, m) [Kol07, Warning 63 (2) and Definition 66 (1′)].
E_{i+1} = (π_i)_tot^{-1} E_i [Kol07, Definition 66 (1)].
The total transform along a morphism #
The exceptional divisor receives the largest index ("added as the last divisor", [Kol07, Definition 65]).
The marked transform as a colon ideal #
F^m · π_*^{-1}(I, m) = π^* I when F^m ∣ π^* I [Kol07, Definition 60].
𝒪(mF) · π^* I is the unique K with F^m · K = π^* I [Kol07, Definition 60].
Transport of the marked transform along an equality of centers e : I = J: the eqToHom of
eqToHom_comp_blowUpπ (Hironaka/Scheme/BlowUp/BlowUpMap.lean) pulls markedTransform J K m back
to markedTransform I K m.
The order predicates #
[Kol07, Definition 66] unrolled on the cons shape: the first blow-up is a smooth blow-up of
order m of (X, I, E) [Kol07, Definition 65], and the tail is a sequence of order m for the
transformed triple.
The marked form of [Kol07, Definition 66] unrolled on the cons shape.
Nonzero stalks and nonzero on every irreducible component #
IsNonzeroEverywhere I iff I is nonzero at the generic point of every irreducible
component: the condition "nonzero on every irreducible component" of [Kol07, Notation 64 (2)].
One blow-up: nonvanishing on the components is preserved #
The unmarked birational transform of an ideal sheaf nonzero on every component is nonzero on
every component of B_Z X (stalkIdeal_controlledTransform_ne_bot, the weak transform being a
controlled transform); the condition of [Kol07, Notation 64 (2)] is preserved.
The marked transform π_*^{-1}(I, m) of an ideal sheaf nonzero on every component is nonzero
on every component of B_Z X (compare the remark after [Kol07, Lemma 62]). The order hypothesis
_hm is present because π_*^{-1}(I, m) is the marked transform of [Kol07, Definition 60] only
under m ≤ ord_Z I, the clause that a sequence of order ≥ m supplies at every stage; the proof
does not need it, because the colon (π^* I : F^m) has nonzero stalks for every m
(stalkIdeal_controlledTransform_ne_bot: over the center by injectivity of π^♯, off it because
π is an isomorphism there).
The stages of a smooth blow-up sequence are smooth (Kollár Notation 19 along the sequence) #
[Kol07, Notation 19] along a sequence, for centers of any shape: if X is smooth of relative
dimension n and every center is smooth over k (IsSmooth), every stage is smooth of relative
dimension n, by smoothOfRelativeDimension_blowUpπ_comp_of_smooth at every stage.
(Hironaka/Scheme/BlowUpSequence/Basic.lean states this for centers of pure codimension; condition
(2) of [Kol07, Definition 66] needs it for IsSmooth.)
[Kol07, Notation 19] along a sequence: every stage is smooth over k.
Nonvanishing along a sequence #
Along a smooth blow-up sequence of order m starting with (X, I, E), every induced ideal is
nonzero on every irreducible component of its stage.
Along a smooth blow-up sequence of order ≥ m starting with (X, I, m, E), every induced
marked ideal is nonzero on every irreducible component of its stage.
No center of a smooth blow-up sequence of order ≥ m ≥ 1 starting with (X, I, m, E)
contains an irreducible component of its stage (compare the remark after [Kol07, Lemma 62]): at a
generic point of a component the stalk of the induced ideal is a nonzero ideal of a field, so its
order there is 0 < m.
The unmarked form: no center of a smooth blow-up sequence of order m ≥ 1 starting with
(X, I, E) contains an irreducible component of its stage.