Kollár's explicit formula along a sequence of order ≥ 1

Kollár's principalization ends with an explicit monomial formula, Π^* I = 𝒪_{X_r}(−∑_{j ≥ s} Π^*_{r,j+1} F_j) [Kol07, 72], for the order-reduction part of the sequence. Here it is proved intrinsically and stage by stage: along a smooth blow-up sequence S of order ≥ 1 for (I, 1, E₀) (clauses (2′)–(4′) of [Kol07, Definition 66]) the pull-back of I to the stage i is a boundary monomial with residual the marked transform I_i (isBoundaryMonomialAt_stageMapAux): at stage 0 the empty product with residual I; from stage i to i + 1 the residual is divided exactly by the exceptional ideal (mark 1: π_i⁻¹(I_i) = I_{F_i} · I_{i+1}, MonomialStalk.lean) and the monomial part is pulled back member by member (MonomialStep.lean) — the centre Z_i has simple normal crossings with the boundary family F_i by clause (3′) at the stages ≤ i. When the last marked transform has order < 1 everywhere ([Kol07, Theorem 107 (1)]) its stalks are the unit ideal, and the pull-back of I to the last stage is a boundary monomial in the final total transform of E₀ (exists_boundaryMonomial_of_isOfOrderGe_one) — the monomial clause of the principalization for the order-reduction part. The general mark is MonomialSeqMark.lean; the clause on the total transform of the boundary in the embedded resolution uses this module (Hironaka/Resolution/Analytic/Wlo09/TotalTransformClause.lean).

theorem AnalyticManifold.FiniteSuccession.stalkIdeal_center_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin S.length) (a : (S.stage i.castSucc).carrier) : Manifold.IdealSheaf.stalkIdeal (S.center i) a = ⋯.idealSheaf.stalkIdeal a

The stalk of the centre ideal C_i is the vanishing ideal of Z_i, as is the stalk of the ideal sheaf of the closed submanifold Z_i.

theorem AnalyticManifold.FiniteSuccession.map_germMap_stalkIdeal_markedTransformSeq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I E₀ : M.IdealSheaf} (hge : S.IsOfOrderGe I 1 E₀) (i : Fin S.length) (x : (S.stage i.succ).carrier) : Ideal.map (Manifold.germMap ⇑(S.map i) ⋯ x) (Manifold.IdealSheaf.stalkIdeal (S.markedTransformSeq I 1 i.castSucc) ((S.map i) x)) = Manifold.vanishingStalk (⇑(S.map i) ⁻¹' Manifold.IdealSheaf.support (S.center i)) x ^ 1 * Manifold.IdealSheaf.stalkIdeal (S.markedTransformSeq I 1 i.succ) x

Kollár's (60.1) at mark 1 along the sequence [Kol07, (60.1)]: the marked transform I_i pulls back to the exceptional ideal of π_i times I_{i+1}, the marking legitimate by clause (4′) of [Kol07, Definition 66] (1 ≤ ord_{Z_i} I_i).

theorem AnalyticManifold.FiniteSuccession.isBoundaryMonomialAt_stageMapAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) {I : M.IdealSheaf} (hge : S.IsOfOrderGe I 1 F.idealSheaf) (i : ℕ) (hi : i < S.length + 1) (x : (M.finStages S.later ⟨i, hi⟩).carrier) : (S.totalTransformSeqFromAux F i hi).IsBoundaryMonomialAt (Manifold.IdealSheaf.pullback ⇑(S.stageMapAux i hi) ⋯ I) (S.markedTransformSeqAux I 1 i hi) x

Kollár's formula along the sequence [Kol07, 72], stage by stage: for a sequence of order ≥ 1 for (I, 1, red F), the pull-back of I to the stage i is a boundary monomial in the total transform of F at that stage with residual the marked transform I_i — the empty product at stage 0, then the step of MonomialStep.lean with the exact division π_i⁻¹(I_i) = I_{F_i} · I_{i+1}, the centre having snc with the boundary by clause (3′) at the stages ≤ i.

theorem AnalyticManifold.FiniteSuccession.exists_boundaryMonomial_of_isOfOrderGe_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) {I : M.IdealSheaf} (hge : S.IsOfOrderGe I 1 F.idealSheaf) (hlt : ∀ (x : (S.stage (Fin.last S.length)).carrier), Manifold.IdealSheaf.ord (S.markedTransformSeq I 1 (Fin.last S.length)) x < ↑1) (x : (S.stage (Fin.last S.length)).carrier) : ∃ (s : Finset (S.totalTransformSeqFrom F (Fin.last S.length)).ι) (α : (S.totalTransformSeqFrom F (Fin.last S.length)).ι → ℕ), (∀ j ∈ s, x ∈ (S.totalTransformSeqFrom F (Fin.last S.length)).hyp j) ∧ (Manifold.IdealSheaf.pullback ⇑(S.stageMap (Fin.last S.length)) ⋯ I).stalkIdeal x = ∏ j ∈ s, Manifold.vanishingStalk ((S.totalTransformSeqFrom F (Fin.last S.length)).hyp j) x ^ α j

Kollár's explicit formula at the last stage, intrinsically [Kol07, 72]: along a sequence of order ≥ 1 for (I, 1, red F) whose last marked transform has order < 1 everywhere ([Kol07, Theorem 107 (1)]), the pull-back of I along the composite is, at every point x of the last stage, a monomial in the vanishing ideals of finitely many members of the final total transform of F through x.