Going up: the order bookkeeping of Kollár's proof of Theorem 84

The tools of the induction in Kollár's proof of the going-up theorem [Kol07, 90], on analytic manifolds: the elementary properties of the cosupport of a marked ideal sheaf [Kol07, Definition 59] along a blow-up sequence, and the passage from orders at points to the order along a pushed-forward centre. The algebraic counterparts are cosupp_pow, cosupp_markedTransformSeq_subset_of_le, cosupp_markedTransformSeq_pow, cosupp_markedTransformSeq_subset_iInter and ordAlongEq_map_of_cosupp_subset.

• setOf_le_ord_pow: cosupp(A^s, c s) = cosupp(A, c) for s ≥ 1 (property (3) of the cosupport in [Kol07, Definition 59]), read on the sets {x | c ≤ ord_x} with ord_pow.
• IsOfOrderGe.isOfOrderGe_pow: a sequence of order ≥ m for (I, m) is of order ≥ m s for (I^s, m s); the marked transforms are the powers (markedTransformSeq_pow).
• IsOfOrderGe.markedTransformSeq_le_of_le, setOf_le_ord_markedTransformSeq_subset_of_le: the marked transform along a sequence is monotone in the ideal sheaf (birationalTransform_mono stage by stage), so its cosupport is antitone (property (1) of the cosupport).
• setOf_le_ord_markedTransformSeq_pow: cosupp Π_*^{-1}(I^s, m s) = cosupp Π_*^{-1}(I, m) at every stage.
• setOf_le_ord_markedTransformSeq_subset_iInter: for I D-balanced and T of order ≥ m for (I|_S, m), cosupp T_*^{-1}(I|_S, m) ⊆ ⋂_{j<m} cosupp T_*^{-1}((D^j I)|_S, m − j) at every stage: the D-balanced inclusion (D^j I)^m ⊆ I^{m−j} pulled back to S, the power rule and pow_markedTransformSeq_le give m · ord T_*^{-1}((D^j I)|_S, m − j) ≥ (m − j) · ord T_*^{-1}(I|_S, m) ≥ (m − j) m.
• le_ordAlong_pushforward_center_of_setOf_le_ord_subset: at a step of T whose centre Z_i has order ≥ m for J and whose points of order ≥ m for J map to points of order ≥ m for A, the order of A along the pushed-forward centre j_i(Z_i) is ≥ m, since the order along a centre at a is determined by the orders at the nearby points of the centre (stalkIdeal_le_pow_of_eventually_le_ord).

Kollár's Lemma 61 iterated and Remark 67 are in Hironaka/Resolution/Analytic/GoingUp/MaxOrder.lean; the induction itself is le_ordAlong_pushforward in GoingUp/Corollary89.lean.

theorem Hironaka.Manifold.setOf_le_ord_pow {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (A : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {s : ℕ} (hs : 1 ≤ s) (c : ℕ) : {x : M | ↑(c * s) ≤ (A ^ s).ord x} = {x : ↑↧M | ↑c ≤ A.ord x}

cosupp(A^s, cs) = cosupp(A, c) for s ≥ 1 (property (3) of the cosupport in [Kol07, Definition 59]): ord_pow read on the sets {x | c ≤ ord_x}.

Along one sequence

theorem AnalyticManifold.FiniteSuccession.IsOfOrderGe.isOfOrderGe_pow {𝕜 : 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₀) (s : ℕ) : B.IsOfOrderGe (I ^ s) (m * s) E₀

A sequence of order ≥ m for (I, m) is of order ≥ m·s for (I^s, m·s) (the order bookkeeping of the power rule, the second line of Kollár's computation in [Kol07, 90]): the marked transforms of the power are the powers (markedTransformSeq_pow), whose order along the centres is s times the order.

theorem AnalyticManifold.FiniteSuccession.IsOfOrderGe.markedTransformSeq_le_of_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {E₀ A A' : M.IdealSheaf} (hAA' : A ≤ A') {c : ℕ} (hA' : B.IsOfOrderGe A' c E₀) (i : Fin (B.length + 1)) : B.markedTransformSeq A c i ≤ B.markedTransformSeq A' c i

The marked transform along a sequence is monotone in the ideal sheaf, the larger ideal being of order ≥ c along the centres: birationalTransform_mono stage by stage (the third line of Kollár's computation in [Kol07, 90]).

theorem AnalyticManifold.FiniteSuccession.setOf_le_ord_markedTransformSeq_subset_of_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {E₀ A A' : M.IdealSheaf} (hAA' : A ≤ A') {c : ℕ} (hA' : B.IsOfOrderGe A' c E₀) (i : Fin (B.length + 1)) : {x : (B.stage i).carrier | ↑c ≤ Manifold.IdealSheaf.ord (B.markedTransformSeq A' c i) x} ⊆ {x : (B.stage i).carrier | ↑c ≤ Manifold.IdealSheaf.ord (B.markedTransformSeq A c i) x}

The marked transform along a sequence is monotone in the ideal sheaf, so the cosupport is antitone (property (1) of the cosupport in [Kol07, Definition 59]): A ≤ A' gives cosupp Π_*^{-1}(A', c) ⊆ cosupp Π_*^{-1}(A, c) at every stage.

theorem AnalyticManifold.FiniteSuccession.setOf_le_ord_markedTransformSeq_pow {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {I E₀ : M.IdealSheaf} {m : ℕ} (hge : B.IsOfOrderGe I m E₀) {s : ℕ} (hs : 1 ≤ s) (i : Fin (B.length + 1)) : {x : (B.stage i).carrier | ↑(m * s) ≤ Manifold.IdealSheaf.ord (B.markedTransformSeq (I ^ s) (m * s) i) x} = {x : ↑↧(B.stage i).carrier | ↑m ≤ Manifold.IdealSheaf.ord (B.markedTransformSeq I m i) x}

Along a sequence of order ≥ m for (I, m), cosupp Π_*^{-1}(I^s, m s) = cosupp Π_*^{-1}(I, m) at every stage, for s ≥ 1 (lines 2 and 4 of Kollár's computation in [Kol07, 90]): markedTransformSeq_pow with setOf_le_ord_pow.

The hypersurface side of the induction

theorem AnalyticManifold.FiniteSuccession.setOf_le_ord_markedTransformSeq_subset_iInter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (T : hS.toAnalyticManifold.FiniteSuccession) {I : M.IdealSheaf} {m : ℕ} (hI : Manifold.IdealSheaf.IsDBalanced I m) {E' : hS.toAnalyticManifold.IdealSheaf} (hT : T.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) m E') (i : Fin (T.length + 1)) : {y : (T.stage i).carrier | ↑m ≤ Manifold.IdealSheaf.ord (T.markedTransformSeq (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) m i) y} ⊆ ⋂ (j : ℕ), ⋂ (_ : j < m), {y : (T.stage i).carrier | ↑(m - j) ≤ Manifold.IdealSheaf.ord (T.markedTransformSeq (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ (Manifold.IdealSheaf.iteratedDeriv I j)) (m - j) i) y}

For I D-balanced and T a sequence on the hypersurface S of order ≥ m for (I|_S, m), at every stage cosupp T_*^{-1}(I|_S, m) ⊆ ⋂_{j<m} cosupp T_*^{-1}((D^j I)|_S, m − j) (the use of the D-balanced property in Kollár's computation in [Kol07, 90]): (D^j I)^m ⊆ I^{m−j}, pulled back to S, the power rule and pow_markedTransformSeq_le ((T_*^{-1}((D^j I)|_S, m−j))^m ⊆ T_*^{-1}((I|_S)^{m−j}, m(m−j))), whence m · ord T_*^{-1}((D^j I)|_S, m−j) ≥ (m−j) · ord T_*^{-1}(I|_S, m) ≥ (m−j) m.

theorem AnalyticManifold.FiniteSuccession.le_ordAlong_pushforward_center_of_setOf_le_ord_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (T : hS.toAnalyticManifold.FiniteSuccession) {m : ℕ} (i : Fin T.length) {A : ((pushforward hS T).stage i.castSucc).IdealSheaf} {J : (T.stage i.castSucc).IdealSheaf} (hJ : ∀ a ∈ Manifold.IdealSheaf.support (T.center i), ↑m ≤ Manifold.IdealSheaf.ordAlongIdeal (T.center i) J a) (hsub : ∀ (y : ↑↧(T.stage i.castSucc).carrier), ↑m ≤ Manifold.IdealSheaf.ord J y → ↑m ≤ Manifold.IdealSheaf.ord A ((pushforwardIncl hS T i.castSucc) y)) (a : ↑↧(M.finStages (pushforward hS T).later i.castSucc).carrier) : a ∈ Manifold.IdealSheaf.support ((pushforward hS T).center i) → ↑m ≤ Manifold.IdealSheaf.ordAlongIdeal ((pushforward hS T).center i) A a

At a step i of T with centre Z_i ⊆ S_i, if J has order ≥ m along Z_i and the points of S_i where J has order ≥ m map to points where A has order ≥ m, then A has order ≥ m along the pushed-forward centre j_i(Z_i) (Kollár's "the last blow-up also has order ≥ m, or, equivalently, cosupp(J_{r−1}, m) ⊆ cosupp(I_{r−1}, m)" in [Kol07, 90]): the order along a centre is the order at the points of its component through the point, and every point of j_i(Z_i) is j_i(y) with y ∈ Z_i, where m ≤ ord_{Z_i} J ≤ ord_y J.