Hironaka's Main Theorem II″(N) on the model manifold

The conclusion of Hironaka's Main Theorem II′(N) [Hir64, p. 156], which II″(N) [Hir64, pp. 158–159] asserts for real spaces, for a non-singular real or complex analytic manifold modelled on 𝕜ⁿ with a normal crossings divisor and a coherent sheaf of nonzero ideals, with its clauses (i)–(iv): properness of the blow-down and, over every compact K, on the finite succession over nhd K, (i) every centre is non-singular, (ii) the order of the weak transform of 𝓘|_{nhd K} is a positive constant on each centre, (iii) each boundary is a simple normal crossing family having simple normal crossings with its centre (the IsSncBoundaryWith form of "only normal crossings with"), (iv) the last boundary is a simple normal crossing family and the last weak transform is the unit ideal. It is proved here for the glued blow-down of the resolution family resolveFam bo T along the exhaustion of a manifold M modelled on 𝕜ⁿ, stated on the extension-compatible family resolveFamExt bo T (Wlo09/FamilyExt.lean). Kollár's form is [Kol07, Theorem 68] with Kol07, Remark 67; Włodarczyk's is [Wlo09, Theorem 2.0.3 (1), (2), (4)] with the reduction of the maximal order in [Wlo09, §6, Step 2a]. The theorem is the input of the main theorem exists_extensionCompatibleFamily_weakTransformSeq_eq_top at the end of this file, which transports it along the chart isomorphism of the boundary of an arbitrary real analytic manifold.

The proof

σ is proper because over each piece of the exhaustion it is a finite composite of blow-ups and properness is local on the target (isProperMap_resolveFamExt_map); over nhd K the succession seq K is the value of resolveFam there, whose centres are closed submanifolds, hence non-singular (clause (i), FiniteSuccession.center_isNonsingular); whose weak transforms of 𝓘|_{nhd K} have order exactly the round's mark along the centres ([Kol07, Remark 67] read backwards, Hironaka/Resolution/Analytic/Wlo09/HironakaClauses.lean; clause (ii), resolveSeqOn_clause_ii); whose boundaries are the ideal sheaves of the total transforms of the simple normal crossing boundary family T.F|_{nhd K}, themselves simple normal crossing families for the standard model and having simple normal crossings with the centre of their stage (clause (3′) of [Kol07, Definition 66]; isSnc_totalTransformSeqFrom_and_boundarySeq_eq_of_forall_lt fed by isOfOrderGe_zero_resolveSeqOn, with center_resolveSeqOn_hasSncWith and the boundary identified through restrictTriple_F_idealSheaf; clause (iii) and the first half of (iv), with the codimension codim i of the centre); and whose last weak transform is the unit ideal (the last round at mark 1, ord_lt; the second half of (iv), weakTransformSeq_last_resolveSeqOn_eq_top).

theorem Hironaka.Manifold.resolveFamExt_mainTheoremIIpp (𝕜 : Type) [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) : IsProperMap ⇑(resolveFamExt bo T).map ∧ ∀ (K : TopologicalSpace.Compacts M.carrier), (∀ (i : Fin ((resolveFamExt bo T).seq K).length), (((resolveFamExt bo T).seq K).center i).IsNonsingular) ∧ (∀ (i : Fin ((resolveFamExt bo T).seq K).length), ∃ (c : ℕ), 0 < c ∧ ∀ y ∈ Manifold.IdealSheaf.support (((resolveFamExt bo T).seq K).center i), Manifold.IdealSheaf.ord (((resolveFamExt bo T).seq K).weakTransformSeq (T.I.restrict ((resolveFamExt bo T).nhd K)) i.castSucc) y = ↑c) ∧ (∀ (i : Fin ((resolveFamExt bo T).seq K).length), (((resolveFamExt bo T).seq K).boundarySeq (AnalyticManifold.IdealSheaf.restrict T.F.idealSheaf ((resolveFamExt bo T).nhd K)) i.castSucc).IsSncBoundaryWith (((resolveFamExt bo T).seq K).center i)) ∧ (((resolveFamExt bo T).seq K).boundarySeq (AnalyticManifold.IdealSheaf.restrict T.F.idealSheaf ((resolveFamExt bo T).nhd K)) (Fin.last ((resolveFamExt bo T).seq K).length)).IsSncBoundary ∧ ((resolveFamExt bo T).seq K).weakTransformSeq (T.I.restrict ((resolveFamExt bo T).nhd K)) (Fin.last ((resolveFamExt bo T).seq K).length) = ⊤

Hironaka's Main Theorem II″(N) on the model manifold ([Hir64, pp. 158–159], with the clauses of Main Theorem II′(N), p. 156) for the glued blow-down of resolveFam bo T: properness (isProperMap_resolveFamExt_map) and, over every compact K, clauses (i), (ii) and the second half of (iv) by the per-open theorems of Hironaka/Resolution/Analytic/Wlo09/HironakaClauses.lean at nhd K, and clause (iii) with the first half of (iv) by the boundary family of the value (the total transform of T.F|_{nhd K} at each stage). Used by exists_extensionCompatibleFamily_weakTransformSeq_eq_top (below) and, for the empty boundary, by exists_extensionCompatibleFamily_isNormalCrossingsDivisor_jacobianIdeal_mul_pullback (Hironaka/Resolution/Analytic/BM97/JacobianAssembly.lean). Stated for 𝕜 = ℝ or ℂ: at 𝕜 = ℝ it is II″(N) (pp. 158–159); at 𝕜 = ℂ it is the compatible-family form of the conclusion of II′(N) (p. 156), without Hironaka's assumption that X admit a projective morphism to a complex Stein space.

theorem AnalyticManifold.exists_extensionCompatibleFamily_weakTransformSeq_eq_top {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] (X : AnalyticManifold ℝ E) (E₀ : X.IdealSheaf) (hE₀ : E₀.IsSncBoundary) (J₀ : X.IdealSheaf) (hJ₀ : Manifold.IdealSheaf.IsNonzeroEverywhere J₀) : ∃ (F : X.ExtensionCompatibleFamily), IsProperMap ⇑F.map ∧ ∀ (K : TopologicalSpace.Compacts X.carrier), (∀ (i : Fin (F.seq K).length), ((F.seq K).center i).IsNonsingular) ∧ (F.seq K).HasConstantPositiveOrderAlongCenters (J₀.restrict (F.nhd K)) ∧ (F.seq K).HasSncBoundaries (E₀.restrict (F.nhd K)) ∧ (F.seq K).weakTransformSeq (J₀.restrict (F.nhd K)) (Fin.last (F.seq K).length) = ⊤

Hironaka's Main Theorem II″(N) for real-analytic manifolds Hir64, Main Theorem II″(N), pp. 158–159, whose conclusion is that of Main Theorem II′(N), p. 156, in the compatible-family form of Włodarczyk's locally finite principalization [Wlo09, Theorem 2.0.3 (1) and (4)]. Let X be a real-analytic manifold, E₀ an ideal sheaf on X with only normal crossings (IsSncBoundary), and J₀ an ideal sheaf on X with nonzero stalks. Then there is a proper analytic map σ : X̃ → X which over an open neighbourhood U_K of every compact K ⊆ X splits, compatibly across compacts (ExtensionCompatibleFamily), into a finite succession of monoidal transformations U_K = U_0 ← U_1 ← ⋯ ← U_r with centres D_i ⊆ U_i such that, for every compact K,

• (i) every centre D_i is non-singular;
• (ii) the order of the weak transform J_i of J₀|_{U_K} is a positive constant along D_i (FiniteSuccession.HasConstantPositiveOrderAlongCenters);
• (iii) with E_0 = E₀|_{U_K} and E_{i+1} = red(σ_{i+1}⁻¹(E_i) ∪ σ_{i+1}⁻¹(D_i)), every E_i has only normal crossings with D_i, and, the first half of (iv), E_r has only normal crossings (FiniteSuccession.HasSncBoundaries);
• the second half of (iv): J_r = 𝒪_{U_r}, the unit ideal sheaf ⊤.

The constant of (ii) may depend on K and i. Clause (i) holds for every finite succession (FiniteSuccession.center_isNonsingular); it is kept as Hironaka's (i). For J₀ = 𝒪_X the weak transforms are the unit ideal, of order 0 everywhere, so (ii) leaves every centre empty, and σ is then an isomorphism.

Relation to the source.

• Translation. F : ExtensionCompatibleFamily X with F.map is the pair $(\tilde X, \sigma)$; F.nhd K is $U_K$ and F.seq K the finite succession over it; (F.seq K).weakTransformSeq (J₀.restrict (F.nhd K)) i is $J_i$ and (F.seq K).boundarySeq (E₀.restrict (F.nhd K)) i is $E_i$.
• Interpretation. Hironaka's "has only normal crossings" for the boundary is read on his global irreducible components [Hir64, Definition 2, p. 141], that is, as simple normal crossings in the sense of [Kol07, Definition 24] (IsSncBoundary, IsSncBoundaryWith).
• Translation. A real-analytic manifold, X : AnalyticManifold ℝ E, is Hironaka's non-singular analytic $\mathbb{R}$-space.
• Interpretation. Hironaka's "coherent sheaf of non-zero ideals" is read as a locally finitely generated ideal sheaf (IdealSheaf X, coherent by Oka's theorem) with nonzero stalks (hJ₀).
• Gap. Hironaka's succession is one locally finite succession $\{f_\lambda : X_{\lambda+1} \to X_\lambda\}$ of $X$ itself, indexed by a countable well-ordered set $\Lambda$ with maximal element $\gamma$ (projective limits at the elements without predecessor) [Hir64, p. 155], whose canonical modification $X_\gamma \to X$ he notes is proper (p. 155, after Main Theorem I′(n)). Here it is replaced by a finite succession $U_0 \leftarrow \cdots \leftarrow U_r$ (F.seq K) over a neighbourhood $U_K$ (F.nhd K) of each compact $K$, compatible across compacts, and the proper map $\sigma$ (F.map). Restricting Hironaka's succession over $U_K$ gives such a family (by local finiteness only finitely many centres meet the preimage of $U_K$); the compatible family is not asserted to come from one succession of $X$. Włodarczyk's "locally finite" is the compatible-family form itself.
• Gap. Clause (i) asserts non-singularity only, and a centre may be empty or have several components. Hironaka's irreducibility of the centres is not asserted per compact: Włodarczyk's centres are disjoint unions of smooth centres [Wlo09, Definition 3.2.4], and the irreducible refinement of the succession over a smaller compact is in general not the restriction of the succession over a larger one, which [Wlo09, Theorem 2.0.3 (4)] requires.
• Strengthening. In clause (iii) IsSncBoundaryWith also asserts that $E_i$ has only normal crossings at every point, which Hironaka's "with $D_i$" [Hir64, Definition 2, p. 141] does not; he derives it from (iii) (the remark after Main Theorem II, p. 143), and it is Wlo09, Theorem 2.0.3 (2).
• Gap. Hironaka's $X$ is any non-singular analytic $\mathbb{R}$-space; II″(N) does not fix its dimension (the "of dimension $N$" is in II′(N), p. 156). Here X has one model space E, so it is pure-dimensional; a non-singular space whose components have different dimensions is the disjoint union of its pure-dimensional open and closed parts, to each of which the theorem applies. No finite-dimensionality of E is assumed: the coordinates E ≃ ℝⁿ that hE₀ provides make E finite-dimensional.
• Restatement. The reducedness and invertibility of E₀, which Hironaka assumes ("reduced analytic subspace everywhere of codimension one"), are not separate hypotheses: both follow from the family of smooth hypersurfaces with simple normal crossings that hE₀ provides, whose reduced ideal sheaf is E₀.

Source statement: [Hir64, Main Theorem II″(N), pp. 158–159]

Source statement: [Wlo09, Theorem 2.0.3 (1) and (4)]