Order reduction on a curve: the general step blows up the cosupport once #
Kollár's outline of the induction, [Kol07, 70], dismisses dimension one: on a curve the cosupport
of an ideal sheaf is a Cartier divisor, "our algorithm tells us to blow up Z := cosupp(I, m)",
and after that one blow-up the transform I ⊗ O_X(Z) has order < m. In this library dimension
one is not a base case of the recursion: the stage tower S0 1 is produced from any base stage
S0 : OrderReductionStage 0 by the general step, the construction of [Kol07, Theorem 103]. This
file checks that the general step does what Kollár says (stage1_BO_eq_blowUp_cosupp): on a
smooth curve X with E = ∅ and max-ord I = m ≥ 1, the value of the unmarked functor
(tower S0 1).bo m is the single blow-up of the reduced cosupport, cons X Z nil with
Z = vanishingIdeal Z.support and Z.support = {x | m ≤ ord_x I}. It is a check of the
construction: the axioms of a smooth blow-up sequence functor of order m alone do not determine
the sequence (on a curve with two points p ≠ q of order m, "blow up {p}, then {q}" is also
a smooth blow-up sequence of order m without empty centres whose end has maximal order < m).
The argument has two halves.
- The value has at most one member, read off the construction through the descent identity of
the global case.
(tower S0 1).bo m = boOfBMO S0.bmo m, whose functor is the glued functorBO.functor 1 m bdof [Kol07, Theorem 103, Step 3] for the databd m j = bdData 1 m j …of [Kol07, Lemma 102], fed with the amalgam ofS0.bmo. Over a local coverg : T' → T(Triple.exists_isLocalCover), the pull-back of the value is the maximal-contact casemaxContactCaseonT'(functor_seq_pullback_localCover), and pulling back preserves the length. At the mark,maxContactCaseis Step 2 of [Kol07, 104] on the tuned triple: Step 2.1 is empty sinceE = ∅(step21Seq_zero), and Step 2.2 is the re-tunedBD_{1,·,0}at the hypersurface of maximal contact, whose raw output (rawSeq) isπ_{-1}followed by the pushed-forward value of the inductive marked functor on the restricted triple, of dimension0, where every marked functor isnil(seq_eq_nil_of_hasDimLE_zero; this is where the base enters, and it enters for every base, so neither the base stage nor the amalgam is unfolded). Each tuning layer (maxContactCase,step22Functor,dataFunctor) returnsnilbelow its mark, so every layer is covered by a two-case lemma… .length ≤ 1. - The centre is forced. Clause (1) of the data,
max-ord I_r < m, excludes the empty sequence (its weak transform isI, of maximal orderm), so the value iscons X Z nil;Zis reduced bycenter_eq_vanishingIdeal_support_of_isOrderSeq; every generic point ofZhas orderm([Kol07, Definition 66]) and{x | m ≤ ord_x I}is closed (isClosed_setOf_le_ord), soZ.support ⊆ cosupp(I, m); conversely a pointxof order≥ moffZhas a preimagex'on the blow-up, which is an isomorphism off the centre (exists_π_eq_of_notMem_support), where the weak transform keeps the order (ord_weakTransform_of_notMem), against clause (1).
At n = 1 the hypothesis I|_H ≠ 0 of [Kol07, Theorem 80 (1)] fails for H = {p}, so the
maximal-contact property of H cannot come from that theorem; it enters here only through the
local existence of a hypersurface of maximal contact built into the construction
(globalizationData_localClass, valid in every dimension), and no global hypersurface is built.
The marked iteration of Kollár's remark is not part of the check.
A marked functor's value on a marked triple of dimension ≤ 0 has length 0 (the
dimension-zero case, OrderGeSeqAssignment.seq_eq_nil_of_hasDimLE_zero).
The output of [Kol07, Lemma 102] is the first blow-up followed by
τ_* BMO_{n−1,m}(S, I_0|_S, m, E_S); at n = 1 this tail is empty: it is the pushed-forward
value of the marked functor on the restricted triple, which has dimension ≤ 0.
The functor of [Kol07, Lemma 102] in dimension 1 has at most one member: the raw output is
π_{-1} followed by the empty tail, and the empty-blow-up convention [Kol07, 32] deletes empty
blow-ups.
The tuned BD_{1,m,j} (the tuning of [Kol07, Theorem 103, Step 1] applied to the functor of
Lemma 102) has at most one member: it is the functor of Lemma 102 on the tuned triple at the mark,
and nil below it.
The functor of the data of [Kol07, Lemma 102] in dimension 1 has at most one member, at
every mark (at the mark 0 the data are the erasure of empty blow-ups from zeroFunctor).
[Kol07, 104, Step 2.2]: the re-tuned functor of Step 2.2 has at most one member when the data of Lemma 102 do.
[Kol07, 104, Step 2.1] with E = ∅: Step 2.1 with no boundary members is empty.
[Kol07, 104] (Step 2 of the proof of Theorem 103) with E = ∅: Step 2 on a triple without
boundary members has at most one member, since Step 2.1 is empty and Step 2.2 has at most one.
[Kol07, Theorem 103, Steps 1 and 2] with E = ∅: the maximal-contact case maxContactCase
on a triple without boundary members has at most one member (nil below the mark).
[Kol07, Theorem 103, Step 3]: BO_{1,m} on a triple without boundary members has at most one
member; over a local cover the value is Step 2's, and pulling back preserves the length.
A blow-up sequence of length at most one that is not empty is a single blow-up.
Order reduction on a curve ([Kol07, 70]): on a smooth curve with E = ∅ and
max-ord I = m ≥ 1, the unmarked functor of the stage produced from any base by the general step
is the single blow-up of the reduced cosupp(I, m). The value has at most one member by the
construction (length_functor_seq_le_one at the data that boOfBMO S0.bmo m exposes), is not
empty by clause (1), and its centre is forced (the centre of an order sequence is reduced, the
order is upper semicontinuous, and the blow-up is an isomorphism off the centre).