The transform identity for the nonmonomial part, at the exact order and modulo N

Kollár's proof of the marked order reduction theorem [Kol07, Theorem 107] rests on an observation made at the end of its first step [Kol07, 111, Step 1]: along a blow-up sequence of order ≥ m for (I, m) whose centres also have order ≥ d for the nonmonomial part N(I), the birational transforms of (I, m) and of N(I) differ by a product of powers of the exceptional divisors, hence only in their monomial part, so that N((Π)⁻¹_*(I, m)) = (Π)⁻¹_* N(I). This module proves two forms of that identity on an analytic manifold, stage by stage along a list of centres:

• nonmonomialTransformIdentityMod_inhabitant, the identity modulo N at an arbitrary order s for (N(𝓘), s): N(mt_i(𝓘, m)) = N(mt_i(N(𝓘), s)) at every stage i, with respect to the transformed boundary. No bound on the order of N(𝓘) and no relation between m and s is needed; the separation step of the proof [Kol07, 111, Step 2] uses it at s < m.
• nonmonomialTransformIdentity_inhabitant, the identity at the exact order d ≥ m when ord N(𝓘) ≤ d everywhere: N(mt_i(𝓘, m)) = mt_i(N(𝓘), d), the right side without an outer N, because the marked transform of a purely nonmonomial ideal at its exact order stays purely nonmonomial (componentExponent_markedTransformSeq_nonmonomialTriple_eq_zero). The first step of the proof [Kol07, 111, Step 1] uses it.

The two identities are the predicates NonmonomialTransformIdentityMod and NonmonomialTransformIdentity, which the assembly of the theorem takes as parameters. The input is the identity for one blow-up along a smooth centre (nonmonomialPart_birationalTransform_eq_nonmonomialPart_totalTransform_nonmonomialPart and its consequences); the induction along the stages realigns the marked ideal from the chart of the stage to the fixed model ψ₀ at each step. The scheme-theoretic counterpart is Hironaka.BMO.nonmonomialPart_markedTransformSeq_eq_of_isOrderGeSeq.

theorem Hironaka.Manifold.BMOmod.nonmonomialTransformIdentityMod_inhabitant {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) : BMO.NonmonomialTransformIdentityMod ψ₀

The transform identity modulo N along a list of centres: for a list of order ≥ m for (𝓘, m) and of order ≥ s for (N(𝓘), s), the nonmonomial parts of the marked transforms of (𝓘, m) and of (N(𝓘), s) coincide at every stage, with respect to the transformed boundary (the observation at the end of [Kol07, 111, Step 1], read modulo the monomial part). Induction on the stage: the base case is the idempotence N(N(𝓘)) = N(𝓘) (nonmonomialPart_nonmonomialPart); at a successor stage the marked ideal is realigned from the chart of the stage to the fixed model ψ₀, the identity for one blow-up, N(π⁻¹_*(J, k)) = N(π^* N(J)), is applied to both marked ideals, and the induction hypothesis identifies the two right sides.

theorem Hironaka.Manifold.BMOmod.componentExponent_markedTransformSeq_nonmonomialTriple_eq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) (L : AnalyticManifold.BlowUpSequence ψ₀ 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) (i : Fin (L.toSuccession.length + 1)) (j : BMO.ComponentIndex (L.toSuccession.totalTransformSeqFrom S.F i)) : BMO.componentExponent (L.toSuccession.totalTransformSeqFrom S.F i) ⋯ (L.toSuccession.markedTransformSeq (BMO.nonmonomialTriple S).I d i) j = 0

The marked transform of a purely nonmonomial ideal at its exact order stays purely nonmonomial: along a list of order ≥ d for (N(𝓘), d), where d bounds the order of N(𝓘) everywhere, the marked transform of (N(𝓘), d) has, at every stage, vanishing exponent along every component of the transformed boundary, i.e. its monomial part is trivial. Induction on the stage: N(𝓘) itself has vanishing exponents (componentExponent_nonmonomialPart_eq_zero); at a successor stage the order of the previous transform along the centre is exactly d, so the marked transform is the weak transform (birationalTransform_eq_weakTransformOf_of_ordAlong_eq), and the weak transform at the exact order of an ideal with vanishing exponents has vanishing exponents (componentExponent_weakTransformOf_eq_zero).

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

The transform identity at the exact order (the observation at the end of [Kol07, 111, Step 1]): for m ≤ d, along a list of order ≥ d for (N(𝓘), d) with ord N(𝓘) ≤ d everywhere, the nonmonomial part of the marked transform of (𝓘, m) at every stage is the marked transform of (N(𝓘), d) itself, N(mt_i(𝓘, m)) = mt_i(N(𝓘), d). The induction on the stage carries along the fact that mt_i(𝓘, m) is nonzero everywhere; the order clause for (𝓘, m) at each centre follows from the one for (N(𝓘), d), since 𝓘_i ⊆ N(𝓘_i) = N_i gives ord_Z 𝓘_i ≥ ord_Z N_i ≥ d ≥ m. At a successor stage the identity for one blow-up gives N(mt_{i+1}(𝓘, m)) = N(π^* N(mt_i(𝓘, m))), the induction hypothesis rewrites the inner ideal to mt_i(N(𝓘), d), and the transform of that ideal at its exact order is its own nonmonomial part (nonmonomialPart_birationalTransform_eq_self, from the purity of the previous theorem).