The full family, the functor BD_{n,m,j} and clause (1) #
The proof of [Kol07, Lemma 102], continued: since S = E^j, every blow-up center is a smooth
subvariety of the birational transform of E^j, so the sequence is of order m for the FULL
boundary E, not only for E − E^j; the functor is
BD_{n,m,j}(X, I, E) := τ_* BMO_{n−1,m}(S, I_0|_S, m, E_S) ∘ π_{-1}; and by [Kol07, Corollary 85]
the output Π_r : X_r → X has Π_r^{-1}_*(E^j) disjoint from cosupp(I_r, m).
The full family. Along a smooth blow-up sequence of order m starting with (X, I, E − E^j)
whose centers lie in the birational transforms of E^j, every center has simple normal crossings
with the total transform of the FULL E (IsOrderSeq.hasSncWith_totalTransformSeq_of_isEraseOf):
by induction along the sequence, carrying the relation that the total transform of E − E^j is
the total transform of E with the birational transform of E^j deleted
(IsEraseOf.isEraseOf_totalTransform, Hironaka/Scheme/Snc/EraseFamily.lean), the one-step content
being IsEraseOf.hasSncWith_of_le: some of the E^i are allowed to contain the center
([Kol07, Definition 24, (4)]). Hence the output rawSeq is a smooth blow-up sequence of order m
starting with (X, I, E) (isOrderSeq_rawSeq). Kollár states this in one sentence; the induction
is not in the sources.
The functor. BD.functor n m j B hDom is rawSeq with its empty blow-ups deleted
([Kol07, 32]; OrderSeqAssignment.ofEraseEmpty, Hironaka/Scheme/BlowUpSequence/Functor.lean; the
order condition survives deletion, IsOrderSeq.eraseEmpty), a smooth blow-up sequence functor of
order m on Lemma 102's standing class Domain n m j; exists_functor is the same in existential
form.
Clause (1). [Kol07, Corollary 89] for the pushed-forward sequence
(cosupp_markedTransformSeq_pushforward_inter_eq_iInter,
Hironaka/Resolution/Algebraic/Kol07/GoingUp.lean, the j = 0 term of the intersection): a point
of the birational transform of E^j at the last stage where the marked transform of I has order
≥ m is a point where the marked transform of I|_S along the composite sequence on S, the final
marked ideal of B on the restricted marked triple, has order ≥ m; clause (1) of Kol07, Theorem
69 for B says that ideal has max-ord < m. Marked and weak transforms of I agree along the
sequence ([Kol07, Remark 67]), and the points of the birational transform of E^j are the image of
the last stage inclusion (ker_pushforwardStageHom,
Hironaka/Scheme/BlowUpSequence/Pushforward.lean).
Used by FunctorialityPullback.lean and Assembly.lean, and outside this directory by
Hironaka/Resolution/Algebraic/Wlo05/EmbeddedCP1Step21.lean and HironakaExamples/Dimension1.lean
(Hironaka/Resolution/Algebraic/Wlo05/EmbeddedCP1Step22Core.lean imports it without using it).
Along a smooth blow-up sequence of order m starting with (X, I, F), where F is E with
E^j deleted, whose centers lie in the birational transforms of E^j, every center has simple
normal crossings with the total transform of E ([Kol07, Definition 24, (4)]; the proof of
[Kol07, Lemma 102]): by induction along the sequence, at the first step
IsEraseOf.hasSncWith_of_le; the total transform of F is the total transform of E with the
birational transform of E^j deleted (IsEraseOf.isEraseOf_totalTransform), which is snc
(AlgebraicGeometry.totalTransform_isSnc).
Deleting an empty first blow-up whose tail has no empty blow-ups ([Kol07, 32]) carries the tail
back along the inverse of the isomorphism blowUpπ X ⊤ (eraseEmpty_cons_top); the final weak
transform and the final strict transform of the result are the pull-backs of the tail's along the
last stage isomorphism (IsOrderSeq.weakTransformSeq_pullback, strictTransformSeq_pullback), so
a disjointness of the final cosupport from a final strict transform transfers.
The output is a smooth blow-up sequence of order m starting with (X, I, E) (Kollár: "we in
fact get a blow-up sequence of order m" for the full boundary, the proof of [Kol07, Lemma 102]):
the order-m sequence for (X, I, E − E^j) (isOrderSeq_rawSeq_erase), whose centers lie in the
birational transforms of E^j (strictTransformSeq_le_center_rawSeq), through
IsOrderSeq.hasSncWith_totalTransformSeq_of_isEraseOf.
If B satisfies clause (1) of [Kol07, Theorem 69], the final cosupport cosupp(I_r, m) of the
output is disjoint from the birational transform (Π_r)^{-1}_* E^j (clause (1) of
[Kol07, Lemma 102]; [Kol07, Corollary 89] for the push-forward; [Kol07, Remark 67]): a point of that
birational transform is the image of a point y of the last stage of the composite sequence on S
(ker_pushforwardStageHom); by the j = 0 term of Corollary 89, ord I_r ≥ m there forces
ord ≥ m for the final marked ideal of B on the restricted marked triple at y, which has
max-ord < m.
Clause (1) of [Kol07, Lemma 102] for the output with its empty blow-ups deleted ([Kol07, 32]),
the form BDData.disjoint_cosupp takes. Only π_{-1} can be empty (center_rawSeq_ne_top_of_pos):
if its center is nonempty nothing is deleted (eraseEmpty_eq_self_iff); if it is empty,
disjoint_eraseEmpty_cons_of_eq_top transports disjoint_cosupp_rawSeq along the isomorphism
carrying the tail back to X.
The boundary-clearing functor BD_{n,m,j} on the standing class Domain n m j of
[Kol07, Lemma 102] (I D-balanced with max-ord I = m, dim X ≤ n), for a marked functor B of
the shape of [Kol07, Theorem 69] in dimensions ≤ n − 1 and mark m (the inductive hypothesis
BMO_{n−1,m}): the output rawSeq for the j-th member of E (positions as in
DivisorFamily.nth) with its empty blow-ups deleted ([Kol07, 32]), a smooth blow-up sequence
functor of order m
(isOrderSeq_rawSeq, IsOrderSeq.eraseEmpty). The extension to BDClass n m j by tuning is
Assembly.lean.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The value of BD_{n,m,j} is the output with its empty blow-ups deleted.
There is a smooth blow-up sequence functor of order m on Domain n m j whose value is the
output with its empty blow-ups deleted: BD.functor, in existential form.