Total, strict and geometric strict transforms of closed subspaces #
The transforms of a closed analytic subspace X ⊆ M, given by its ideal sheaf I of finite type,
under the blowing-up π : M' → M with centre the closed submanifold Y (IsBlowUp ψ Y c π),
exceptional divisor F = π⁻¹(Y) with ideal sheaf I_F = hY.idealSheaf.pullback π h.contMDiff,
following [BM97, §3, "The strict transform"] and [Hir64, Ch. 0, §5, p. 142].
- The total transform
σ⁻¹(X): the closed subspace ofM'defined byπ⁻¹(I) = π^*I · 𝒪_{M'}, the pull-backI.pullback π h.contMDiffalong the blow-up (its points are the preimages of the points ofX,IdealSheaf.support_pullback). - The strict transform
X'([BM97, Proposition 3.13]; compare the controlled transform of a marked ideal, [Wlo09, Definition 3.2.4, (3)]). Bierstone–Milman give two forms: the ideal generated ata'by the strict transformsf' = y_exc^{-d}(f ∘ σ)of thef ∈ I_{σ(a')}, and (Proposition 3.13) the saturation⋃_k (I_{σ⁻¹(X)} : I_F^k)with respect to the exceptional divisor.strictTransformSubspaceis the saturation: the ideal sheaf whose stalks aresaturationStalk hY h I a' = ⨆ k, (π⁻¹(I)_{a'} : I_{F,a'}^k), taken by a classical choice when this stalk family has local generators (Bierstone–Milman's "I_{X'}is an ideal of finite type sinceXis locally Noetherian", proved inHironaka.Manifold.BlowUp.Transform.SaturationFiniteType), the unit ideal sheaf otherwise, the pattern of the weak transform; in the first case its stalks are the saturations (stalkIdeal_strictTransformSubspace_of_hasLocalGenerators). The generated-by-strict-transforms form isstrictTransformElems; that its span is contained in the saturation is immediate (span_strictTransformElems_le_saturationStalk, one direction of Proposition 3.13); the other direction is proved inHironaka.Manifold.BlowUp.Transform.StrictSubspaceProp313. - The geometric strict transform
X''([BM97, Remarks 1.7, (2)] and [BM97, Remark 3.15]): the smallest closed subspace ofσ⁻¹(X)containing the set|σ⁻¹(X)| ∖ |F|; in ideal-sheaf terms the largest ideal sheafJ ≥ π⁻¹(I)whose cosupport contains that set (geometricCandidates;geometricStrictTransformis the greatest element, by a classical choice, the unit ideal sheaf if there is none). The total transform is a candidate, and the strict transform is one as soon as its stalks are the saturation (strictTransform_mem_geometricCandidates_of_hasLocalGenerators), which givesX'' ⊆ X'.
Conventions: ideal sheaves are ordered by inclusion of stalk ideals, so X' ⊆ σ⁻¹(X) reads
π⁻¹(I) ≤ I_{X'}; ⊤ is the empty subspace. The strict transform of the centre itself is empty
(the saturation of I_F is ⊤).
The strict transform #
theorem
Manifold.stalkIdeal_strictTransformSubspace_of_hasLocalGenerators
{𝕜 : 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))
(hex : IdealSheaf.HasLocalGenerators (saturationStalk hY h I))
(a' : M')
:
theorem
Manifold.strictTransformSubspace_of_not_hasLocalGenerators
{𝕜 : 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))
(hex : ¬IdealSheaf.HasLocalGenerators (saturationStalk hY h I))
:
theorem
Manifold.totalTransform_stalkIdeal_le_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')
:
The total transform lies in its saturation (the term k = 0).
theorem
Manifold.totalTransform_le_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))
:
X' ⊆ σ⁻¹(X) — the strict transform contains the total transform's ideal
sheaf (unconditionally: if the saturation is not of finite type the chosen ideal sheaf is the
empty subspace).
def
Manifold.strictTransformElems
{𝕜 : 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')
:
Set ↑((structureSheaf 𝕜 E M').presheaf.stalk a')
The strict transforms of the elements of I at a':
the germs g = y_exc^{-d}(f ∘ σ), i.e. y^d · g = σ^*(f) for some f ∈ I_{σ(a')}, some
generator y of I_{F,a'} and some d (in the domain 𝒪_{M',a'} the ideal they generate is
the one generated with the maximal d = μ_{C,σ(a')}(f)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Manifold.span_strictTransformElems_le_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')
:
A strict transform
g = y^{-d}(f ∘ σ) lies in the saturation — y^d g = σ^*(f) ∈ π⁻¹(I)_{a'}.
The geometric strict transform #
def
Manifold.geometricCandidates
{𝕜 : 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))
:
Set (IdealSheaf (structureSheaf 𝕜 E M'))
The closed subspaces Z ⊆ σ⁻¹(X) whose set
of points contains |σ⁻¹(X)| ∖ |F| — as ideal sheaves, the J ≥ π⁻¹(I) with
|σ⁻¹(X)| ∖ |F| ⊆ |J|.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Manifold.geometricStrictTransform
{𝕜 : 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 geometric strict transform X'' —
the smallest closed subspace of σ⁻¹(X) containing the set |σ⁻¹(X)| ∖ |F|, i.e. the greatest
element of geometricCandidates (it exists by local Noetherianness), taken by
Classical.choice; the unit ideal sheaf if there is none.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Manifold.isGreatest_geometricStrictTransform_of_exists
{𝕜 : 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))
(hex : ∃ (J : IdealSheaf (structureSheaf 𝕜 E M')), IsGreatest (geometricCandidates hY h I) J)
:
IsGreatest (geometricCandidates hY h I) (geometricStrictTransform hY h I)
theorem
Manifold.totalTransform_mem_geometricCandidates
{𝕜 : 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))
:
The total transform is a candidate (Z = σ⁻¹(X)).
theorem
Manifold.saturationStalk_of_notMem_cosupport
{𝕜 : 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'}
(ha' : a' ∉ (IdealSheaf.pullback π ⋯ hY.idealSheaf).support)
:
Off the exceptional divisor the saturation is the total transform's stalk (I_{F,a'} = 𝒪).
theorem
Manifold.strictTransform_mem_geometricCandidates_of_hasLocalGenerators
{𝕜 : 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))
(hex : IdealSheaf.HasLocalGenerators (saturationStalk hY h I))
:
The strict transform is a candidate as soon as its stalks are the saturation
(X' ⊆ σ⁻¹(X), and off F the strict and total transforms agree).
theorem
Manifold.strictTransform_le_geometricStrictTransform_of_exists
{𝕜 : 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))
(hex : IdealSheaf.HasLocalGenerators (saturationStalk hY h I))
(hg : ∃ (J : IdealSheaf (structureSheaf 𝕜 E M')), IsGreatest (geometricCandidates hY h I) J)
:
Given the two existence facts (the finite type of the saturation and local Noetherianness): the strict transform's ideal sheaf lies in the geometric strict transform's.