Restriction of the induced divisors to a hypersurface #
Kollár's going up and down [Kol07, Corollary 85] pushes blow-up sequences between a smooth
hypersurface H and its ambient X when every center lies in the birational transform of H
(a hypersurface of maximal contact, [Kol07, Definition 78]); the proof observes that "E|_H is
again a divisor with simple normal crossings" and that the restriction to H of the divisors
induced on X is the family induced on H by E|_H: E_i|_{H_i} = (E|_H)_i. With the
embeddings H_i ↪ X_i of Hironaka/Scheme/BlowUpSequence/Restrict.lean (closed immersions with
kernels the strict transforms of H) and Kollár's H + E as DivisorFamily.append, this module
proves that identity (totalTransformSeq_comap_pullback) from three pieces:
- the point lemma
hasSncWith_append_of_le: a centerZ ⊆ Hhaving simple normal crossings withEhas simple normal crossings withE + HwhenE + Hhas simple normal crossings (an exchange of coordinates in𝔪/𝔪²); - the stagewise statement: the families
E_i + H_ikeep simple normal crossings along the sequence (AlgebraicGeometry.totalTransform_isSncat each stage, up to the reindexing between(E + H)_1andE_1 + H_1), and the centers have simple normal crossings with them; - the one-step computation
strictTransform_comap_blowUpMap_of_hasSncWith: strict transforms restrict to strict transforms,(π_*^{-1} K)|_{H'} = (π_H)_*^{-1}(K|_H), the chart computation of [Hau14, Proposition 5.3] read on the chart shape of the total transform: modulo the coordinate ofH', the exceptional coordinate is still a member of a regular system of parameters, so the two saturations agree (map_iSup_colon_pow_eq_of_shape).
The statement carries [Smooth f] and IsSmooth S f without a relative dimension, so the stages
are shown smooth over k by Zariski-locality from the equidimensional statement
(smooth_blowUpπ_comp_of_smooth', IsSmooth.smooth_stageMap'). The last section gives the
push-forward of a nonzero ideal sheaf along a closed immersion, used for the intermediate triples
of the chain of hypersurfaces in [Kol07, 108].
Reindexing a divisor family #
Simple normal crossing data at a point transport along a reindexing of the family with matching components.
HasSncWith is invariant under reindexing with matching components.
Stages smooth over k, without a relative dimension #
The blow-up of a scheme smooth over k along a center smooth over k is smooth over k
([Kol07, Notation 19] without the equidimensional convention). Smoothness is Zariski-local on the
source; over an affine open V of X on which f has a relative dimension
(exists_affineOpen_smoothOfRelativeDimension) the blow-up restricts to the blow-up of V
(blowUp.restrictIso), where smoothOfRelativeDimension_blowUpπ_comp_of_smooth applies.
Every stage of a sequence smooth over k is smooth over k [Kol07, Notation 19], without a
relative dimension.
The stalk map of a closed immersion #
The stalk map of a closed immersion is surjective with kernel the stalk of its kernel ideal
sheaf (the factorisation through the image, ker_stalkMap_subschemeι).
The algebra: saturation modulo a coordinate #
The algebra behind [Hau14, Proposition 5.3]: in a regular local ring R with regular system of
parameters z, for the quotient φ : R → S = R/(z_h) and an ideal T of one of the four chart
shapes (z_a z_j), (z_a), (z_j), (1) with a, j ≠ h, saturating by (z_j) commutes with
passing to the quotient: the saturation is computed once in R and once in S, whose regular
system of parameters is the image of the coordinates other than z_h
(span_range_comp_compl_eq_maximalIdeal). Not in the sources in this form.
Strict transforms restrict to strict transforms #
For a closed immersion g : Y ⟶ X with image H = V(g.ker), a center Z = V(D) ⊆ H having
simple normal crossings with E + H, and a component K of E, the strict transform of K
restricted to B_Z H (along the closed immersion blowUpMap g D) is the strict transform of
K|_H: (π_*^{-1} K)|_{H'} = (π_H)_*^{-1}(K|_H) ([Kol07, Corollary 85, proof];
[Hau14, Proposition 5.3]). Stalkwise (ext_stalkIdeal) at y' over x' = blowUpMap g D y': the
stalk map is surjective with kernel the stalk of H' = V(π_*^{-1} H); off the exceptional divisor
both sides are the total transforms; on it, the chart shape for the family E + H
(exists_totalTransformData_of_mem_support) writes F = (z'_j), the total transform of K as
(z'_a z'_j), (z'_a), (z'_j) or (1), and that of H as (z'_{a_H} z'_j) with a_H ∉ {j, a}
(H ⊇ Z and x' ∈ H'), so H' has stalk (z'_{a_H}) and both saturations are computed by
map_iSup_colon_pow_eq_of_shape.
The family form: the total transform of E restricted to B_Z H is the total transform of
E|_H [Kol07, Corollary 85, proof]; componentwise strictTransform_comap_blowUpMap_of_hasSncWith,
and the exceptional divisor of B_Z X restricts to that of B_Z H (exceptionalDivisor_comap).
The point lemma #
Index function for the appended family E + H from one for E and a coordinate for H.
Equations
Instances For
At x ∈ Z with Z ⊆ H = V(J), if Z has simple normal crossings with E and H + E has
simple normal crossings, then Z has simple normal crossings with H + E
[Kol07, Definition 24]. Not in the sources in this form; the argument: in E-adapted coordinates
z with I_Z = (z_s)_{s ∈ S}, write I_H = (g) with g a coordinate of the (E + H)-adapted
system, and g = Σ_{s ∈ S} a_s z_s; if every coefficient at a non-E index lay in 𝔪 then g
would lie in 𝔪² plus the span of the E-coordinates, contradicting notMem_sq_sup_span_image
in the (E + H)-adapted system; so some a_{s₀} is a unit at a non-E index s₀ ∈ S, and
exchanging z_{s₀} for g gives a regular system of parameters adapted to E, H and Z.
The families E_i + H_i along the sequence #
The reindexing between (E + H)_1 = (E + H).totalTransform D and
E_1 + H_1 = (E.totalTransform D).append (strictTransform D J): the two appended slots are
swapped.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The reindexing appendTotalEquiv matches the components: strict transforms of E to strict
transforms of E, H_1 to H_1, the exceptional divisor to itself.
One step: if E + H has simple normal crossings and the center has simple normal crossings
with E + H, then E_1 + H_1 has simple normal crossings, H_1 the strict transform of H
([Kol07, Corollary 85, proof]; AlgebraicGeometry.totalTransform_isSnc).
isSnc_totalTransformSeq_append in the ⟨j, hj⟩ form of the indices: by induction along the
sequence, the head step by the point lemma hasSncWith_append_of_le and
isSnc_totalTransform_append_of_hasSncWith.
Along a smooth blow-up sequence whose centers lie in the strict transforms H_i of H = V(J)
and have simple normal crossings with the induced families E_i, and with E + H having simple
normal crossings, every E_i + H_i has simple normal crossings [Kol07, Corollary 85, proof].
Under the same hypotheses every center Z_i has simple normal crossings with E_i + H_i
(the point lemma hasSncWith_append_of_le at stage i, the stage being smooth over k by
IsSmooth.smooth_stageMap').
Restriction of the induced divisors to H #
totalTransformSeq_comap_pullback for an arbitrary closed immersion g : Y ⟶ X with image
H = V(g.ker), in the ⟨j, hj⟩ form: by induction along the sequence, the head step is the
one-step identity for the family, totalTransform_comap_blowUpMap_of_hasSncWith, and the tail's
embedding blowUpMap g D is again a closed immersion with kernel strictTransform D g.ker, so
that the hypotheses transport: E_1 + H_1 has simple normal crossings by
isSnc_totalTransform_append_of_hasSncWith, the hypotheses on the centers by reindexing.
Let H = V(J) be a smooth hypersurface with H + E having simple normal crossings and S a
smooth blow-up sequence of the kind in [Kol07, Corollary 85]: its centers lie in the strict
transforms H_i and have simple normal crossings with the induced families E_i. Then at every
stage the induced family E_i restricted to H_i (along pullbackStageHom, a closed immersion
onto H_i) is the induced family of the restricted data on H: E_i|_{H_i} = (E|_H)_i
([Kol07, Corollary 85, proof]; the setting of [Kol07, Definition 78]). The case of J.subschemeι
of totalTransformSeq_comap_pullbackStageHom_mk (ker_subschemeι).
Push-forward of a nonzero ideal sheaf along a closed immersion #
The push-forward along a closed immersion ℓ : Y → X of an ideal sheaf nonzero on every
component of Y is nonzero on every component of X (the condition of [Kol07, Notation 64 (2)]
for the intermediate triples (Y_i, (Y ↪ Y_i)_* J, 1, ∅) of the chain of hypersurfaces in
[Kol07, 108]). Off the image of V(Z) the stalk is the unit ideal (Mathlib's support_map); at
ℓ y with y ∈ V(Z) it is the preimage of the stalk Z_y under the surjective stalk map of ℓ
(ker_stalkMap_of_isClosedImmersion applied to V(Z) → Y → X, whose kernel ideal sheaf is
Z.map ℓ), nonzero since Z_y is.