Transforms under a blowing-up: marked ideal sheaves, weak transforms, strict transforms of sets

Transforms under the blowing-up π : M' → M of an analytic manifold along a closed submanifold Y of codimension c (IsBlowUp ψ Y c π, with total transform I.pullback π h.contMDiff and exceptional ideal sheaf I_F = hY.idealSheaf.pullback π h.contMDiff), and two unfoldings of the orders along a centre:

• MarkedIdealSheaf and MarkedIdealSheaf.birationalTransform: the marked ideal sheaf (I, m) and its birational transform (I_F^{-m} π⁻¹(I), m) [Kol07, Definition 60, (60.1)], the quotient of the total transform by the m-th power of the exceptional ideal sheaf I_F (IdealSheaf.IsDivExceptional);
• IdealSheaf.weakTransformOf hY h I: Hironaka's weak transform, division by the generic order along each component of the centre ([Hir64, Ch. 0, §5, p. 142]; [BM97, Remark 1.8]), for the blowing-up h and the ideal sheaf hY.idealSheaf of its centre — the unbundled reading of AnalyticManifold.IdealSheaf.weakTransform, the weak transform of the analytic main theorems;
• strictTransformSet π Y H: the strict transform of a subset, the closure of π⁻¹(H ∖ Y);
• the order along a centre depends only on the stalk (IdealSheaf.ordAlongIdeal_congr_stalk), and the generic order is the infimum over the component of the centre (IdealSheaf.genericOrdAlong_def).

The quotients are classical choices, the unit ideal sheaf when no ideal sheaf has the colon stalks.

theorem Manifold.IdealSheaf.ordAlongIdeal_congr_stalk {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D J J' : IdealSheaf 𝒪) (a : ↑X) (h : J.stalkIdeal a = J'.stalkIdeal a) : D.ordAlongIdeal J a = D.ordAlongIdeal J' a

The order along D at a depends only on the stalk of J at a.

theorem Manifold.IdealSheaf.genericOrdAlong_def {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D J : IdealSheaf 𝒪) (a : ↑X) : D.genericOrdAlong J a = ⨅ y ∈ connectedComponentIn D.support a, D.ordAlongIdeal J y

The generic order unfolded: the infimum over the component of the centre of the order of J along D.

structure Manifold.MarkedIdealSheaf {X : TopCat} (𝒪 : TopCat.Sheaf CommRingCat X) : Type u_1

A marked ideal sheaf (I, m) [Kol07, Definition 60].

• I : IdealSheaf 𝒪

  The ideal sheaf.

• m : ℕ

  The marking.

noncomputable def Manifold.MarkedIdealSheaf.birationalTransform {𝕜 : 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 π) (J : MarkedIdealSheaf (structureSheaf 𝕜 E M)) : MarkedIdealSheaf (structureSheaf 𝕜 E M')

The birational transform of a marked ideal sheaf, π_*^{-1}(I, m) := (I_F^{-m} · π⁻¹(I), m) [Kol07, Definition 60, (60.1)]: the ideal sheaf with stalks (π⁻¹(I)_a : I_{F,a}^m) when it exists (which is the case for m ≤ ν_Y(I)), the unit ideal sheaf otherwise.

Equations

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

@[reducible, inline]

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

The weak transform of I by the blowing-up π with centre Y [Hir64, Ch. 0, §5, p. 142]: π⁻¹(I) divided by the ν-th power of I_F, ν the generic order of I along the component of Y through the point (a classical choice of the ideal sheaf with those colon stalks; the unit ideal sheaf if none exists) — the weak transform AnalyticManifold.IdealSheaf.weakTransform of the analytic main theorems along the analytic map π with the ideal sheaf hY.idealSheaf of the centre, read on the bundled manifolds ⟨M⟩, ⟨M'⟩.

Equations

• Manifold.IdealSheaf.weakTransformOf hY h I = AnalyticManifold.IdealSheaf.weakTransform ⟨π, ⋯⟩ I hY.idealSheaf

def Manifold.strictTransformSet {M M' : Type u} [TopologicalSpace M'] (π : M' → M) (Y H : Set M) : Set M'

The strict transform of a subset H ⊆ M under π with centre Y: the closure of π⁻¹(H ∖ Y) (the set underlying the strict transform of [BM97, §3, "The strict transform"]).

Equations

• Manifold.strictTransformSet π Y H = closure (π ⁻¹' (H \ Y))