The round order of Step 1 on a relatively compact open set

Step 1 of the proof of [Kol07, Theorem 107] (item 111) applies order reduction to the nonmonomial part N(𝓘) at its maximal order d = max-ord N(𝓘) and repeats until that order drops below m. On a scheme the maximal order is a single number; on a manifold the order of N(𝓘) need not be bounded, so the round order is read on a relatively compact open U: d_U is the supremum of ord_x N(𝓘) over closure U, finite because N(𝓘) is nonzero at every point and the order of such an ideal sheaf is bounded on a compact set (IdealSheaf.bddAbove_ord_on_compact). This is the locally finite reading of [Wlo09, Theorem 2.0.3 (1)], in which the resolution is constructed on a neighbourhood of a compact set. The file supplies the round order, its finiteness, and the fact that the restriction of the nonmonomial triple (M, N(𝓘), E) to U lies in the class of BO_{n,d_U} (the domain of the order reduction functor of [Kol07, Theorem 68]) when d_U ≥ 1. The analytic counterpart of Hironaka.BMO.roundOrder.

noncomputable def Hironaka.Manifold.BMO.roundOrderOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) : ℕ

The round order d_U of a triple on a relatively compact open U: the supremum over closure U of the order of the nonmonomial part N(𝓘), as a natural number. Kollár's d = max-ord N(I) of [Kol07, 111, Step 1], read on a neighbourhood of a compact set. The supremum is finite when closure U is compact (coe_roundOrderOn).

Equations

• Hironaka.Manifold.BMO.roundOrderOn T U = (⨆ (x : ↑(closure ↑U)), (Hironaka.Manifold.BMO.nonmonomialPart T.F ⋯ T.I).ord ↑x).toNat

theorem Hironaka.Manifold.BMO.coe_roundOrderOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ↑(roundOrderOn T U) = ⨆ (x : ↑(closure ↑U)), (nonmonomialPart T.F ⋯ T.I).ord ↑x

The round order is the genuine supremum: (d_U : ℕ∞) = sup_{x ∈ closure U} ord_x N(𝓘). The supremum is finite because N(𝓘) is nonzero at every point and the order of such an ideal sheaf is bounded on the compact set closure U.

theorem Hironaka.Manifold.BMO.ord_le_roundOrderOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {x : M.carrier} (hx : x ∈ ↑U) : (nonmonomialPart T.F ⋯ T.I).ord x ≤ ↑(roundOrderOn T U)

The order of N(𝓘) at any point of U is at most the round order d_U.

theorem Hironaka.Manifold.BMO.boClass_nonmonomialTriple_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hpos : 1 ≤ roundOrderOn T U) : Manifold.AnalyticTriple.BOClass (roundOrderOn T U) ((nonmonomialTriple T).pullback (M.inclusion U) ⋯)

For d_U ≥ 1, the restriction of the nonmonomial triple (M, N(𝓘), E) to a relatively compact open U lies in the class BOClass d_U of the order reduction functor BO_{n,d_U} of Kol07, Theorem 68, defined on triples whose ideal has order at most d: the order of N(𝓘) on U is at most d_U, and only finitely many boundary members meet closure U. This is the input of a round of [Kol07, 111, Step 1].