Kollár's Lemma 62 along a succession, and the going-down property of maximal contact

Kollár's Lemma 62 iterated along the restriction of a succession Π to a closed submanifold S whose strict transforms contain the centres ([Kol07, Definition 30.2] and [Kol07, Lemma 62]): the marked transforms of (J|_S, m) along Π|_S are the restrictions of the marked transforms of (J, m) along Π (markedTransformSeq_pullback_restrictIncl, induction on the stage with birationalTransform_pullback_restrictMap at each step). Hence the going-down property of maximal contact [Kol07, 51.1]: the order clause (4′) of [Kol07, Definition 66] for Π|_S and (J|_S, m) — the order can only go up under restriction (the opening remark of [Kol07, §9]), and the marked transforms of Π|_S are restrictions (le_ordAlong_restrictSubmanifold).

Two bookkeeping facts make the induction typecheck on FiniteSuccession: the ideal sheaf of a closed submanifold does not depend on the chart or the codimension of the submanifold predicate (IsClosedSubmanifold.idealSheaf_congr; idealSheaf_eq_of_set below is its same-set corollary), so the marked transform depends only on the centre as a set and on the blow-down (MarkedIdealSheaf.birationalTransform_congr); and the centre of the restriction at step i is the pull-back of C_i (center_restrictSubmanifold).

theorem Manifold.IsClosedSubmanifold.idealSheaf_eq_of_set {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n n' : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {ψ' : E ≃L[𝕜] Fin n' → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c c' : ℕ} (hY : IsClosedSubmanifold ψ Y c) (hY' : IsClosedSubmanifold ψ' Y c') : hY.idealSheaf = hY'.idealSheaf

The ideal sheaf of a closed submanifold depends neither on the chart ψ nor on the codimension of the submanifold predicate: the same-set case of IsClosedSubmanifold.idealSheaf_congr.

theorem Hironaka.Manifold.le_ordAlongIdeal_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] {D K : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)} (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) {b : N} {m : ℕ} (hm : ↑m ≤ D.ordAlongIdeal K (φ b)) : ↑m ≤ (Manifold.IdealSheaf.pullback φ hφ D).ordAlongIdeal (Manifold.IdealSheaf.pullback φ hφ K) b

The order along a centre under pull-back: if m ≤ ord_D K at φ b, then m ≤ ord_{φ⁻¹D} (φ⁻¹K) at b — pulling back is a ring map on stalks, so K_{φ b} ⊆ D_{φ b}^m gives (φ⁻¹K)_b ⊆ (φ⁻¹D)_b^m (the order can only go up under restriction, the opening remark of [Kol07, §9]).

theorem AnalyticManifold.FiniteSuccession.isClosedSubmanifold_preimage_center {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : Fin S.length) : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑(S.restrictIncl hH hc i.castSucc) ⁻¹' Manifold.IdealSheaf.support (S.center i)) (S.codim i - s)

Kollár's Z_i ∩ S_i as a closed submanifold of the stage S_i of the restriction, in the induced chart and of codimension c_i − s (restrictCenterSub' typed on the stages of the succession).

theorem AnalyticManifold.FiniteSuccession.restrictCenterOf_eq_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : ℕ) (hi : i < S.length) : S.restrictCenterOf hH hc i hi = Manifold.IdealSheaf.pullback ⇑⋯.inclusionMap ⋯ (S.center ⟨i, hi⟩)

The centre of the restriction at step i, at the recursion level: the pull-back of C_i under the embedding S_i ↪ M_i (idealSheaf_preimageVal_eq_pullback).

theorem AnalyticManifold.FiniteSuccession.center_restrictSubmanifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : Fin S.length) : (S.restrictSubmanifold hH hc).center i = Manifold.IdealSheaf.pullback ⇑(S.restrictIncl hH hc i.castSucc) ⋯ (S.center i)

The centre of Π|_S at step i is the pull-back of the centre C_i of Π under the embedding S_i ↪ M_i (Kollár's Z_i ∩ S_i, [Kol07, Definition 30.2]).

theorem AnalyticManifold.FiniteSuccession.birationalTransform_restrict_step {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : Fin S.length) (K : (S.stage i.castSucc).IdealSheaf) {m : ℕ} (hm : ∀ a ∈ Manifold.IdealSheaf.support (S.center i), ↑m ≤ Manifold.IdealSheaf.ordAlongIdeal (S.center i) K a) : (Manifold.MarkedIdealSheaf.birationalTransform ⋯ ⋯ { I := Manifold.IdealSheaf.pullback ⇑(S.restrictIncl hH hc i.castSucc) ⋯ K, m := m }).I = Manifold.IdealSheaf.pullback ⇑(S.restrictIncl hH hc i.succ) ⋯ (Manifold.MarkedIdealSheaf.birationalTransform ⋯ ⋯ { I := K, m := m }).I

The inductive step: Kollár's Lemma 62 at stage i of the succession, read on the stages of the succession — the marked transform under π_i|_{S_{i+1}} of the restriction of (K, m) is the restriction of the marked transform under π_i, for a mark m legitimate along Z_i ([Kol07, Lemma 62]).

theorem AnalyticManifold.FiniteSuccession.markedTransformSeq_pullback_restrictIncl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) {J E₀ : M.IdealSheaf} {m : ℕ} (hge : S.IsOfOrderGe J m E₀) (i : Fin (S.length + 1)) : (S.restrictSubmanifold hH hc).markedTransformSeq (Manifold.IdealSheaf.pullback ⇑hH.inclusionMap ⋯ J) m i = Manifold.IdealSheaf.pullback ⇑(S.restrictIncl hH hc i) ⋯ (S.markedTransformSeq J m i)

Kollár's Lemma 62 iterated along the restriction of a blow-up sequence ([Kol07, Lemma 62] and [Kol07, Definition 30.2]): for Π of order ≥ m for (J, m) with centres in the strict transforms S_i of S, the marked transform of (J|_S, m) along Π|_S is, at every stage, the restriction under S_i ↪ M_i of the marked transform of (J, m) along Π. Induction on the stage; the order clause (4′) of Π makes the mark legitimate at each step.

theorem AnalyticManifold.FiniteSuccession.le_ordAlong_restrictSubmanifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) {J E₀ : M.IdealSheaf} {m : ℕ} (hge : S.IsOfOrderGe J m E₀) (i : Fin S.length) (a : ↑↧(hH.toAnalyticManifold.finStages (S.restrictSubmanifold hH hc).later i.castSucc).carrier) : a ∈ Manifold.IdealSheaf.support ((S.restrictSubmanifold hH hc).center i) → ↑m ≤ Manifold.IdealSheaf.ordAlongIdeal ((S.restrictSubmanifold hH hc).center i) ((S.restrictSubmanifold hH hc).markedTransformSeq (Manifold.IdealSheaf.pullback ⇑hH.inclusionMap ⋯ J) m i.castSucc) a

The going-down property of maximal contact [Kol07, 51.1] — the order clause (4′) of [Kol07, Definition 66] for Π|_S: the marked transforms of (J|_S, m) along Π|_S have order ≥ m along the centres Z_i ∩ S_i at every point — they are the restrictions of the marked transforms of Π (markedTransformSeq_pullback_restrictIncl), the centres of Π|_S are the restrictions of the centres of Π, and the order can only go up under restriction.

theorem AnalyticManifold.FiniteSuccession.isOfOrderGe_restrictSubmanifold_of_hasOnlyNormalCrossingsWith {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) {J : M.IdealSheaf} {m : ℕ} (hge : S.IsOfOrderGe J m ⊤) (hnc : ∀ (i : Fin S.length), ((S.restrictSubmanifold hH hc).boundarySeq ⊤ i.castSucc).HasOnlyNormalCrossingsWith ((S.restrictSubmanifold hH hc).center i)) : (S.restrictSubmanifold hH hc).IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hH.inclusionMap ⋯ J) m ⊤

The assembly of [Kol07, Definition 66] for Π|_S from its two clauses: given the normal-crossings clause (3′) for the boundary of Π|_S, the restricted succession is of order ≥ m for (J|_S, m) with the empty boundary — the order clause (4′) is le_ordAlong_restrictSubmanifold.