Going up: Lemma 61 along a sequence, and Remark 67

Kollár's Lemma 61 [Kol07, Lemma 61] iterated along a sequence, and his Remark 67 [Kol07, Remark 67]: along a sequence of order ≥ m for (I, m) with ord I ≤ m everywhere, every marked transform has order ≤ m everywhere, and the sequence is then of order exactly m ("the converse also holds").

• ord_birationalTransform_le_of_mem, ord_birationalTransform_le: Lemma 61 on a manifold for one blowing-up, ord_{a'} π_*^{-1}(J, m) ≤ m when m ≤ ord_Y J along the centre and ord J ≤ m everywhere. Over the centre: an adapted chart and a blow-up chart at a', Kollár's coordinates at a' (kollarCoords, the centred coordinates shifted so that a' is the origin of the chart ring) and the chart-ring map χ (exists_isChartRingHom); the stalk of the marked transform is χ(π_*^{-1}(J_a, m)) (the stalk formula for the centred coordinates, carried across the shift by chartRingEquivShift); the chart-level Lemma 61 (ord_map_transformIdeal_le_of_hasCohenChart, with a Cohen chart on the regular local ℚ-algebra 𝒪_{π a'}) bounds the order in the localisation R'_{𝔪'}; the induced local homomorphism R'_{𝔪'} → 𝒪_{a'} reflects the powers of the maximal ideal (ordFaithful_chartLocalHom, through the identification of completions), so the bound descends to the stalk. Off the centre the marked transform is the total transform and π is a local analytic isomorphism (ord_pullback_of_isLocalDiffeomorphAt).
• ord_markedTransformSeq_le: Lemma 61 iterated along the sequence.
• isOfOrder_of_isOfOrderGe_of_ord_le: Remark 67. The marked transforms are the birational transforms (the colon characterization with the exponent m on the exceptional divisor, the order along the centre being exactly m), and the order clause of [Kol07, Definition 66] holds with equality.

The algebraic counterparts are maxOrd_markedTransformSeq_le and isOrderGeSeq_iff_isOrderSeq. Remark 67 is what lets the going-up theorem conclude with a sequence of order exactly m.

theorem Hironaka.Manifold.ord_birationalTransform_le_of_mem {𝕜 : 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 π) (J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {m : ℕ} (hm : ∀ a ∈ Y, ↑m ≤ hY.idealSheaf.ordAlongIdeal J a) (hJ : ∀ (y : ↑↧M), J.ord y ≤ ↑m) {a' : M'} (haY : π a' ∈ Y) : (Manifold.MarkedIdealSheaf.birationalTransform hY h { I := J, m := m }).I.ord a' ≤ ↑m

[Kol07, Lemma 61] on a manifold, at a point over the centre: for m ≤ ord_Y J along the centre and ord J ≤ m everywhere, the marked transform π_*^{-1}(J, m) has order ≤ m at every point a' over Y. Kollár's coordinates at a', the stalk formula for the marked transform, the chart-level Lemma 61 in the localisation of the chart ring at the origin, and the order-faithfulness of the chart-ring local homomorphism.

theorem Hironaka.Manifold.ord_birationalTransform_le {𝕜 : 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 π) (J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {m : ℕ} (hm : ∀ a ∈ Y, ↑m ≤ hY.idealSheaf.ordAlongIdeal J a) (hJ : ∀ (y : ↑↧M), J.ord y ≤ ↑m) (a' : M') : (Manifold.MarkedIdealSheaf.birationalTransform hY h { I := J, m := m }).I.ord a' ≤ ↑m

[Kol07, Lemma 61] on a manifold: for m ≤ ord_Y J along the centre and ord J ≤ m everywhere, the marked transform π_*^{-1}(J, m) has order ≤ m everywhere. Over the centre this is ord_birationalTransform_le_of_mem; off the centre the marked transform is the total transform (birationalTransform_stalkIdeal_of_notMem) and π is a local analytic isomorphism there.

theorem AnalyticManifold.FiniteSuccession.ord_markedTransformSeq_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {I E₀ : M.IdealSheaf} {m : ℕ} (hge : B.IsOfOrderGe I m E₀) (hI : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord I y ≤ ↑m) (i : Fin (B.length + 1)) (x : (B.stage i).carrier) : Manifold.IdealSheaf.ord (B.markedTransformSeq I m i) x ≤ ↑m

[Kol07, Lemma 61] iterated (Kollár's "max-ord I_i ≤ m by (61)" in [Kol07, Remark 67]): along a sequence of order ≥ m for (I, m) with ord I ≤ m everywhere, every marked transform has order ≤ m everywhere. Over the centre by the chart-level Lemma 61 transported to the analytic stalk, off the centre by ord_pullback_of_isLocalDiffeomorphAt. The algebraic counterpart is maxOrd_markedTransformSeq_le.

theorem AnalyticManifold.FiniteSuccession.isOfOrder_of_isOfOrderGe_of_ord_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {I E₀ : M.IdealSheaf} {m : ℕ} (hge : B.IsOfOrderGe I m E₀) (hI : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord I y ≤ ↑m) : B.IsOfOrder I E₀ m

[Kol07, Remark 67], "the converse also holds": a sequence of order ≥ m for (I, m) with max-ord I ≤ m is a sequence of order m starting with (X, I). The marked transforms are the birational transforms (the argument of markedTransformSeq_eq_weakTransformSeq), whose order along the centres is ≥ m by hypothesis and ≤ m by ord_markedTransformSeq_le. The algebraic counterpart is the converse direction of isOrderGeSeq_iff_isOrderSeq.