The marked transform of the monomial ideal #
Kollár's Step 3 blows up a centre Z_S of order ≥ m for the marked monomial ideal
𝒪_X(−∑ a_D D); the marked transform π_*^{-1}(I, m) = 𝒪(mF) · π^* I of
[Kol07, Definition 60] is again the monomial ideal of the transported piece family: the
exponent of an old piece is unchanged and the exponent of the new piece F_P = π⁻¹(Z_P) is
a(P) − m, Kollár's "its coefficient is a_{j_ℓ} = a_{j₁} + a_{j₂} − m" of
[Kol07, 111, Step 3.2]. This module proves it stalk by stalk; the computation is the one behind
[Hau14, Proposition 5.4], not in the sources in this form.
stalkIdeal_monomial_exponentAt,monomial_exponentAt_eq_prod: the marked monomial ideal of a realising piece family is the product∏_c 𝓘(D_c)^{a_c}over the pieces. At a pointxits stalk is∏_{c ∈ faceAt x} (𝓘(D_c))_x^{a_c}(stalkIdeal_monomialofHironaka/Resolution/Algebraic/MarkedOrderReduction/Split.lean, the inner product over the components of a member collapsing to the one component throughx). These are stated for a regular ambient scheme withIsSncandRealizesonly, without a structure morphism, so that they apply on the blow-up, where the hypotheses give regular stalks but no relative dimension.stalkIdeal_vanishingIdeal_blowUpPieces_piece_of_lt,stalkIdeal_vanishingIdeal_blowUpPieces_piece_newComp: the stalks of the transported pieces' ideals, the strict transform of the piece's ideal and the exceptional ideal.comap_monomial_eq,markedTransform_monomial:π^* 𝒪_X(−∑ a_c D_c) = F^m · 𝒪_{X'}(−∑ a'_{c'} D'_{c'}). At a pointx'ofFoverx ∈ Z_Q,π^* z_c = u_c · ewithethe exceptional generator and(u_c)the strict transform's stalk forc ∈ Q, while forc ∉ Qthe strict transform is(π^* z_c)(Hironaka/Scheme/Snc/TotalTransformSnc.lean); soπ^* I_x = ∏_c (u_c)^{a_c} · e^{a(Q)}and the exponent ofF_Qisa(Q) − monceF^mis divided out. OffFthe blow-up is an isomorphism.
markedTransform_monomial is applied at every step of the run in
Hironaka/Resolution/Algebraic/Monomial/Geometric/OrderSeq.lean.
The monomial ideal as a product over the pieces #
The stalk of the marked monomial ideal at x is the product over the pieces through x of
the powers of their reduced stalks: the inner product of stalkIdeal_monomial
(Hironaka/Resolution/Algebraic/MarkedOrderReduction/Split.lean) over the components of a member
through x collapses to the one component through x, whose exponent is that of the unique piece
through its generic point, and the members through x correspond to the pieces through x.
The marked monomial ideal is the product over the pieces ∏_{c < nextComp} 𝓘(D_c)^{a_c}:
stalk by stalk, the pieces missing x contribute the unit ideal.
The stalks of the transported pieces #
The reduced ideal of the strict transform of an old piece has, at every point, the stalk of
the strict transform of the piece's ideal: through the member of the transported family (a
smooth divisor, stalkIdeal_vanishingIdeal_piece on the blow-up), whose strict transform has
the same saturation stalk as the piece's (stalkIdeal_strictTransformAlong_eq_iSup).
The reduced ideal of the new piece F_P = π⁻¹(Z_P) has, at a point over Z_P, the stalk of
the exceptional ideal (the new piece's member is the exceptional divisor).
The total transform of a piece's ideal at a point of the exceptional divisor #
At a point x' of the exceptional divisor over x ∈ Z_Q, the total transform of the ideal
of a piece c is the strict transform times the exceptional ideal if c ∈ Q (π^* z_c = u_c · e)
and the strict transform itself if c ∉ Q (the piece is transversal to the centre, or misses
x); the two cases of Hironaka/Scheme/Snc/TotalTransformSnc.lean, as in [Hau14, Proposition 5.4].
The total transform of the monomial ideal #
Stalk by stalk: π^* 𝒪_X(−∑ a_c D_c) = F^m · 𝒪_{X'}(−∑ a'_{c'} D'_{c'}) at every point of the
blow-up. Over a point of Z_Q the old pieces contribute their strict transforms and, for the
pieces of Q, one exceptional factor each (F^{a(Q)} in all), the new piece F_Q contributes
F^{a(Q) − m}, and the other new pieces miss the point; off the exceptional divisor the blow-up
is an isomorphism.
The total transform of the marked monomial ideal is F^m times the monomial ideal of the
transported piece family: the old pieces keep their exponents, the new piece F_P gets
a(P) − m ([Kol07, 111, Step 3.2]).
The marked transform of the marked monomial ideal under the blow-up of a centre of order
≥ m is the monomial ideal of the transported piece family: 𝒪(mF) · π^* I of
[Kol07, Definition 60] divides F^m out of the total transform.