Kollár's Theorem 84: the normal-crossings clause of the push-forward, and the theorem

The going-up theorem [Kol07, Theorem 84] lifts a smooth blow-up sequence T of order ≥ m for (I|_S, m) on a hypersurface S ⊆ X to the push-forward Π = j_* T of order ≥ m for (I, m) on X, when I is D-balanced with max-ord I = m. The order clause (4′) is Kollár's induction [Kol07, 90] (le_ordAlong_pushforward in GoingUp/Corollary89.lean); this module proves the normal-crossings clause (3′), that the centre Z_i^X = j_i(Z_i) of the push-forward has only normal crossings with the boundary E_i^X of the push-forward at every stage, and assembles the theorem.

Kollár argues the order clause only (his items 86–90) and states in [Kol07, 30.3] that the push-forward of a smooth blow-up sequence is smooth, without further argument; the clause is proved here from the restriction of sequences [Kol07, 30.2] and Hironaka's reduced boundary [Hir64, Main Theorem II′(N), p. 156]. The boundary E_i^X is the reduced ideal sheaf of the family F_i^X of exceptional divisors, which has simple normal crossings with the strict transform S_i properly, and its trace on S_i is, through the identification e_i : T_i ≃ S_i, the boundary of T; clause (3′) of T at stage i transports along e_i (HasOnlyNormalCrossingsWith.pullback_diffeomorph) to the trace level and lifts to X_i by hasSncWith_of_hasSncWith_traceFamily. The induction on the stage is the point: the identification of E_i^X with F_i^X and of its trace with the boundary of Π|_S (in the prefix-bounded forms …_of_forall_lt of Hironaka/Manifold/FiniteSuccession/BoundaryFamily.lean and Restrict/BoundaryTrace.lean) uses clause (3′) at the stages < i only, so the argument closes stage by stage.

• hasOnlyNormalCrossingsWith_idealSheaf_of_traceFamily: for one closed submanifold, clause (3′) at the trace level implies clause (3′) in the ambient manifold.
• pushforward_hasOnlyNormalCrossingsWith_center_of_forall_lt: the stage step.
• pushforward_hasOnlyNormalCrossingsWith_center: clause (3′) of the push-forward.
• pushforward_isOfOrderGe, pushforward_isOfOrder, pushforward_isOfOrder_of_not_subset_cosupp: Theorem 84 in the ≥ m form, with the exact order (by [Kol07, Remark 67]), and as printed.

Together with going down [Kol07, 51.1] this yields Kollár's Corollary 85, in GoingUp/Corollary85.lean.

theorem Hironaka.Manifold.hasOnlyNormalCrossingsWith_idealSheaf_of_traceFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {X : AnalyticManifold 𝕜 E} {S : Set X.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (F : Manifold.HypersurfaceFamily X.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFS : Manifold.HypersurfaceFamily.HasSncWithProper ψ F S s) {Z : Set X.carrier} {c : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ Z c) (hZS : Z ⊆ S) (h : AnalyticManifold.IdealSheaf.HasOnlyNormalCrossingsWith (hS.traceFamily F).idealSheaf ⋯.idealSheaf) : AnalyticManifold.IdealSheaf.HasOnlyNormalCrossingsWith F.idealSheaf hZ.idealSheaf

The lifting of clause (3′) from a closed submanifold to the ambient manifold (the ingredient of [Kol07, 30.2] the push-forward needs): for a closed submanifold S ⊆ X and a simple normal crossing family F having simple normal crossings with S properly, a closed submanifold Z ⊆ S whose ideal sheaf in S has only normal crossings with the reduced ideal sheaf of the trace F|_S has, in X, an ideal sheaf with only normal crossings with the reduced ideal sheaf of F: the dictionary hasOnlyNormalCrossingsWith_idealSheaf_iff on both sides around hasSncWith_of_hasSncWith_traceFamily.

theorem AnalyticManifold.FiniteSuccession.pushforward_hasOnlyNormalCrossingsWith_center_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 : hS.toAnalyticManifold.IdealSheaf} {m : ℕ} (hge : T.IsOfOrderGe J m ⊤) (i : Fin T.length) (h3 : ∀ (i' : Fin T.length), ↑i' < ↑i → ((pushforward hS T).boundarySeq ⊤ i'.castSucc).HasOnlyNormalCrossingsWith ((pushforward hS T).center i')) : ((pushforward hS T).boundarySeq ⊤ i.castSucc).HasOnlyNormalCrossingsWith ((pushforward hS T).center i)

The stage step for clause (3′) of the push-forward ([Kol07, 30.2–30.3]): if the push-forward Π = j_* T of a sequence T of order ≥ m (with the empty boundary) satisfies clause (3′) at every stage < i, it satisfies it at stage i. Through e_i : T_i ≃ S_i, clause (3′) of T at stage i becomes clause (3′) of Π|_S (HasOnlyNormalCrossingsWith.pullback_diffeomorph along e_i⁻¹, the boundary and centre identities boundarySeq_pushforwardStageIso, center_pushforwardStageIso); by the prefix-bounded comparison of the boundary with the family of exceptional divisors, the boundary of Π|_S is the reduced ideal sheaf of the trace of F_i^X on S_i, and the lifting hasOnlyNormalCrossingsWith_idealSheaf_of_traceFamily gives clause (3′) of Π at stage i.

theorem AnalyticManifold.FiniteSuccession.pushforward_hasOnlyNormalCrossingsWith_center {𝕜 : 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 : hS.toAnalyticManifold.IdealSheaf} {m : ℕ} (hge : T.IsOfOrderGe J m ⊤) (i : Fin T.length) : ((pushforward hS T).boundarySeq ⊤ i.castSucc).HasOnlyNormalCrossingsWith ((pushforward hS T).center i)

Clause (3′) of the push-forward ([Kol07, 30.2–30.3] made precise, with Hironaka's reduced boundary [Hir64, Main Theorem II′(N), p. 156]): the centre Z_i^X of j_* T has only normal crossings with its boundary at every stage, for T of order ≥ m with the empty boundary. Induction on a bound for the stage with the stage step.

theorem AnalyticManifold.FiniteSuccession.pushforward_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 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) (hT : T.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) m ⊤) : (pushforward hS T).IsOfOrderGe I m ⊤

Theorem 84 [Kol07, Theorem 84] in the ≥ m form: the push-forward j_* T of a smooth blow-up sequence of order ≥ m for (I|_S, m) (empty boundary) is of order ≥ m for (I, m), when I is D-balanced with ord I ≤ m everywhere. Clause (4′) is Kollár's induction (le_ordAlong_pushforward), clause (3′) is pushforward_hasOnlyNormalCrossingsWith_center (the identification S_{i+1} = (π_i)^{-1}_* S_i of [Kol07, 30.2] and the lifting of simple normal crossings; Kollár does not argue it beyond 30.2).

theorem AnalyticManifold.FiniteSuccession.pushforward_isOfOrder {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 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) (hT : T.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) m ⊤) : (pushforward hS T).IsOfOrder I ⊤ m

Theorem 84 [Kol07, Theorem 84], the conclusion as printed: j_* T is of order exactly m ([Kol07, Remark 67], isOfOrder_of_isOfOrderGe_of_ord_le).

theorem AnalyticManifold.FiniteSuccession.pushforward_isOfOrder_of_not_subset_cosupp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 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) (_hSc : ¬S ⊆ {x : M.carrier | ↑m ≤ Manifold.IdealSheaf.ord I x}) (hT : T.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) m ⊤) : (pushforward hS T).IsOfOrder I ⊤ m

Theorem 84 as printed [Kol07, Theorem 84]. The hypothesis _hSc : S ⊄ cosupp(I, m) is part of Kollár's statement and is kept so that the theorem reads as printed; the proof does not need it, because it is pushforward_isOfOrder, whose induction on the stage works for every smooth hypersurface S (the algebraic version IsDBalanced.isOrderSeq_pushforward likewise does without it).