The maximal coefficient ideal sheaf: Proposition 99, orders and cosupports #
Kollár's maximal coefficient ideal [Kol07, Definition 98] on an analytic manifold,
IdealSheaf.tuning J m s (Hironaka/Manifold/IdealSheaf/Tuning.lean), has Kollár's sum
∑_{wt(e) ≥ s} ∏_j (D^j J)^{e_j} as its stalk at every point. Through the regular coordinates c
of the stalk 𝒪_{M,a} (exists_regularCoords_stalk) the derivative stalks are the Hironaka
library's c.Dpow j J_a (stalkIdeal_iteratedDeriv_eq_Dpow), so W_s(J)_a = c.W m s J_a is the
Hironaka library's coefficient ideal (stalkIdeal_tuning_eq_W). Every statement here is the
corresponding statement of the Hironaka library read at each stalk (IdealSheaf.ext, le_def):
[Kol07, Proposition 99] (1) tuning_anti, (2) tuning_mul_le, (3) deriv_tuning_succ,
(4) tuning_one and iteratedDeriv_tuning, (5) isMCInvariant_tuning, (6) tuning_mul_tuning,
(7) tuning_pow, (8) isDBalanced_tuning; [Kol07, Corollary 101] at the parameter
tuningParam m = max (m − 1) 1 · lcm(2, …, m); the order and cosupport identities
le_ord_tuning_iff, ord_tuning, cosupport_tuning (the local form of Kollár's
max-ord W(I) = m! [Kol07, Theorem 54.2], and the remark after [Kol07, Definition 83] that the
cosupport of a D-balanced ideal is cosupp(I, m)); and W_{s(1)}(J) = J. Kollár's hypothesis
m = max-ord I enters as hI : ∀ y, J.ord y ≤ m, i.e. ord J_a ≤ m at each stalk, exactly what
the Hironaka library uses. These are the properties of the tuned ideal sheaves that the
order-reduction algorithm relies on (Hironaka/Resolution/Analytic/OrderReduction/Tuned.lean).
Regular coordinates of the stalk at any point, 𝕜-linear and spanning the 𝕜-derivations
(exists_regularCoords_stalk in the chart at the point).
Definition 98 at the stalks and its finite form #
The stalk of W_s(J) is Kollár's sum [Kol07, Definition 98].
Through regular coordinates of the stalk, W_s(J)_a = c.W m s J_a, the Hironaka library's
coefficient ideal.
The finite form of W_s(J): a finite sum of finite products
(IsLocalRing.iSup_wt_eq_sum_tuningExponents at every stalk).
Proposition 99 (1)–(8) #
W_0(J) = 𝒪.
W_t(J) ⊆ W_s(J) for s ≤ t [Kol07, Proposition 99 (1)].
W_s(J) · W_t(J) ⊆ W_{s+t}(J) [Kol07, Proposition 99 (2)].
J^k ⊆ W_s(J) when s ≤ m k: J^k is the term of W_s(J) with exponent vector
(k, 0, …, 0), of weight m k.
MC(J)^s ⊆ W_s(J): MC(J) = D^{m−1} J has weight 1, so MC(J)^s is a term of weight
s.
W_1(J) = D^{m−1} J: Kollár's "W_1(I) = MC(I)" [Kol07, Proposition 99 (4)].
D(W_{s+1}(J)) = W_s(J) for ord J ≤ m, m ≥ 1 [Kol07, Proposition 99 (3)].
Kollár's "MC(W_s(I)) = W_1(I) = MC(I)" [Kol07, Proposition 99 (4)]:
D^{s−1}(W_s(J)) = D^{m−1} J for s ≥ 1.
W_s(J) is MC-invariant with respect to s [Kol07, Proposition 99 (5)].
W_s(J) · W_t(J) = W_{s+t}(J) for s = r · lcm(2, …, m) and t ≥ (m − 1) · lcm(2, …, m)
[Kol07, Proposition 99 (6)].
W_s(J)^j = W_{js}(J) for s = r · lcm(2, …, m), r ≥ m − 1 [Kol07, Proposition 99 (7)].
W_s(J) is D-balanced with respect to s for s = r · lcm(2, …, m), r ≥ m − 1
[Kol07, Proposition 99 (8)].
Corollary 101 at the parameter tuningParam m #
W_{s(m)}(J) is D-balanced with respect to s(m) = tuningParam m ([Kol07, Corollary 101] at
s = s(m)).
W_{s(m)}(J) is MC-invariant with respect to s(m) = tuningParam m ([Kol07, Corollary 101]
at s = s(m)).
Orders and cosupports #
For m, s ≥ 1, s ≤ ord_x W_s(J) ↔ m ≤ ord_x J (the local form of Kollár's
max-ord W(I) = m!, [Kol07, Theorem 54.2 (i)]).
The cosupport of W_s(J) is the locus where J has order ≥ m (the remark after
[Kol07, Definition 83]: "cosupp(I, m) = cosupp I" for a D-balanced ideal): off it W_s(J) is
the unit sheaf (W_eq_top_of_ord_lt), on it W_s(J) has order ≥ s ≥ 1 (le_ord_W).
ord_x W_s(J) = s where ord_x J = m ≥ 1 (the local form of [Kol07, Theorem 54.2 (i)]).
W_{s(1)}(J) = J: for m = 1 the coefficient ideal is the ideal itself (Kollár's "I = W(I)"
for an ideal of order 1, [Kol07, Theorem 103, proof, Step 2.4]).