Going up: Corollary 89 on the push-forward and the order clause of Theorem 84

Kollár's Corollary 89 [Kol07, Corollary 89] for the push-forward Π = j_* T of a sequence T on the smooth hypersurface S, read on the stages of T through the embeddings j_i : T_i ↪ X_i, and the induction of Kollár's proof of the going-up theorem [Kol07, 90]: the order clause (4′) of the push-forward.

• PushforwardStage.logDerivIter_pullback_incl, logDerivIter_pullback_pushforwardIncl: the restriction identity (87.1) of [Kol07, 87] along j_i: the restriction to T_i of D^r(−log S_i)(J) is the r-th derivative of the restriction (logDerivIter_pullback_inclusionMap along ι_{S_i}, then the locality of D along the diffeomorphism e_i).
• le_ordAlong_markedTransformSeq_iteratedDeriv_of_forall_lt: the order clause of [Kol07, Corollary 77] on a prefix (the prefix-bounded form of IsOfOrderGe.isOfOrderGe_iteratedDeriv).
• setOf_le_ord_markedTransformSeq_pushforward_inter_eq_iInter_of_forall_lt: Corollary 89 on the push-forward at a stage i, from the order clause (4′) of Π on the steps before i: {y ∈ T_i | ord_{j_i y} Π_*^{-1}(I, m) ≥ m} = ⋂_{j<m} cosupp T_*^{-1}((D^j I)|_S, m − j). The prefix-bounded Theorem 88 on Π, restricted to T_i summand by summand with (87.1) and the push-forward identity, then cosupp(I, m) = cosupp(D^{m−1}(I), 1) [Kol07, Lemma 74 (3)] and the cosupport of a sum [Kol07, Definition 59], as for Corollary 89 itself in Hironaka/Resolution/Analytic/LogDerivSequence.lean; setOf_le_ord_markedTransformSeq_pushforward_inter_eq_iInter is its form for Π of order ≥ m.
• le_ordAlong_pushforward (the order half of [Kol07, Theorem 84], Kollár's item 90): for I D-balanced with ord I ≤ m everywhere and T of order ≥ m for (I|_S, m) (any boundary), Π has order ≥ m for (I, m) along every centre. Induction on the stage: Corollary 89 for the prefix, the D-balanced inclusion (setOf_le_ord_markedTransformSeq_subset_iInter) and the order along the pushed-forward centre (le_ordAlong_pushforward_center_of_setOf_le_ord_subset).

The normal-crossings clause of the push-forward and the assembly of Theorem 84 are in GoingUp/Theorem84.lean.

theorem Manifold.PushforwardStage.logDerivIter_pullback_incl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Tᵢ : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} (P : PushforwardStage ψ 1 Tᵢ) {S' : Set P.space.carrier} (hS' : IsClosedSubmanifold ψ S' 1) (hset : S' = P.sub) (r : ℕ) (J : P.space.IdealSheaf) : IdealSheaf.pullback ⇑P.incl ⋯ (IdealSheaf.logDerivIter E ψ hS' r J) = (IdealSheaf.pullback ⇑P.incl ⋯ J).iteratedDeriv r

The restriction identity (87.1) of [Kol07, 87] along j_i = ι_{S_i} ∘ e_i at one stage of the push-forward: for the hypersurface S' = S_i of X_i, the restriction to T_i of D^r(−log S')(J) is the r-th derivative of the restriction (logDerivIter_pullback_inclusionMap along ι_{S_i} and iteratedDeriv_pullback_of_isLocalDiffeomorph along the diffeomorphism e_i).

Corollary 77's order clause on a prefix

theorem AnalyticManifold.FiniteSuccession.le_ordAlong_markedTransformSeq_iteratedDeriv_of_forall_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {I : M.IdealSheaf} {m j : ℕ} (hj : j ≤ m) (k : ℕ) (h4 : ∀ (i : Fin B.length), ↑i < k → ∀ a ∈ Manifold.IdealSheaf.support (B.center i), ↑m ≤ Manifold.IdealSheaf.ordAlongIdeal (B.center i) (B.markedTransformSeq I m i.castSucc) a) (i : Fin B.length) : ↑i < k → ∀ a ∈ Manifold.IdealSheaf.support (B.center i), ↑(m - j) ≤ Manifold.IdealSheaf.ordAlongIdeal (B.center i) (B.markedTransformSeq (Manifold.IdealSheaf.iteratedDeriv I j) (m - j) i.castSucc) a

[Kol07, Corollary 77] on a prefix: the order clause of IsOfOrderGe.isOfOrderGe_iteratedDeriv from the order clause (4′) alone. If the marked transforms of (I, m) have order ≥ m along the centres of the steps before k, the marked transforms of (D^j I, m − j) have order ≥ m − j along those centres.

Corollary 89 on the push-forward

theorem AnalyticManifold.FiniteSuccession.logDerivIter_pullback_pushforwardIncl {𝕜 : 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) (i : Fin (T.length + 1)) (r : ℕ) (J : ((pushforward hS T).stage i).IdealSheaf) : Manifold.IdealSheaf.pullback ⇑(pushforwardIncl hS T i) ⋯ (Manifold.IdealSheaf.logDerivIter E ψ ⋯ r J) = (Manifold.IdealSheaf.pullback ⇑(pushforwardIncl hS T i) ⋯ J).iteratedDeriv r

The restriction identity (87.1) of [Kol07, 87] along the inclusions j_i : T_i ↪ X_i of the push-forward: the restriction to T_i of D^r(−log S_i)(J) is the r-th derivative of the restriction; the strict transform S_i of the push-forward is the stage data's S_i (strictTransformSeqAux_pushforward_succ).

theorem AnalyticManifold.FiniteSuccession.setOf_le_ord_markedTransformSeq_pushforward_inter_eq_iInter_of_forall_lt {𝕜 : 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 : ℕ} (hm : 1 ≤ m) (i : Fin (T.length + 1)) (h4 : ∀ (i' : Fin T.length), ↑i' < ↑i → ∀ a ∈ Manifold.IdealSheaf.support ((pushforward hS T).center i'), ↑m ≤ Manifold.IdealSheaf.ordAlongIdeal ((pushforward hS T).center i') ((pushforward hS T).markedTransformSeq I m i'.castSucc) a) : {y : (T.stage i).carrier | ↑m ≤ Manifold.IdealSheaf.ord ((pushforward hS T).markedTransformSeq I m i) ((pushforwardIncl hS T 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}

Corollary 89 on the push-forward [Kol07, Corollary 89], at a stage i from the order clause (4′) of Π = j_* T on the steps before i (the working form inside the induction of Kollár's proof of Theorem 84): on T_i, the points where the marked transform of (I, m) along Π has order ≥ m are those where every marked transform of ((D^j I)|_S, m − j) along T has order ≥ m − j. The prefix-bounded Theorem 88 on Π at the stage i, its summands restricted to T_i by (87.1) along j_i and the push-forward identity for (D^j I, m − j) (Corollary 77's order clause on the prefix), then cosupp(I, m) = cosupp(D^{m−1}(I), 1) [Kol07, Lemma 74 (3)] and the cosupport of a sum: the proof of Corollary 89 in Hironaka/Resolution/Analytic/LogDerivSequence.lean read through j_i.

theorem AnalyticManifold.FiniteSuccession.setOf_le_ord_markedTransformSeq_pushforward_inter_eq_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 E₀ : M.IdealSheaf} {m : ℕ} (hge : (pushforward hS T).IsOfOrderGe I m E₀) (hm : 1 ≤ m) (i : Fin (T.length + 1)) : {y : (T.stage i).carrier | ↑m ≤ Manifold.IdealSheaf.ord ((pushforward hS T).markedTransformSeq I m i) ((pushforwardIncl hS T 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}

Corollary 89 on the push-forward [Kol07, Corollary 89], read on the stages of T: for Π = j_* T of order ≥ m for (I, m), 1 ≤ m, at every stage i, the points of T_i whose image in X_i lies in cosupp Π_*^{-1}(I, m) are the points of ⋂_{j<m} cosupp T_*^{-1}((D^j I)|_S, m − j): Corollary 89 on Π, its right side carried to the stages of T by the push-forward identity stage by stage (the order clause (4′) of hge is all that is used: setOf_le_ord_markedTransformSeq_pushforward_inter_eq_iInter_of_forall_lt). The algebraic counterpart is cosupp_markedTransformSeq_pushforward_inter_eq_iInter.

The order clause of the push-forward

theorem AnalyticManifold.FiniteSuccession.le_ordAlong_pushforward {𝕜 : 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) (_hmax : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord I y ≤ ↑m) {E' : hS.toAnalyticManifold.IdealSheaf} (hT : T.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) m E') (i : Fin T.length) (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) ((pushforward hS T).markedTransformSeq I m i.castSucc) a

The order half of the going-up theorem [Kol07, Theorem 84], Kollár's induction [Kol07, 90]: for I D-balanced with ord I ≤ m everywhere, S a smooth hypersurface and T a sequence of order ≥ m for (I|_S, m) (any boundary), the pushed-forward sequence j_* T has order ≥ m for (I, m) along every centre, i.e. clause (4′) of [Kol07, Definition 66] at every stage. Induction on the stage: Corollary 89 for the prefix of j_* T read on the stages of T, then the D-balanced property and the order along the pushed-forward centre. The hypothesis _hmax : ∀ y, I.ord y ≤ m is Kollár's m = max-ord I of Theorem 84 and is kept so that this half carries the hypotheses of the theorem it serves; the proof does not need it, because Kollár's induction uses only the D-balanced property, the bound entering only in the passage from order ≥ m to order exactly m ([Kol07, Remark 67], pushforward_isOfOrder). The algebraic counterpart is IsDBalanced.isOrderSeq_pushforward.