The monomial split, III: the factorisation and its uniqueness #
The split I = M(I) · N(I) of [Kol07, Definition–Lemma 110] in its fine form (one exponent per
irreducible component; Hironaka/Resolution/Algebraic/MarkedOrderReduction/MonomialPart.lean):
M(I) = ∏_D 𝓘_D^{ord_D I} divides I because at every point x the ideal I_x lies in
(z_c)^{ord_D I} for every component D through x ([Kol07, Definition 47] propagated from the
generic point, stalkIdeal_le_pow_of_specializes) and the powers of the distinct parameters z_c
multiply (prod_dvd_of_forall_dvd_of_pairwise); the quotient N(I) = (I : M(I)) then satisfies
M(I) · N(I) = I (the division by an invertible ideal sheaf), has order 0 at every generic
point (ord_η I = ord_η I + ord_η N(I), orders adding at the generic point of a component), is
nonzero on every component (N(I) ⊇ I), and the factorisation is unique (the exponents are read
off as orders at the generic points, the cofactor is the colon). The monomial part absorbs
monomials and the nonmonomial part ignores them (Kollár's "differ … only in their monomial part",
[Kol07, 111, Step 1]), and for E = ∅ the nonmonomial part is I (the last paragraph of
[Kol07, 111]).
monomial_congr,monomial_add,isNonzeroEverywhere_nonmonomialPart_of,nonmonomialPart_of_isEmpty_offor any family, and in the setting of a normal-crossings family on a smooth Noetherian scheme (Hironaka.BMO.Snc):le_monomialPart,monomialPart_dvd,monomialPart_mul_nonmonomialPart,ord_monomial_mul_genericPoint,ord_monomialPart_of_mem_genericPoints,ord_nonmonomialPart_eq_zero,monomial_eq_monomialPart_of_mul_eq,monomialPart_monomial_mul,nonmonomialPart_monomial_mul. The statements on a triple are inHironaka/Resolution/Algebraic/MarkedOrderReduction/SplitTriple.lean.
A monomial depends on its exponents only at the generic points of the members' components.
Exponents add: 𝒪_X(−∑ (a_D + b_D) D) = 𝒪_X(−∑ a_D D) · 𝒪_X(−∑ b_D D).
N(I) is nonzero on every component when I is, since N(I) ⊇ I ([Kol07, Notation 64 (2)]
for the nonmonomial part).
For the empty family the monomial part is the empty product 𝒪_X and the nonmonomial part is
I (the last paragraph of [Kol07, 111]: "if E = ∅ then N(I) = I").
I ⊆ M(I) ([Kol07, Definition 47] and [Kol07, Definition–Lemma 110]): at a point x, in
Kollár's coordinates, I_x ⊆ (z_c)^{ord_D I} for each member through x
(stalkIdeal_le_pow_of_specializes), and the powers of the distinct parameters multiply.
M(I) divides I: I ⊆ M(I) and M(I) is invertible.
The split I = M(I) · N(I) of [Kol07, Definition–Lemma 110].
The exponent bookkeeping at a generic point: for a monomial K = 𝒪_X(−∑ a_D D) and any J,
ord_η (K · J) = a_D + ord_η J at the generic point η of D.
The order of M(I) at the generic point of a component is the component's exponent
ord_D I.
ord_D N(I) = 0 at every component: "cosupp N(I) does not contain any of the E^i" of
[Kol07, Definition–Lemma 110], in the fine form.
The uniqueness of the split ([Kol07, Definition–Lemma 110]: "uniquely"): the exponents are the orders at the generic points and the cofactor is the colon.
The monomial part absorbs monomials ([Kol07, 111, Step 1]: the two transforms "differ … only in their monomial part").
The nonmonomial part ignores monomials ([Kol07, 111, Step 1]).