The Jacobian clause on the glued blow-down

For the glued blow-down σ : M̃ → M of the resolution family resolveFam bo T, on the extension-compatible family resolveFamExt bo T (Wlo09/FamilyExt.lean), the product of the Jacobian ideal of σ with σ⁻¹(𝓘) is the ideal sheaf of a normal-crossings divisor (resolveFamExt_jacobianIdeal_mul_pullback_isNormalCrossingsDivisor): the remark after [BM97, Theorem 1.10], that if J is the ideal generated locally by the Jacobian determinant of the composite of the blowings-up then J · σ⁻¹(𝓘) is a normal-crossings divisor. It is the input of Bierstone–Milman's principalization theorem with the Jacobian clause, the main theorem exists_extensionCompatibleFamily_isNormalCrossingsDivisor_jacobianIdeal_mul_pullback at the end of this file, which transports the clauses on the model, together with those of Main Theorem II″(N) for the empty boundary (resolveFamExt_mainTheoremIIpp), to an arbitrary real-analytic manifold.

• On a piece U (the relatively compact opens of the exhaustion, resolveSeqOn_jacobianIdeal_mul_pullback_composite_isNormalCrossingsDivisor): the Jacobian ideal of the composite blow-down of resolveSeqOn bo T U hU is a monomial in the exceptional family at every point (jacobianLedger_composite_of_forall_hasSncWith, Hironaka/Resolution/Analytic/BM97/LedgerSequence.lean, its hypothesis that the centres have simple normal crossings with the boundary being the corollary center_resolveSeqOn_hasSncWith of clause (3′) of the value) and the pull-back of 𝓘|_U is a boundary monomial (pullbackIsMonomialAtLast_resolveSeqOn, Hironaka/Resolution/Analytic/Wlo09/Monomial.lean); the product of two monomials of one simple normal crossing family is a normal-crossings divisor (isNormalCrossingsDivisor_jacobianIdeal_mul_of_forall_monomial, Principalization/JacobianMonomial.lean).
• On M̃ (resolveFamExt_jacobianIdeal_mul_pullback_isNormalCrossingsDivisor): every point is ι_m q (toLimit_surjective); the stalk of J · σ⁻¹(𝓘) at ι_m q is carried by the germ isomorphism of ι_m onto the piece's stalk (the Jacobian factor by CompatibleFamily.jacobianStalk_limitBlowDown_toLimitMap, Hironaka/Resolution/Analytic/BM97/LedgerLimit.lean; the pull-back factor by pullback_comp and limitDesc_comp_toLimitMap), and the normal-crossings form is transported back along the local diffeomorphism ι_m (exists_monomial_of_comap_of_isLocalDiffeomorphAt).
• resolveFamExt_comap_map_isNormalCrossingsDivisor: σ⁻¹(𝓘) alone is the ideal sheaf of a normal-crossings divisor ([Kol07, Theorem 35 (2)]; [Wlo09, Theorem 2.0.3 (3)]; [BM97, Theorem 1.10]), the gluing tool CompatibleFamily.isNormalCrossingsDivisor_comap_limitBlowDown fed on each piece by resolveSeqOn_comap_last_isNormalCrossingsDivisor; this is the form the main theorems use.

theorem Hironaka.Manifold.resolveSeqOn_jacobianIdeal_mul_pullback_composite_isNormalCrossingsDivisor {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((resolveSeqOn bo T U hU).toSuccession.composite.jacobianIdeal * Manifold.IdealSheaf.pullback ⇑(resolveSeqOn bo T U hU).toSuccession.composite ⋯ (restrictTriple T U).I).IsNormalCrossingsDivisor

On the piece: for the value resolveSeqOn bo T U hU of the resolution family on the relatively compact open U, the Jacobian ideal of the composite blow-down times the pull-back of 𝓘|_U is a normal-crossings divisor (the remark after [BM97, Theorem 1.10]): isNormalCrossingsDivisor_jacobianIdeal_mul_of_forall_monomial with the Jacobian ledger jacobianLedger_composite_of_forall_hasSncWith (its simple-normal-crossings hypothesis on the centres from center_resolveSeqOn_hasSncWith) and the boundary-monomial form of the pull-back, pullbackIsMonomialAtLast_resolveSeqOn.

theorem Hironaka.Manifold.resolveFamExt_jacobianIdeal_mul_pullback_isNormalCrossingsDivisor {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) : ((resolveFamExt bo T).map.jacobianIdeal * Manifold.IdealSheaf.pullback ⇑(resolveFamExt bo T).map ⋯ T.I).IsNormalCrossingsDivisor

The product of the Jacobian ideal of the glued blow-down σ with σ⁻¹(𝓘) is a normal-crossings divisor (the remark after [BM97, Theorem 1.10]): every point of M̃ lies on a piece (toLimit_surjective); the stalk of J · σ⁻¹(𝓘) at ι_m q is carried onto the piece's by the germ isomorphism of ι_m = toLimitMap m (the Jacobian factor by CompatibleFamily.jacobianStalk_limitBlowDown_toLimitMap, the pull-back factor by pullback_comp and limitDesc_comp_toLimitMap), and the normal-crossings form is transported back along the local diffeomorphism ι_m by exists_monomial_of_comap_of_isLocalDiffeomorphAt. Used by exists_extensionCompatibleFamily_isNormalCrossingsDivisor_jacobianIdeal_mul_pullback (below).

theorem Hironaka.Manifold.resolveFamExt_comap_map_isNormalCrossingsDivisor {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) : AnalyticManifold.IdealSheaf.IsNormalCrossingsDivisor (Manifold.IdealSheaf.pullback ⇑(resolveFamExt bo T).map ⋯ T.I)

σ⁻¹(𝓘) is the ideal sheaf of a normal-crossings divisor ([Kol07, Theorem 35 (2)]; [Wlo09, Theorem 2.0.3 (3)]; [BM97, Theorem 1.10]): the gluing tool CompatibleFamily.isNormalCrossingsDivisor_comap_limitBlowDown at resolveFam bo T, fed on each piece by resolveSeqOn_comap_last_isNormalCrossingsDivisor. Used by exists_extensionCompatibleFamily_isNormalCrossingsDivisor_jacobianIdeal_mul_pullback (below).

theorem AnalyticManifold.exists_extensionCompatibleFamily_isNormalCrossingsDivisor_jacobianIdeal_mul_pullback {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (M : AnalyticManifold ℝ E) (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) : ∃ (F : M.ExtensionCompatibleFamily), IsProperMap ⇑F.map ∧ (∀ (K : TopologicalSpace.Compacts M.carrier), (∀ (i : Fin (F.seq K).length), ((F.seq K).center i).IsNonsingular) ∧ (F.seq K).HasSncBoundaries ⊤ ∧ (F.seq K).weakTransformSeq (I.restrict (F.nhd K)) (Fin.last (F.seq K).length) = ⊤) ∧ IdealSheaf.IsNormalCrossingsDivisor (Manifold.IdealSheaf.pullback ⇑F.map ⋯ I) ∧ (F.map.jacobianIdeal * Manifold.IdealSheaf.pullback ⇑F.map ⋯ I).IsNormalCrossingsDivisor ∧ F.map.IsIsoOver (Manifold.IdealSheaf.support I)ᶜ

Real-analytic principalization with the Jacobian clause BM97, Theorem 1.10 and the sentence following it, in the compatible-family form of [Wlo09, Theorem 2.0.3 (1), (2) and (4)]. Let M be a real-analytic manifold modelled on a finite-dimensional real vector space and I an ideal sheaf on M with nonzero stalks. Then there is a proper analytic map σ : M̃ → M which over an open neighbourhood U_K of every compact K ⊆ M splits, compatibly across compacts (ExtensionCompatibleFamily), into a finite succession of monoidal transformations U_K = U_0 ← ⋯ ← U_r with centres D_i, such that

• for every compact K: every centre D_i is smooth; the exceptional divisors E_i, the boundaries started at the empty boundary E_0 = ⊤, have simple normal crossings with the centres, and the last one E_r has simple normal crossings (FiniteSuccession.HasSncBoundaries); and the weak transform of I|_{U_K} on U_r is the unit ideal sheaf;
• the pull-back σ*(I) is a normal-crossings divisor (IdealSheaf.IsNormalCrossingsDivisor);
• the product of the Jacobian ideal of σ (AnalyticMap.jacobianIdeal: the ideal sheaf generated locally, in analytic coordinates, by the Jacobian determinant of σ) with σ*(I) is a normal-crossings divisor;
• σ is an analytic isomorphism over the complement of the support of I (AnalyticMap.IsIsoOver), the support being Kollár's cosupport cosupp I [Kol07, Theorem 21 (2)].

The clauses on the successions are stated over each compact; the normal-crossings, Jacobian and isomorphism clauses, being local on M̃, are stated on σ itself. For I = 𝒪_M the support of I is empty, so σ is an isomorphism by the last clause.

Relation to the source.

• Translation. I.pullback F.map F.map.contMDiff is Bierstone–Milman's $\sigma^{-1}(I) = \sigma^*(I) \cdot \mathcal{O}_{M_k}$, and F.map.jacobianIdeal * I.pullback F.map F.map.contMDiff their $\mathcal{J} \cdot \sigma^{-1}(I)$, $\mathcal{J}$ the ideal generated by the Jacobian determinant of $\sigma$; (F.seq K).weakTransformSeq (I.restrict (F.nhd K)) (Fin.last _) = ⊤ is their $I_k = \mathcal{O}_{M_k}$; (F.seq K).HasSncBoundaries ⊤ is the clause on the exceptional divisors $E_j$, ⊤ being the empty boundary; and F.map.IsIsoOver I.supportᶜ says that $\sigma$ is an isomorphism over the complement of the support of $I$.
• Interpretation. Bierstone–Milman's "smooth $\mathrm{inv}_I$-admissible centres" are read as smooth centres having simple normal crossings with the exceptional divisor accumulated so far; the invariant $\mathrm{inv}_I$ does not appear in the statement.
• Correction. The hypothesis that I has nonzero stalks (hI) is tacit in the source: without it $\sigma^*(I)$ could not be a divisor. Kollár's principalization states it explicitly, for an ideal sheaf "not zero on any irreducible component" [Kol07, Theorem 35].
• Strengthening. Bierstone–Milman's finite sequence of blow-ups, for a quasi-compact $|M|$, is here a finite succession over a neighbourhood of every compact, compatible across compacts: for a manifold that is not quasi-compact the finite sequence is replaced by a locally finite one, by analogy with the remark after [BM97, Theorem 1.6], which is made for Theorem 1.6 only. For a compact M the family contains one finite succession over M.
• Strengthening. That the last exceptional divisor $E_r$ has simple normal crossings (in HasSncBoundaries) is not a clause of [BM97, Theorem 1.10]: it is their remark that admissibility "guarantees that $E_{i+1}$ is a collection of smooth hypersurfaces having only normal crossings" [BM97, after (1.2)], and [Wlo09, Theorem 2.0.3 (2)] at $i = r$.
• Strengthening. The clause that $\sigma$ is an isomorphism over the complement of the support of $I$ (F.map.IsIsoOver I.supportᶜ) is not in [BM97, Theorem 1.10] or [Wlo09, Theorem 2.0.3]; it is [Wlo09, Lemma 4.0.3], cf. [Kol07, Theorem 35 (3)].

Source statement: [BM97, Theorem 1.10]

Source statement: [Wlo09, Theorem 2.0.3] (compatible-family form)