Transforms of ideal sheaves under a blowing-up: the definitions

The transforms of an ideal sheaf under the blowing-up π : M' → M of an analytic manifold along a closed submanifold Y of codimension c, following Hironaka's total and weak transforms [Hir64, Ch. 0, §5, pp. 141–142] and Bierstone–Milman's strict transform [BM97, §3]. The blowing-up is IsBlowUp ψ Y c π and the ideal sheaves are those of Manifold.IdealSheaf.

• IdealSheaf.IsDivExceptional Itot IF m J': the specification of the quotient IF^{-m} · Itot, stalkwise the colon ideal (Itot_a : IF_a^{m a});
• IdealSheaf.ordAlongIdeal D J a: the order of J along the ideal sheaf D of a centre at a, sup {p | J_a ⊆ D_a^p} [BM97, §3], and IdealSheaf.genericOrdAlong D J a, its infimum over the connected component of the centre through a (the order at the generic point of the component, [Kol07, Definition 47]);
• the total transform π⁻¹(I) = π^*I · 𝒪_{M'} is the pullback I.pullback π h.contMDiff of the ideal sheaf along the analytic map π ([Hir64, Ch. 0, §5, p. 142]; [BM97, Theorem 1.10]), and the ideal sheaf I_F = π^*I_Y of the exceptional divisor is hY.idealSheaf.pullback π h.contMDiff (I_Y = IsClosedSubmanifold.idealSheaf hY);
• strictTransformSubspace hY h I: the strict transform X' of the closed subspace X ⊆ M with ideal sheaf I [BM97, §3, "The strict transform"; Proposition 3.13], the saturation of the total transform with respect to the exceptional divisor, stalkwise saturationStalk hY h I a' = ⨆ k, (π⁻¹(I)_{a'} : I_{F,a'}^k).

The analytic main theorems carry, along a succession of monoidal transformations, two transforms of ideal sheaves on bundled analytic manifolds, defined for any analytic map f : M' → M and any ideal sheaf D of the centre:

• AnalyticManifold.IdealSheaf.weakTransform f J D, Hironaka's weak transform of J Hir64, p. 142: f⁻¹(J) divided by the m-th power of f⁻¹(D), m the generic order of J along the component of the centre;
• AnalyticManifold.IdealSheaf.reducedTransform f E D, the reduced subspace red(f⁻¹(E) ∪ f⁻¹(D)) of the boundary clause of Hironaka's Main Theorem II'(N) Hir64, Main Theorem II'(N) (iii), p. 156, through the vanishing ideals vanishingStalk.

The quotients, the strict transform and the reduced transform are defined by their stalkwise specification and a classical choice: the unique ideal sheaf with the prescribed stalks when one exists (uniqueness is IdealSheaf.ext), the unit ideal sheaf (for the reduced transform, the product f^*E · f^*D) otherwise. Existence (the colon stalks are locally generated by the divided generators) and the identification with Kollár's chart formula are proved in Hironaka.Manifold.BlowUp.Transform.Colon.

def Manifold.IdealSheaf.IsDivExceptional {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (Itot IF : IdealSheaf 𝒪) (m : ↑X → ℕ) (J' : IdealSheaf 𝒪) : Prop

J' is the m-fold quotient of Itot by IF: at every point a its stalk is the colon ideal (Itot_a : IF_a^{m a}), the germs g with g · IF_a^{m a} ⊆ Itot_a ([Hir64, Ch. 0, §5, p. 142]; [Kol07, Definition 60, (60.1)]). The exponent may vary with the point: Hironaka's weak transform divides by the generic order along each component of the centre.

Equations

• Itot.IsDivExceptional IF m J' = ∀ (a : ↑X), J'.stalkIdeal a = Submodule.colon (Itot.stalkIdeal a) ↑(IF.stalkIdeal a ^ m a)

noncomputable def Manifold.IdealSheaf.ordAlongIdeal {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D J : IdealSheaf 𝒪) (a : ↑X) : ℕ∞

The order of J along the centre with ideal sheaf D at a, ν_{D,a}(J) = sup {p | J_a ⊆ D_a^p} (in ℕ∞; ⊤ when J_a = 0) [BM97, §3].

Equations

• D.ordAlongIdeal J a = ⨆ (p : ℕ), ⨆ (_ : J.stalkIdeal a ≤ D.stalkIdeal a ^ p), ↑p

noncomputable def Manifold.IdealSheaf.genericOrdAlong {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D J : IdealSheaf 𝒪) (a : ↑X) : ℕ∞

The generic order of J along the connected component of the centre D through a: the infimum of ν_{D,y}(J) over that component (the order at the generic point of the component, [Kol07, Definition 47]).

Equations

• D.genericOrdAlong J a = ⨅ y ∈ connectedComponentIn D.support a, D.ordAlongIdeal J y

The strict transform of a closed subspace

noncomputable def Manifold.saturationStalk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (I : IdealSheaf (structureSheaf 𝕜 E M)) (a' : M') : Ideal ↑((structureSheaf 𝕜 E M').presheaf.stalk a')

The saturation of the total transform (the pull-back π⁻¹(I) along the blow-up) with respect to the exceptional divisor at a', ⋃_k (π⁻¹(I)_{a'} : I_{F,a'}^k) — the germs g with y_exc^k g ∈ π⁻¹(I)_{a'} for some k.

Equations

• Manifold.saturationStalk hY h I a' = ⨆ (k : ℕ), Submodule.colon ((Manifold.IdealSheaf.pullback π ⋯ I).stalkIdeal a') ↑((Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf).stalkIdeal a' ^ k)

noncomputable def Manifold.strictTransformSubspace {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (I : IdealSheaf (structureSheaf 𝕜 E M)) : IdealSheaf (structureSheaf 𝕜 E M')

The strict transform X' of the closed subspace X ⊆ M with ideal sheaf I under the blowing-up π with centre Y — the ideal sheaf whose stalks are the saturations ⋃_k (π⁻¹(I)_{a'} : I_{F,a'}^k) (of finite type since X is locally Noetherian, as Bierstone–Milman remark after Proposition 3.13), taken when that stalk family has local generators, the unit ideal sheaf otherwise (the pattern of the weak transform).

Equations

• One or more equations did not get rendered due to their size.

The transforms of the analytic main theorems

noncomputable def AnalyticManifold.IdealSheaf.weakTransform {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M M' : AnalyticManifold 𝕜 E} (f : AnalyticMap M' M) (J D : M.IdealSheaf) : M'.IdealSheaf

Hironaka's weak transform of J by the monoidal transformation f with centre D [Hir64, p. 142]: f⁻¹(J) divided by the m-th power of the ideal of f⁻¹(D), m the order of J at the generic point of (each component of) D. Formally: the ideal sheaf whose stalk at every a' is the colon ideal (f⁻¹(J)_{a'} : f⁻¹(D)_{a'}^m), m the generic order of J along the connected component of the cosupport of D through f a' (IdealSheaf.genericOrdAlong, read in ℕ; IdealSheaf.IsDivExceptional), chosen when such an ideal sheaf exists — Hironaka shows that it does when f is the monoidal transformation with centre D — and the unit ideal sheaf otherwise. The total transform f⁻¹(J) is IdealSheaf.pullback.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AnalyticManifold.IdealSheaf.reducedTransform {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M M' : AnalyticManifold 𝕜 E} (f : AnalyticMap M' M) : M.IdealSheaf → (D : M.IdealSheaf) → M'.IdealSheaf

Hironaka's red(f⁻¹(E) ∪ f⁻¹(D)) [Hir64, Main Theorem II'(N) (iii), p. 156]; Włodarczyk's exceptional divisor of a composite of blow-ups [Wlo09, Remark (1) after Theorem 2.0.3]: the reduced closed analytic subspace of M' whose set of points is f⁻¹(E) ∪ f⁻¹(D) — the ideal sheaf whose stalks are the vanishing ideals of that closed set (vanishingStalk, the germs vanishing on the set near the point), when these stalks have local generators (they do when E is a normal crossings divisor and f the monoidal transformation with centre D, the case of the main theorems: Hironaka/Manifold/FiniteSuccession/BoundaryFamily.lean), and otherwise the product f^*E · f^*D, which has the same set of points.

Equations

• One or more equations did not get rendered due to their size.