Step 1 of Theorem 103: the tuned triple #
Step 1 of the proof of [Kol07, Theorem 103] replaces I by an ideal W(I) = W_s(I) which is
D-balanced and MC-invariant and for which order reduction is equivalent to order reduction for I,
taking s = m! "to avoid further choices". The ideal
W_s(I) is the maximal coefficient ideal of [Kol07, Definition 98], and [Kol07, Corollary 101]
admits any s = r · lcm(2, …, m) with r ≥ m − 1. On manifolds the tuned ideal sheaf is
𝓘.tuning m (tuningParam m), the maximal coefficient ideal sheaf of order s = tuningParam m,
where tuningParam m = max (m − 1) 1 · lcm(2, …, m) is the smallest admissible choice of s made
positive; this differs from Kollár's m!, which the argument does not need.
AnalyticTriple.tuned T m hm— the triple(M, W_s(𝓘), E): the tuned ideal sheaf with the same boundary; it is nonzero everywhere since𝓘^s ⊆ W_s(𝓘)and the stalks are domains.AnalyticTriple.boClass_tuned,hasMaximalContact_tuned,localMCClass_tuned,isDBalanced_tuned,isMCInvariant_tuned— the tuned triple of a triple ofBOClass mlies inBOClass s(the order ofW_s(𝓘)is at mostseverywhere), a hypersurface of maximal contact for(𝓘, m)is one for(W_s(𝓘), s)(MC(W_s(I)) = MC(I), [Kol07, Proposition 99 (4)]), and the tuned ideal sheaf is D-balanced and MC-invariant ([Kol07, Proposition 99 (5), (8)]). These need onlyord 𝓘 ≤ meverywhere, so no case distinction onmax-ord I = mis made: where the order is everywhere< mthe order-reduction sequence is empty anyway, no centre of a sequence of order≥ sbeing nonempty.AnalyticBlowUpSequenceAssignment.ofTunedClass— the Step 1 wrapper: a functor on a class whose tuned triples lie in the domain of a functorBat the marksis evaluated on the tuned triple.
The transfer of the order-reduction clauses between (𝓘, m) and (W_s(𝓘), s) is in
TunedLemmas.lean; the wrapper is applied to the local functor of Step 2 in Assembly.lean.
The tuned triple (M, W_s(𝓘), E) of Step 1 of the proof of [Kol07, Theorem 103], with
s = tuningParam m: the ideal sheaf replaced by its maximal coefficient ideal sheaf
𝓘.tuning m (tuningParam m) ([Kol07, Definition 98]), the boundary kept. The tuned ideal sheaf is
nonzero everywhere: it contains 𝓘^s (pow_le_tuning) and the stalks are domains.
Equations
- T.tuned m hm = { I := Manifold.IdealSheaf.tuning T.I m (IsLocalRing.tuningParam m), isNonzeroEverywhere := ⋯, F := T.F, isSnc := ⋯ }
Instances For
For ord 𝓘 ≤ m everywhere, the tuned ideal sheaf has order at most s = tuningParam m
everywhere: exactly s where ord 𝓘 = m, less than s where ord 𝓘 < m.
The tuned triple of a triple of the class BOClass m lies in the class BOClass s,
s = tuningParam m (Step 1 of the proof of [Kol07, Theorem 103]).
The tuned ideal sheaf is D-balanced at the mark s = tuningParam m (Step 1 of the proof of
[Kol07, Theorem 103]; [Kol07, Proposition 99 (8)]).
The tuned ideal sheaf is MC-invariant at the mark s = tuningParam m (Step 1 of the proof of
[Kol07, Theorem 103]; [Kol07, Proposition 99 (5)]).
A hypersurface of maximal contact for (𝓘, m) is one for (W_s(𝓘), s), since
MC(W_s(I)) = MC(I) ([Kol07, Proposition 99 (4)]): the class with a global hypersurface of maximal
contact is stable under tuning.
The tuned triple of a triple of LocalMCClass m lies in LocalMCClass s, s = tuningParam m.
The wrapper for Step 1 of the proof of [Kol07, Theorem 103] ("from now on we assume that I is
D-balanced and MC-invariant"): a blow-up sequence functor on the class C whose values are those
of the functor B (at the mark s = tuningParam m) on the tuned triples; the class C forces
1 ≤ m and its tuned triples lie in the domain of B.
Equations
- One or more equations did not get rendered due to their size.