The going-up theorem for D-balanced ideals #
Kollár's going-up theorem [Kol07, Theorem 84]: for a D-balanced ideal I with max-ord I = m on
a smooth variety X and a smooth hypersurface S ⊆ X, the push-forward to X of a smooth blow-up
sequence of order ≥ m for (S, I|_S, m) is a smooth blow-up sequence of order m for (X, I).
Its proof [Kol07, 90] is by induction on the length: assuming the statement for sequences of
length < r, Corollary 89 for the prefix Π_{r−1} and the D-balanced property give
cosupp(J_{r−1}, m) ⊆ cosupp(I_{r−1}, m), so the last blow-up also has order ≥ m.
This module proves the theorem with the boundary E of [Kol07, Corollary 85] carried along
(IsDBalanced.isOrderSeq_pushforward) and in the printed form at E = ∅
(IsDBalanced.isOrderSeq_pushforward_of_not_subset_cosupp). The induction is run as a strong
induction on the stage index: the clauses at the stages < l make the prefix B.take l a sequence
of order ≥ m (isOrderGeSeq_take_of_forall_lt, Hironaka/Scheme/BlowUpSequence/Truncate.lean),
to which Corollary 89 applies, and the results are carried from the prefix to stage l along the
truncation lemmas. Together with the going-down theorem this gives the one-to-one correspondence of
Corollary 85 between order reduction on X and on a hypersurface of maximal contact.
Two groups of auxiliary lemmas are proved on the way:
- Corollary 89 read on the push-forward (
cosupp_markedTransformSeq_pushforward_inter_eq_iInter).Hironaka/Resolution/Algebraic/Kol07/Corollary89.leanstates Corollary 89 on the restrictionΠ|_S = B.pullback ιwith the stage liftsB.pullbackStageHom ι i; forB = T.pushforward ιthe restriction isTitself (pullback_pushforward) and the lifts are the stage inclusionsT.pushforwardStageHom ι i(pullbackStageHom_pushforward_heq_mk, by induction with the transport ofpullbackStageHomalongeqToHom-composites), so the two sets of Corollary 89 are transported pointwise to the stages ofT. - The simple normal crossing lemmas along a sequence (
E_j + H_jis snc,E_j|_{H_j} = (E|_H)_j) in prefix form, with the normal crossing hypothesis only at the stages< j(isSnc_totalTransformSeq_append_of_forall_lt,totalTransformSeq_comap_pullbackStageHom_of_forall_lt), the form the induction uses.
Congruences along an equality of sequences and of morphisms #
The stage lifts of a pullback depend only on the pulled-back morphism.
Transport of the stage lifts along an eqToHom on the source (the stage-lift form of
pullback_eqToHom_comp).
The embeddings of the pushforward are the stage lifts of its restriction #
On the push-forward B = T.pushforward j along a closed immersion [Kol07, 30.3], the stage
lift B.pullbackStageHom j n : (B.pullback j)_n ⟶ B_n of the restriction [Kol07, 30.2] is the
stage inclusion T.pushforwardStageHom j n : T_n ⟶ B_n; heterogeneously, as B.pullback j = T
holds only propositionally.
Corollary 89 on the push-forward #
The centers of a push-forward along S.subschemeι lie in the strict transforms of S
(strictTransformSeq_le_center_pushforward with ker S.subschemeι = S).
[Kol07, Corollary 89] for the push-forward Π = T.pushforward S.subschemeι, read on the
stages of T through the embeddings T.pushforwardStageHom, as the first line of [Kol07, 90]
uses it: the restricted sequence Π|_S is T and its stage lifts are the stage inclusions
(pullbackStageHom_pushforward_heq_mk); the two sets of Corollary 89 are transported pointwise
along the equality of stages.
More congruences along equalities of schemes and sequences #
comap of a family along heterogeneously equal morphisms (equal sources).
The maximal order of heterogeneously equal ideal sheaves.
Simple normal crossings along a sequence, in prefix form #
isSnc_totalTransformSeq_append_mk with the normal crossing hypothesis only at the stages
< j: E_j + H_j is snc as soon as the centers before j have simple normal crossings with the
E_i; the same induction, using one clause per step.
totalTransformSeq_comap_pullbackStageHom_mk with the normal crossing hypothesis only at the
stages < j: E_j|_{H_j} = (E|_H)_j; the same induction.
The induction of Kollár's item 90, and Theorem 84 as printed #
The going-up theorem [Kol07, Theorem 84] with the boundary E of [Kol07, Corollary 85]
carried along: for a D-balanced I with max-ord I = m, a smooth hypersurface S with E + S
snc, and a smooth blow-up sequence T of order ≥ m for (S, I|_S, m, E|_S), the push-forward
B = T.pushforward ι is a smooth blow-up sequence of order m for (X, I, E).
The proof is the induction of [Kol07, 90]. B is smooth (IsSmooth.pushforward); its normal
crossing and order clauses are proved at every stage l by strong induction on l, the clauses at
the stages < l making the prefix B.take l a sequence of order ≥ m
(isOrderGeSeq_take_of_forall_lt). At stage l, with the stage inclusion g = j_l : S_l ↪ X_l:
the order clause follows from max-ord I_l ≤ m (Lemma 61 iterated along the prefix) and
cosupp(J_l, m) ⊆ j_l^{-1} cosupp(I_l, m), the latter from Corollary 89 on the prefix T.take l
(whose push-forward is B.take l) and the D-balanced property
(cosupp_markedTransformSeq_subset_iInter), carried to stage l of T and B along the
truncation lemmas; the normal crossing clause lifts the simple normal crossings of Z_l with
(E|_S)_l in S_l to E_l in X_l, using E_l + S_l snc and E_l|_{S_l} = (E|_S)_l from the
prefix forms of the snc lemmas. Finally Remark 67 (max-ord I = m) turns order ≥ m into
order m.
Kollár's Theorem 84 [Kol07, Theorem 84] as printed: the going-up theorem at E = ∅
(E + S = S alone is snc for a smooth hypersurface, isSnc_append_empty_of_isSmoothDivisor;
∅|_S = ∅, empty_comap). The hypothesis _hSc, that S is not contained in
cosupp(I, m), is part of Kollár's statement of Theorem 84 and is kept so that the theorem reads
as printed; the proof does not need it, because it goes through
IsDBalanced.isOrderSeq_pushforward, whose Corollary 89 rests on the sheaf-level form of
Lemma 62, which holds with no nonvanishing hypothesis on the restriction I|_S.