Lemma 102: the order clause #
[Kol07, Lemma 102] asserts that BD_{n,m,j} is a smooth blow-up sequence functor of order m.
For the construction BDan of BD.lean this is proved here: the first blow-up, of Z_{-1}, has
order s = tuningParam m for the tuned ideal (FirstStep.lean); the tail is the push-forward of
the value of the input functor on the
restricted triple, of order ≥ m for (I_0, E) by [Kol07, Corollary 85] with the transform of
E^j in the boundary (BDCor85.lean); and the first blow-up, when it is empty (no component of
E^j lies in cosupp(I, m)), is deleted ([Kol07, 32]).
The tail of the core is the push-forward of a list of centres, while Corollary 85 is stated for the
push-forward of a succession of blow-ups. Their identification for lists without empty centres,
BlowUpSequence.toSuccession_pushforward, enters here as the hypothesis PushforwardBridge ψ₀, so
that the clause is proved for any model; BDBridge.lean discharges it and states the clause
unconditionally (BDan_isOfOrder).
PushforwardBridge ψ₀— the identification as a hypothesis.BlowUpSequence.noEmptyCenters_pushforward_of_bridge,BlowUpSequence.isOfOrderGe_map_emptyBlowUp— the push-forward of a list without empty centres has none ([Kol07, 32]); a sequence of order≥ mon the blow-up of an empty centre, transported along the isomorphism with the base, is of order≥ mthere.BDan.weakTransform_eq_weakTransformI,BDan.reducedTransform_eq_idealSheaf_append— the weak transform and the boundary after the first blow-up, in the form used by the successions, areI_0and the reduced ideal sheaf of(E - E^j)|_{X_0} + S_0.BDan.weakTransformI_eq_comap_of_eq_empty,BDan.idealSheaf_append_eq_comap_of_eq_empty— whenZ_{-1} = ∅the first blow-up is an isomorphism and both are pull-backs.BDan.pushforward_isOfOrderGe_of_bridge,BDan.cons_isOfOrder_of_bridge,BDan.coreOfListOf_isOfOrderGe_of_bridge— the order clause for the core over any sequenceLonS_0without empty centres and of order≥ sfor the restricted triple: its tail, the core before the deletion of the empty first blow-up, and the core.BDan_isOfOrder_of_bridge— the order clause of Lemma 102, given the identification: the previous item at the value of the input functor.
The identification of the push-forward of a list of centres on a closed hypersurface S with
the push-forward of the corresponding succession of blow-ups ([Kol07, 30.3]), for lists without
empty centres, as a hypothesis on the model; it is BlowUpSequence.toSuccession_pushforward
(BDBridge.lean).
Equations
- One or more equations did not get rendered due to their size.
Instances For
[Kol07, 32] for the push-forward: the centres of the push-forward are the images of the centres, so a list without empty centres pushes forward to one without empty centres (through the identification).
Transport of [Kol07, Definition 66] along the isomorphism of an empty blow-up ([Kol07, 32]): a
list on the blow-up of the empty centre, of order ≥ m for the pull-backs of (I, E₀),
transported to M along the isomorphism is of order ≥ m for (I, E₀).
The support of E is the support of E - E^j together with E^j.
The weak transform under the first blow-up, in the form used by the successions, is I_0.
The boundary after the first blow-up is the reduced ideal sheaf of (E - E^j)|_{X_0} + S_0: the
total transform of E and the family (E - E^j)|_{X_0} + S_0 have the same support, since
Z_{-1} ⊆ E^j.
When Z_{-1} = ∅ the weak transform I_0 is the pull-back of 𝓘 along the isomorphism
π_{-1}.
When Z_{-1} = ∅ the first blow-up is an isomorphism and the boundary after it is the
pull-back of the boundary.
The pushed-forward tail of the core over a sequence L of order ≥ s for the restricted
triple, without empty centres, is of order ≥ s for (I_0, E - E^j + S_0): the going-up property
of D-balanced ideals with S_0 added to the boundary ([Kol07, Theorem 84], [Kol07, Corollary 85];
pushforward_isOfOrderGe_append), given the identification of the two push-forwards.
The core before the deletion of the empty first blow-up is of order s: the first step by
BD.isOfOrder_firstStep and the pushed-forward tail by pushforward_isOfOrderGe_of_bridge.
The order clause of [Kol07, Lemma 102] for the core over a sequence, given the
identification of the two push-forwards: if L has no empty centres and is a smooth blow-up
sequence of order ≥ s for the restricted triple, the core over L at Z_{-1} and S_0 is a
smooth blow-up sequence of order ≥ s starting with (M, 𝓘, s, E) — the first blow-up has order
s and the tail order ≥ s (cons_isOfOrder_of_bridge); when Z_{-1} is empty the first blow-up
is deleted and the tail is transported along the isomorphism of the empty blow-up.
The order clause of [Kol07, Lemma 102], given the identification of the two push-forwards:
BD_{n,m,j}(M, 𝓘, E) is a smooth blow-up sequence of order m starting with (M, 𝓘, E). The
first blow-up has order s = tuningParam m for the tuned ideal (BD.isOfOrder_firstStep); the
pushed-forward
tail has order ≥ s by [Kol07, Corollary 85] with S_0 in the boundary
(pushforward_isOfOrderGe_append, the weak transform I_0 being D-balanced of order ≤ s);
when the first blow-up is empty it is deleted and the tail is transported along the isomorphism.
The whole is proved for the tuned triple (M, W_s(𝓘), E) at the mark s and carried back to
(𝓘, m) by orderReduction_tuned_iff (Step 1 of the proof of [Kol07, Theorem 103]).