The rounds on the nonmonomial part: the order transfer

Kollár's proof of the marked order reduction theorem [Kol07, Theorem 107] opens with rounds of order reduction on the nonmonomial part N(I) at its maximal order d, "until its order drops below m" [Kol07, 111, Step 1]; the modified algorithm of [Wlo09, Theorem 7.4.1] opens with the same rounds, run "until we drop max{ord_x N(I) : x ∈ supp I} to 1", i.e. at d ≥ 2 only. The library writes this loop once, with the mark m and a threshold t (m ≤ t) as parameters: the descent runs through the bounds d = D, …, t. Kollár's first step is the instance t = m, the first phase of the modified algorithm is m = 1, t = 2. The modules Modified/StepA*.lean hold this loop: the link (StepALink.lean), the descent (StepAChain.lean), the value on a relatively compact open (StepAFamily.lean) and its naturality.

This module holds the order transfer of a round: a list of order ≥ d for (N(𝓘), d) is of order ≥ m for (𝓘, m) when m ≤ d, by the identity N((Π)⁻¹_*(𝓘, m)) = (Π)⁻¹_* N(𝓘) of [Kol07, 111, Step 1] and 𝓘 ≤ N(𝓘) (the order along a centre is antitone in the ideal, ordAlongIdeal_anti). The identity is the predicate NonmonomialTransformIdentity, which the assembly takes as a parameter and which nonmonomialTransformIdentity_inhabitant proves.

theorem Hironaka.Manifold.BMOmod.ordAlongIdeal_anti {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (D : M.IdealSheaf) {J J' : M.IdealSheaf} (h : J ≤ J') (a : M.carrier) : Manifold.IdealSheaf.ordAlongIdeal D J' a ≤ Manifold.IdealSheaf.ordAlongIdeal D J a

The order along a centre is antitone in the ideal: a smaller ideal lies in more powers.

def Hironaka.Manifold.BMOmod.NonmonomialTransformIdentity {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) : Prop

The transform identity for the nonmonomial part at the exact order: along a list of order ≥ d for (N(𝓘), d), with 1 ≤ m ≤ d and d an upper bound of ord N(𝓘) on the manifold, the nonmonomial part of the marked transform of (𝓘, m) at every stage is the marked transform of (N(𝓘), d). This is Kollár's observation that the two birational transforms differ only in their monomial part, by a product of powers of the exceptional divisors [Kol07, 111, Step 1], in the setting of that step: order reduction of N(I) at its maximal order, so that every centre has order exactly d for N(𝓘) and the marked transform of (N(𝓘), d) stays purely nonmonomial. Without the bound the identity fails: for N = (x²), d = 1 and the blow-up of {x = 0} the marked transform of (N, 1) acquires a monomial factor. The predicate is a parameter of the assembly; nonmonomialTransformIdentity_inhabitant proves it.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.BMOmod.isOfOrderGe_of_nonmonomial {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (hid : NonmonomialTransformIdentity ψ₀) {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) (L : AnalyticManifold.BlowUpSequence ψ₀ M) {m d : ℕ} (hm : 1 ≤ m) (hmd : m ≤ d) (hmax : ∀ (x : ↑↧M.carrier), Manifold.IdealSheaf.ord (BMO.nonmonomialTriple S).I x ≤ ↑d) (hL : L.toSuccession.IsOfOrderGe (BMO.nonmonomialTriple S).I d S.F.idealSheaf) : L.toSuccession.IsOfOrderGe S.I m S.F.idealSheaf

The order transfer: a list of order ≥ d for (N(𝓘), d), with d bounding ord N(𝓘), is of order ≥ m for (𝓘, m) when m ≤ d. The normal crossings clause is shared (same centres, same boundary), and at every stage 𝓘_i ≤ N(𝓘_i) = N_i (le_nonmonomialPart and the transform identity), so the order along the centre only grows: ord_Z 𝓘_i ≥ ord_Z N_i ≥ d ≥ m [Kol07, 111, Step 1].