The order of the colon stalk of a total transform

Two steps of Kollár's argument rest on one local computation: in the proof of [Kol07, Lemma 102], the order of I_0 along E^{jk} is that of I diminished by m ("max-ord_{E^{jk}} I_0 ≤ 0"), and in the one-dimensional case of the induction [Kol07, 70], "max-ord I ⊗ 𝒪_X(Z) < max-ord I". Both concern a point a' of the blown-up manifold over the centre Y at which the blowing-up is a local analytic isomorphism, as it is for a centre of codimension one ([Kol07, Warning 20]: the blow-up of a Cartier divisor is an isomorphism). There the total transform π⁻¹(𝓘)_{a'} has the order of 𝓘_{π a'}, at most m; it lies in the m-th power of the exceptional ideal (u), u the scaling coordinate of a blow-up chart, as soon as ord_Y 𝓘 ≥ m at π a'; and the colon (π⁻¹(𝓘)_{a'} : u^m), which is the stalk of the controlled transform of (𝓘, m) and of the weak transform when m is the order of 𝓘 along the centre, is then the unit ideal: writing J = u^m · (J : u^m) gives m + ord (J : u^m) ≤ ord J ≤ m, the order being additive on the regular local stalk.

• ord_colon_totalTransform_eq_zero — the computation, as an equality of orders.

The general fact about a Noetherian local ring behind it is IsLocalRing.colon_span_singleton_pow_eq_top_of_ord_le. The result is used for the first centre of Lemma 102 (FirstStep.lean) and for the one-dimensional case (BaseCases.lean).

theorem Hironaka.Manifold.ord_colon_totalTransform_eq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {m : ℕ} {a' : M'} (hloc : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ π a') (hle : I.ord (π a') ≤ ↑m) (ha : π a' ∈ Y) (hord : ↑m ≤ hY.idealSheaf.ordAlongIdeal I (π a')) : IsLocalRing.ord (Submodule.colon ((Manifold.IdealSheaf.pullback π ⋯ I).stalkIdeal a') ↑((Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf).stalkIdeal a' ^ m)) = 0

The computation behind the proof of [Kol07, Lemma 102] ("max-ord_{E^{jk}} I_0 = max-ord_{E^{jk}} I − m ≤ 0") and the one-dimensional case of [Kol07, 70]: at a point a' over the centre where the blowing-up is a local analytic isomorphism, if ord 𝓘 ≤ m at π a' and ord_Y 𝓘 ≥ m at π a', the colon (π⁻¹(𝓘)_{a'} : I_{F,a'}^m) of the total transform by the m-th power of the exceptional ideal (the stalk of the controlled transform of (𝓘, m), and of the weak transform when m is the order along the centre) is the unit ideal, so it has order 0. The exceptional stalk is generated by the scaling coordinate u of a blow-up chart; the total transform lies in (u)^m and has the order of 𝓘 at π a', at most m; and the order is additive on the regular local stalk.