Strict transforms of closed subspaces: the smooth case #
The strict transform X' of a closed subspace X ⊆ M under the blowing-up π : M' → M along a
closed submanifold Y is defined ideal-theoretically (strictTransformSubspace: the saturation
⋃_k (π⁻¹(I_X) : I_F^k) of the total transform with respect to the exceptional divisor F,
[BM97, Proposition 3.13]), and the geometric strict transform X'' as the smallest closed
subspace of π⁻¹(X) containing |π⁻¹(X)| ∖ |F| (geometricStrictTransform). This file proves
that in the smooth case these agree with the geometric constructions on the manifold:
- for closed submanifolds
Y ⊆ Sthe strict transform ofSis the ideal sheaf (IsClosedSubmanifold.idealSheaf) of the closed submanifoldstrictTransformSet π Y S = closure (π⁻¹(S ∖ Y)), andX' = X''(the identification of the blow-up ofSwith the birational transform ofSin [Kol07, Definition 30, 30.2]); - for
S = Ythe strict transform is empty, the total transform is the exceptional divisor, and its idealπ^*I_Y = I_Fis locally principal (blowing up a smooth variety along itself, as in the proof of [Kol07, Corollary 22]; [Wlo09, Lemma 5.3.7]); - for a smooth hypersurface
Hhaving simple normal crossings withY(in coordinates: at every point ofH ∩ Ya chart adapted toYin whichHis a coordinate hyperplane), the strict transform ofHis the ideal sheaf of the smooth hypersurfacestrictTransformSet π Y H; forY ⊆ Hit is the birational transformπ^{-1}_*(I_H, 1)[BM97, §3, "The strict transform"].
The argument #
Everything reduces to a stalkwise identity saturation = I_{S'} for the closed submanifold
S' = strictTransformSet π Y S, then IdealSheaf.ext (the saturation stalks have local
generators because I_{S'} does, so strictTransformSubspace is the sheaf with those stalks;
the finite-type clause holds outright here).
saturation ⊆ I_{S'}is chart-free (saturationStalk_le_idealSheaf_strictTransform): pulled back germs ofI_Svanish onπ⁻¹(S) ⊇ S'(totalTransform_stalkIdeal_le_idealSheaf_of_subset, from the vanishing characterisationgerm_mem_stalkIdeal_idealSheaf_iff); a germtwithu^k t ∈ π⁻¹(I_S),uthe exceptional coordinate, vanishes onS' ∖ F ⊇ π⁻¹(S ∖ Y), which is dense inS', sotvanishes onS'(eq_zero_on_closure_of_pow_mul_eq_zero).I_{S'} ⊆ saturationis the chart computation. ForY ⊆ Sit uses the flag chart (exists_adaptedChart_flag:Y = {z_σ = 0},S = {z_{σ(τ j)} = 0}) and the blow-up chart formulasu_i u_{σ k} = π^* z_{σ k}(IsBlowUpChart.germMap_coord_of_ne): on the chartsi ∉ range τ,S' = {u_{σ(τ j)} = 0}and eachu_{σ(τ j)} ∈ (π⁻¹(I_S) : I_F); on the chartsi ∈ range τ,S'is absent and the saturation is⊤. For a hypersurface it uses the three chart lemmas ofHironaka.Manifold.BlowUp.Transform.Strict(strictTransform_inter_source_self/_of_ne/_off) forH = {z_k = 0}withkthe blow-up index, another centre index, or an off-centre index. Off the centre the saturation is the total transform (saturationStalk_of_notMem_cosupport) and the transported chart gives the generators.X' = X'': every candidate vanishes onπ⁻¹(S ∖ Y)(its stalks at those points lie in the maximal ideal), hence on the closureS', so lies inI_{S'}(geometricCandidates_le_idealSheaf_strictTransform); withstrictTransform_mem_geometricCandidates_of_hasLocalGeneratorsthis makesI_{S'}the greatest candidate, andgeometricStrictTransform(a classical choice of the greatest element) equals it.- The case
S = Yis immediate:I_F = π⁻¹(I_Y)by definition (both are the pullback ofI_Y), so1lies in the saturation; the principal stalks arestalkIdeal_exceptionalIdealSheaf_eq_span_coord.
Conventions: ideal sheaves are ordered by inclusion of stalks, ⊤ is the empty subspace; the
strict transform set is Kollár's birational transform of a subvariety. The statements quantify
over closed-submanifold witnesses hS'/hH' of the strict transform set where they name its
ideal sheaf; the witnesses are supplied by IsClosedSubmanifold.strictTransform and
isClosedSubmanifold_strictTransform_of_charts. The topological lemmas and the vanishing
characterisation are routine (the sources' "dense in the strict transform").
Two topological lemmas: vanishing on a dense subset #
A continuous function vanishing on A ∩ W vanishes on closure A ∩ W (W open).
A continuous function vanishing, up to a factor nonzero on A, on the closure of A,
vanishes on that closure.
The vanishing characterisation of the ideal of a closed submanifold #
A germ at a point of a closed submanifold lies in its ideal iff a representing function
vanishes on the submanifold near the point (germ_mem_stalkIdeal_idealSheaf_iff, read
through stalkToGerm).
Stalkwise lemmas on the saturation (no chart on M needed) #
The total transform of the ideal of a closed submanifold S lies in the
ideal of any closed submanifold S' ⊆ π⁻¹(S) — pulled-back germs of functions vanishing on S
vanish on π⁻¹(S).
Off π⁻¹(S) the saturation of the total transform of I_S is the unit ideal (the stalk of
I_S at π p ∉ S is ⊤).
If a generator u of the exceptional ideal at p lies in the total transform, the saturation
is the unit ideal (1 ∈ (π⁻¹(I) : I_F)).
v lies in the saturation (π⁻¹(I) : I_F) as soon as u v lies in the total transform, u
a generator of the exceptional ideal at p — BM97's f' = y_exc^{-1} (f ∘ σ) (BM97, §3, "The
strict transform") read as a membership.
Every
candidate J (an ideal sheaf ≥ π⁻¹(I_S) whose cosupport contains
|π⁻¹(S)| ∖ |F| = π⁻¹(S ∖ Y)) lies in the ideal of the submanifold strict transform S': a
section of J vanishes at every point of the cosupport of J (the stalk ideal lies in the maximal
ideal there), hence on π⁻¹(S ∖ Y), hence — by continuity — on its closure S'.
Blowing up a smooth X along itself #
The saturation of the total
transform of the centre's own ideal is the unit ideal at every point — I_F = π⁻¹(I_X), so
1 ∈ (π⁻¹(I_X) : I_F).
The strict transform of the
centre is empty — the unit ideal sheaf (IdealSheaf.ext from saturationStalk_self_eq_top; the
constant family ⊤ has local generators).
The total transform of the centre is the exceptional divisor,
π⁻¹(X) = F — as closed subspaces, both being the pullback of I_X along π; the two
readings coincide by rfl.
The points of π⁻¹(X) are π⁻¹(X) = |F|
(IdealSheaf.support_pullback, cosupport_idealSheaf).
The
stalks of the total transform of the centre are principal — spanned by the scaling coordinate u_i
in the blow-up chart i (stalkIdeal_exceptionalIdealSheaf_eq_span_coord), by 1 off
the exceptional divisor.
The saturation lies in the ideal of the submanifold strict transform #
Inclusion "saturation ⊆ I_{S'}" ([BM97, Proposition 3.13] read
in the smooth case): a germ t at p in the saturation (π⁻¹(I_S) : I_F^k) has u^k t in
π⁻¹(I_S) ⊆ I_{S'} for the exceptional coordinate u = u_i of the blow-up chart, so t vanishes
on S' ∖ F ⊇ π⁻¹(S ∖ Y), which is dense in S' = closure (π⁻¹(S ∖ Y)); hence t ∈ I_{S'}
(mem_stalkIdeal_idealSheaf_iff_eventually). S' is any closed-submanifold witness of the strict
transform set; no containment Y ⊆ S is needed.
A closed submanifold containing the centre #
Off the strict
transform set the saturation is the unit ideal — either π p ∉ S (the total transform is ⊤
there), or p lies over the centre in a blow-up chart Φ of index i in which some S-coordinate
u_{σ (τ j)} is a unit at p, so u_i = u_i u_{σ(τ j)} / u_{σ(τ j)} = π^*z_{σ(τ j)} / u_{σ(τ j)}
lies in π⁻¹(I_S) and 1 ∈ (π⁻¹(I_S) : I_F).
The inclusion
"I_{S'} ⊆ saturation": over the centre, in the flag chart, S' is {u_{σ(τ j)} = 0}
on the blow-up charts of index i ∉ range τ (strictTransform_inter_source_of_not_mem_range) and
u_i u_{σ(τ j)} = π^* z_{σ(τ j)} ∈ π⁻¹(I_S), so each generator u_{σ(τ j)} lies in
(π⁻¹(I_S) : I_F); off the centre π is a local isomorphism and the saturation is the total
transform (saturationStalk_of_notMem_cosupport), whose generators z_{σ₁ j} ∘ π are
the coordinates of the transported chart (exists_adaptedChart_strictTransform_off').
Stalkwise, the saturation of the total transform of I_S by the exceptional
divisor is the ideal of the submanifold strict transform S' (both inclusions above).
The saturation stalks have local generators (they are the stalks of the ideal sheaf
idealSheaf of the submanifold S', which is locally finitely generated) — the finite-type clause
holds outright in the smooth case, without any Noetherian hypothesis.
A restatement: the strict
transform X' of a closed submanifold S ⊇ Y IS the closed submanifold Bl_Y S ⊆ Bl_Y M — its
ideal sheaf is idealSheaf of the strict transform set, for any closed-submanifold
witness hS' of that set.
The strict transform of a closed
submanifold S ⊇ Y is the ideal sheaf (IsIdealSheafOf) of the closed
submanifold strictTransformSet π Y S of M', of the codimension of S
(IsClosedSubmanifold.strictTransform supplies the witness).
The points of X' are the strict transform set closure (π⁻¹(S ∖ Y)).
The ideal
sheaf of X' is the greatest of candidates — it is a candidate because its stalks are
the saturation (strictTransform_mem_geometricCandidates_of_hasLocalGenerators), and
every candidate lies in it (geometricCandidates_le_idealSheaf_strictTransform). The geometric
strict transform exists here without local Noetherianity.
The geometric strict transform of a closed submanifold S ⊇ Y
is its strict transform — geometricStrictTransform is the Classical.choice of the
greatest candidate, which isGreatest_geometricCandidates_strictTransform_of_subset exhibits.
A smooth hypersurface with simple normal crossings with the centre #
The inclusion
"I_{H'} ⊆ saturation" for a smooth hypersurface H with snc charts along the centre: at a point
over H ∩ Y take the chart φ of hchart (H = {z_k = 0}) and a blow-up chart Φ of index i;
if k = σ i, H' misses the chart and u_i = π^*z_k ∈ π⁻¹(I_H) makes the saturation ⊤; if
k = σ k' with k' ≠ i, H' = {u_{σ k'} = 0} on the chart and u_i u_{σ k'} = π^* z_k, so the
generator u_{σ k'} lies in (π⁻¹(I_H) : I_F) (and the saturation is ⊤ where u_{σ k'} is a
unit); if k is off the centre, H' = {u_k = 0} and u_k = π^* z_k ∈ π⁻¹(I_H). Off the centre
the saturation is the total transform and the transported chart gives the generator.
Off π⁻¹(H) both sides are ⊤.
Stalkwise, the saturation of the total transform of I_H is the
ideal of the hypersurface strict transform H', for any codimension-one witness hH'.
The saturation stalks have local generators — they are the stalks of the ideal
sheaf of the smooth hypersurface H'
(isClosedSubmanifold_strictTransform_of_charts).
A restatement: the strict transform of a smooth hypersurface
H with snc charts along the centre is idealSheaf of the strict transform set, for any
codimension-one witness hH' of that set.
The strict transform of a smooth hypersurface H with snc charts
along the centre is the ideal sheaf of the smooth hypersurface strictTransformSet π Y H
(isClosedSubmanifold_strictTransform_of_charts).
For a smooth
hypersurface H ⊇ Y, the strict transform of H is the marked transform
π^{-1}_*(I_H, 1) — both are the ideal sheaf of the strict transform set
(isIdealSheafOf_strictTransform, strictTransform_submanifold_eq_blowUp with s = 1).