The first step of Lemma 102: the centre Z_{-1} #
The proof of [Kol07, Lemma 102] begins by blowing up Z_{-1}, "the union of those irreducible
components E^{jk} ⊂ E^j" contained in cosupp(I, m): the blow-up π_{-1} : X_0 → X is an
isomorphism, but the order of I along each such component drops by m, giving a new ideal sheaf
I_0 with max-ord_{E^{jk}} I_0 ≤ 0, so that cosupp(I_0, m) contains no irreducible component
of E^j. On a manifold the irreducible components of the smooth
hypersurface E^j are its connected components, and Z_{-1} is the set BD.Zminus1:
the points of E^j whose component lies in {ord 𝓘 ≥ m}.
The first group of results describes Z_{-1} as a set and as a submanifold: its characterisation
(mem_Zminus1_iff), the inclusions Z_{-1} ⊆ cosupp(𝓘, m) and Z_{-1} ⊆ E^j, the fact that it
is a
union of connected components of E^j, and that it is a closed hypersurface
(isClosedSubmanifold_Zminus1): every point of E^j has an adapted chart of E^j whose source
meets E^j only inside the component of the point, so on that source Z_{-1} is all of E^j or
empty.
The second group is the first step itself. Blowing up Z_{-1} is a smooth blow-up sequence of
order m (isOfOrder_firstStep): Z_{-1} has simple normal crossings with E, an snc chart of
E at a point of Z_{-1} restricted to a neighbourhood meeting E^j only in the component of the
point being adapted to Z_{-1} (hasSncWith_Zminus1), and the order of 𝓘 along Z_{-1} is m
at each of its points, at least m because ord 𝓘 ≥ m on all of Z_{-1} and at most m by the
bound (ordAlong_Zminus1_eq). The weak transform I_0 has order 0 over Z_{-1}
(ord_weakTransformOf_eq_zero_of_mem_Zminus1): the blowing-up of a hypersurface is a local
analytic isomorphism ([Kol07, Warning 20]), so the total transform has the order of 𝓘, at most
m, and lies in the m-th power of the exceptional ideal, whose colon by that power is then the
unit ideal (ColonOrder.lean). Off Z_{-1} the weak transform has the order of 𝓘 at the image
(ord_weakTransformOf_eq_of_not_mem). Hence no component of the transform of E^j lies in
cosupp(I_0, m) (Zminus1_weakTransformOf_eq_empty).
The last group prepares the next triple (S, I_0|_S, E_S) of Kollár's proof, which requires
I_0|_S nonzero on every component of S = E^j. A D-balanced ideal sheaf ([Kol07, Definition 83])
of order at most m has order 0 or m at every point (ord_eq_zero_or_eq_of_isDBalanced), and
for such 𝓘 the restriction of I_0 to the transform of E^j is nonzero everywhere
(isNonzeroEverywhere_pullback_weakTransformOf): its zero stalks form an open and closed set, while
every component of the transform of E^j carries a point where I_0 has order 0.
The results are assembled into Lemma 102's functor in BD.lean; their behaviour under pull-back is
in Functoriality.lean.
A point lies in Z_{-1} iff it lies in E^j and its connected component in E^j lies in
cosupp(𝓘, m) (the definition of Zminus1 unfolded; the proof of [Kol07, Lemma 102]).
The connected component through a point of Z_{-1} lies in Z_{-1}: Z_{-1} is a union of
connected components of the hypersurface.
Z_{-1} ⊆ cosupp(𝓘, m) (the proof of [Kol07, Lemma 102]).
Z_{-1} ⊆ E^j ("E^{jk} ⊂ E^j" in the proof of [Kol07, Lemma 102]).
Z_{-1}, a union of connected components of the closed hypersurface E^j, is a closed
hypersurface: on the source of an adapted chart of E^j meeting E^j only inside one component,
Z_{-1} is all of E^j or empty.
Z_{-1} has simple normal crossings with E, and the order along it #
Z_{-1} has simple normal crossings with E (the centre of the proof of [Kol07, Lemma 102]
must be admissible): an snc chart of E at a point of Z_{-1}, restricted to a neighbourhood
meeting E^j only inside the component of the point, is adapted to Z_{-1} with the coordinate
of E^j.
The order of 𝓘 along Z_{-1} at each of its points is m (the proof of
[Kol07, Lemma 102], "max-ord_{E^{jk}} I ≤ m to start with"): at least m because ord 𝓘 ≥ m on
all of Z_{-1}, at most m by the bound at the point.
The first step of the proof of [Kol07, Lemma 102], "blow up Z_{-1}": for ord 𝓘 ≤ m
everywhere, blowing up Z_{-1} is a smooth blow-up sequence of order m starting with
(M, 𝓘, E) ([Kol07, Definition 66]): the centre has normal crossings with E
(hasSncWith_Zminus1) and ord_{Z_{-1}} 𝓘 = m at every point of the centre
(ordAlong_Zminus1_eq).
The orders of the weak transform #
"Since max-ord_{E^{jk}} I ≤ m to start with, max-ord_{E^{jk}} I_0 = max-ord_{E^{jk}} I − m ≤ 0"
(the proof of [Kol07, Lemma 102]): for ord 𝓘 ≤ m everywhere, the weak transform I_0 of 𝓘 by
the blowing-up of Z_{-1} has order 0 at every point over Z_{-1}. The stalk of I_0 is the
colon (π⁻¹(𝓘)_{x'} : u^m), m being the order of 𝓘 along Z_{-1} and u the scaling
coordinate of a blow-up chart; π⁻¹(𝓘)_{x'} ⊆ (u)^m, and ord π⁻¹(𝓘)_{x'} = ord 𝓘_{π x'} ≤ m
because the blowing-up of a hypersurface is an isomorphism ([Kol07, Warning 20]); the colon is then
the unit ideal (ord_colon_totalTransform_eq_zero).
Off the centre the blowing-up is the identity on the ideal sheaf: at a point not over Z_{-1}
the weak transform has the order of 𝓘 at its image. The exponent of the colon is 0 there (the
component of the centre through a point off it is empty), so the stalk of I_0 is the total
transform's, and π is a local analytic isomorphism off the centre.
"Thus cosupp(I_0, m) does not contain any irreducible component of E^j" (the proof of
[Kol07, Lemma 102]): for 1 ≤ m and ord 𝓘 ≤ m everywhere, no connected component of the
preimage of E^j under the blowing-up of Z_{-1} lies in cosupp(I_0, m). The points over
Z_{-1} carry order 0; a component not over Z_{-1} is, through the isomorphism π
([Kol07, Warning 20]), a component of E^j that was not selected, which carries a point of order
< m of 𝓘, where I_0 has that order.
The restriction of the weak transform to the transform of E^j is nonzero #
A D-balanced ideal sheaf ([Kol07, Definition 83]) with ord 𝓘 ≤ m everywhere has order 0 or
m at every point, as Kollár notes after Definition 83. Not stated in the sources for sheaves; the
argument: if 0 < ord_x 𝓘 = k < m then x ∉ cosupp(D^k 𝓘), so (D^k 𝓘)^m ⊆ 𝓘^{m-k} makes the
stalk of 𝓘^{m-k}, hence of 𝓘, the unit ideal at x.
The next triple (S, I_0|_S, E_S) of the proof of [Kol07, Lemma 102], with S := E^j, has an
ideal sheaf that is nonzero on every component of S, as [Kol07, Definition 31 (1)] requires: for
D-balanced 𝓘 ([Kol07, Definition 83]) with ord 𝓘 ≤ m everywhere, the restriction of the weak
transform I_0 to the transform of E^j (a closed hypersurface hZ' of the blown-up manifold) is
nonzero everywhere. The zero stalks of the restriction form an open and closed set, hence a union
of components of the transform of E^j; but every component carries a point where I_0 has order
0: every point over Z_{-1}, and on a component not over Z_{-1} the point of order < m, hence
0 by D-balancedness, of 𝓘 on the unselected component of E^j it covers; there the restricted
stalk is the unit ideal.