Kollár's formula at mark m: the residual identity along a sequence of order ≥ m

Kollár's birational transform of a marked ideal, π_*^{-1}(I, m) := (𝒪(mF) · π^*I, m) [Kol07, (60.1)], and the explicit formula of [Kol07, 72] at a general mark: along a sequence of order ≥ m for (I, m, red F) the pull-back of I to every stage is a boundary monomial in the total transform of F with residual the marked transform at mark m — the exact division π⁻¹(J)_p = I_{F,p}^m · π_*^{-1}(J, m)_p at one blowing-up, then stage by stage. The mark-1 case is MonomialSeq.lean (stalkIdeal_totalTransform_eq_mul_birationalTransform, map_germMap_stalkIdeal_markedTransformSeq, isBoundaryMonomialAt_stageMapAux); the rounds of the resolution run at the marks d_U, …, 1 (the maximal order d_i of clause (2) of [Hir64, Main Theorem II(N), p. 176]), so the residual identity at the round's own mark is what the assembled resolution needs (the mark-1 identity for the whole list has a non-unit residual when d_U ≥ 2).

• stalkIdeal_totalTransform_eq_pow_mul_birationalTransform — (60.1) at mark m, exact, at one blowing-up (isDivExceptional_birationalTransform already carries the mark).
• FiniteSuccession.map_germMap_stalkIdeal_markedTransformSeq_of_isOfOrderGe — the same along a sequence of order ≥ m, stage by stage.
• FiniteSuccession.isBoundaryMonomialAt_stageMapAux_of_isOfOrderGe — the residual identity at mark m ([Kol07, 72] with the residual kept; isBoundaryMonomialAt_pullback with e := m).
• FiniteSuccession.isBoundaryMonomialAt_comap_stageMapAux — a boundary monomial with residual pulls back along a sequence whose centres have only normal crossings with the boundary, the residual pulled back as it is (isBoundaryMonomialAt_pullback with e := 0).
• FiniteSuccession.isOfOrderGe_zero_of_isOfOrderGe — order ≥ m gives order ≥ 0 for any ideal: at mark 0 only clause (3′) of [Kol07, Definition 66] remains.
• BlowUpSequence.pullbackIsMonomialAtLast_of_isBoundaryMonomialAt — PullbackIsMonomialAtLast is multiplicative in the ideal: if J = (monomial in F) · R at every point and the list makes R a boundary monomial at its last stage, it makes J one.

Used for the monomial clause of the assembled resolution (Hironaka/Resolution/Analytic/Wlo09/Monomial.lean).

theorem Hironaka.Manifold.stalkIdeal_totalTransform_eq_pow_mul_birationalTransform {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M M' : AnalyticManifold 𝕜 E} {π : M'.carrier → M.carrier} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (J : M.IdealSheaf) (m : ℕ) (hm : ∀ a ∈ Y, ↑m ≤ hY.idealSheaf.ordAlongIdeal J a) (p : M'.carrier) : (Manifold.IdealSheaf.pullback π ⋯ J).stalkIdeal p = (Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf).stalkIdeal p ^ m * (Manifold.MarkedIdealSheaf.birationalTransform hY h { I := J, m := m }).I.stalkIdeal p

Kollár's (60.1) at mark m, in its exact form [Kol07, (60.1)]: when ord_Y J ≥ m, the total transform of J is the m-th power of the exceptional ideal times the marked transform at mark m at every stalk, π⁻¹(J)_p = I_{F,p}^m · π_*^{-1}(J, m)_p — the marked transform's stalk is the colon (π⁻¹(J)_p : I_{F,p}^m) (isDivExceptional_birationalTransform), π⁻¹(J)_p ⊆ I_{F,p}^m because J_a ⊆ I_{Y,a}^m on the centre, and I_{F,p} is principal. The mark-1 case is stalkIdeal_totalTransform_eq_mul_birationalTransform.

theorem AnalyticManifold.FiniteSuccession.map_germMap_stalkIdeal_markedTransformSeq_of_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I E₀ : M.IdealSheaf} {m : ℕ} (hge : S.IsOfOrderGe I m 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 m i.castSucc) ((S.map i) x)) = Manifold.vanishingStalk (⇑(S.map i) ⁻¹' Manifold.IdealSheaf.support (S.center i)) x ^ m * Manifold.IdealSheaf.stalkIdeal (S.markedTransformSeq I m i.succ) x

Kollár's (60.1) at mark m along a sequence of order ≥ m (clause (4′) of [Kol07, Definition 66]): the marked transform I_i pulls back to the m-th power of the exceptional ideal of π_i times I_{i+1} (the mark-1 case is map_germMap_stalkIdeal_markedTransformSeq).

theorem AnalyticManifold.FiniteSuccession.isBoundaryMonomialAt_stageMapAux_of_isOfOrderGe {𝕜 : 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} {m : ℕ} (hge : S.IsOfOrderGe I m 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 m i hi) x

Kollár's formula [Kol07, 72] at mark m, stage by stage — the residual identity: along a sequence of order ≥ m for (I, m, 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 at mark m — the empty product at stage 0, then the step of MonomialStep.lean with the exact division π_i⁻¹(I_i) = I_{F_i}^m · I_{i+1}, the centre having snc with the boundary by clause (3′). The mark-1 case is isBoundaryMonomialAt_stageMapAux.

theorem AnalyticManifold.FiniteSuccession.isBoundaryMonomialAt_comap_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) (h3 : ∀ (i : Fin S.length), (S.boundarySeq F.idealSheaf i.castSucc).HasOnlyNormalCrossingsWith (S.center i)) {J R : M.IdealSheaf} (i : ℕ) (hi : i < S.length + 1) (x : (M.finStages S.later ⟨i, hi⟩).carrier) : F.IsBoundaryMonomialAt J R ((S.stageMapAux i hi) x) → (S.totalTransformSeqFromAux F i hi).IsBoundaryMonomialAt (Manifold.IdealSheaf.pullback ⇑(S.stageMapAux i hi) ⋯ J) (Manifold.IdealSheaf.pullback ⇑(S.stageMapAux i hi) ⋯ R) x

A boundary monomial with residual pulls back along a sequence whose centres have only normal crossings with the boundary (clause (3′) of [Kol07, Definition 66]): at a point of stage i, if J = (monomial in F) · R at its image, then π_i^* J = (monomial in the total transform of F) · π_i^* R — isBoundaryMonomialAt_pullback with e := 0, the residual pulled back as it is.

theorem AnalyticManifold.FiniteSuccession.isOfOrderGe_zero_of_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I I' E₀ : M.IdealSheaf} {m : ℕ} (hge : S.IsOfOrderGe I m E₀) : S.IsOfOrderGe I' 0 E₀

Order ≥ m gives order ≥ 0 for any ideal: at mark 0 only clause (3′) of [Kol07, Definition 66] — the centres have only normal crossings with the boundary — remains.

theorem AnalyticManifold.BlowUpSequence.pullbackIsMonomialAtLast_of_isBoundaryMonomialAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (h3 : ∀ (i : Fin L.toSuccession.length), (L.toSuccession.boundarySeq F.idealSheaf i.castSucc).HasOnlyNormalCrossingsWith (L.toSuccession.center i)) {J R : M.IdealSheaf} (hJR : ∀ (p : M.carrier), F.IsBoundaryMonomialAt J R p) (hR : L.PullbackIsMonomialAtLast F R) : L.PullbackIsMonomialAtLast F J

PullbackIsMonomialAtLast is multiplicative in the ideal: if J = (monomial in F) · R at every point and the list makes R a boundary monomial at its last stage, it makes J one — isBoundaryMonomialAt_comap_stageMapAux at the last stage, then the product of two boundary monomials in the same family is one (the exponents add over the union of the index sets).