Going up: the marked transform along the push-forward

The restriction of the push-forward is the given sequence, read on the marked transforms. For Π = j_* T the push-forward [Kol07, 30.3] of a sequence T on the closed submanifold S ⊆ M and J an ideal sheaf on M, the marked transform of (J, m) along Π, restricted to S_i through the embedding j_i : T_i ↪ X_i (pushforwardIncl), is the marked transform of (J|_S, m) along T, as soon as the marked transforms of Π have order ≥ m along the centres of the steps before the stage (the order clause (4′) of [Kol07, Definition 66] on the prefix). The algebraic counterpart is pullback_pushforward.

• PushforwardStage.birationalTransform_pullback_incl_blowUpStep, the step: with j_{i+1} = ι_{S_{i+1}} ∘ e_{i+1} (blowUpStep), the one-blowing-up Lemma 62 [Kol07, Lemma 62] handles ι_{S_{i+1}} (the marked transform restricts to the strict transform S_{i+1}), the invariance birationalTransform_pullback_of_comp_eq handles e_{i+1} (the unique diffeomorphism over S_i between the given blowing-up e_i ∘ π_i^T and the restricted blow-down), and the base change birationalTransform_image_diffeomorph handles e_i.
• birationalTransform_pushforward_step: the step read on the sequence's own data (the chosen charts, the centres Z_i^X = j_i(Z_i) by support_pushforwardCenterOf).
• markedTransformSeq_pullback_pushforwardIncl_of_forall_lt: the identity at a stage i from the order clause (4′) of Π on the steps before i, the form used inside the induction of Kollár's proof of Theorem 84 (a prefix-bounded hypothesis rather than a truncated sequence, whose stage types would not be definitionally those of Π); markedTransformSeq_pullback_pushforwardIncl is its corollary for Π of order ≥ m.

The proof is an induction on the stage with the one-blowing-up Lemma 62, as for the restriction of a sequence to a submanifold in Hironaka/Manifold/Sequence/Restrict/.

theorem Manifold.PushforwardStage.birationalTransform_pullback_incl_blowUpStep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ T' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s Tᵢ) {Z : Set Tᵢ.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) {π : AnalyticMap T' Tᵢ} (hπ : IsBlowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c ⇑π) (A : P.space.IdealSheaf) {m : ℕ} (hm : ∀ a ∈ ⋯.imageVal (⇑P.iso '' Z), ↑m ≤ ⋯.idealSheaf.ordAlongIdeal A a) : IdealSheaf.pullback ⇑(P.blowUpStep hZ hπ).incl ⋯ (MarkedIdealSheaf.birationalTransform ⋯ ⋯ { I := A, m := m }).I = (MarkedIdealSheaf.birationalTransform hZ hπ { I := IdealSheaf.pullback ⇑P.incl ⋯ A, m := m }).I

The step of the push-forward identity at one stage ([Kol07, 30.3] with [Kol07, Lemma 62]): for the stage data P = (X_i, S_i, e_i) and a blowing-up π : T' → T_i along Z, the marked transform of (A, m) along the blowing-up X_{i+1} → X_i of Z_i^X = j_i(e_i(Z)), pulled back along j_{i+1} = ι_{S_{i+1}} ∘ e_{i+1}, is the marked transform of (j_i^* A, m) along π: Lemma 62 for ι_{S_{i+1}}, the invariance under the unique diffeomorphism e_{i+1} over S_i, the base change along e_i.

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

The step of the push-forward identity on the sequence's own data: the marked transform of (K, m) along the i-th blow-down of the push-forward, pulled back along j_{i+1}, is the marked transform of (j_i^* K, m) along the i-th blow-down of T, for K of order ≥ m along the centre Z_i^X. The centre of the push-forward is j_i(Z_i) (support_pushforwardCenterOf) and its blow-down the blowing-up along it; a case split on the index, as in the definition of the push-forward.

theorem AnalyticManifold.FiniteSuccession.markedTransformSeq_pullback_pushforwardIncl_of_forall_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (J : M.IdealSheaf) {m k : ℕ} (h4 : ∀ (i : Fin T.length), ↑i < k → ∀ a ∈ Manifold.IdealSheaf.support ((pushforward hS T).center i), ↑m ≤ Manifold.IdealSheaf.ordAlongIdeal ((pushforward hS T).center i) ((pushforward hS T).markedTransformSeq J m i.castSucc) a) (i : Fin (T.length + 1)) (hi : ↑i ≤ k) : Manifold.IdealSheaf.pullback ⇑(pushforwardIncl hS T i) ⋯ ((pushforward hS T).markedTransformSeq J m i) = T.markedTransformSeq (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J) m i

The push-forward identity in its working form: for a stage i such that the marked transforms of (J, m) along the push-forward have order ≥ m along the centres of the steps before i (the order clause (4′) on the prefix), the marked transform of (J, m) along the push-forward at stage i, restricted to S_i through j_i, is the marked transform of (J|_S, m) along T. Induction on the stage with birationalTransform_pushforward_step.

theorem AnalyticManifold.FiniteSuccession.markedTransformSeq_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) {E₀ : M.IdealSheaf} {m : ℕ} (J : M.IdealSheaf) (hge : (pushforward hS T).IsOfOrderGe J m E₀) (i : Fin (T.length + 1)) : Manifold.IdealSheaf.pullback ⇑(pushforwardIncl hS T i) ⋯ ((pushforward hS T).markedTransformSeq J m i) = T.markedTransformSeq (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J) m i

The restriction of the push-forward is the given sequence, read on the marked transforms ([Kol07, 30.2–30.3]; the algebraic counterpart is pullback_pushforward): for Π = j_* T of order ≥ m for (J, m), the marked transform of (J, m) along Π restricted to S_i through the embedding j_i : T_i ↪ X_i (pushforwardIncl) is the marked transform of (J|_S, m) along T. Induction on the stage with the one-blowing-up Lemma 62 [Kol07, Lemma 62], the stage S_i ⊆ X_i being identified with T_i by the unique diffeomorphism between two blowings-up of one centre [BM88, Definition 4.1], along which the colon stalks correspond. The centres correspond by support_center_pushforward. The order clause (4′) of Π is all that the induction uses (markedTransformSeq_pullback_pushforwardIncl_of_forall_lt).