The exceptional divisor of a smooth blow-up is smooth #
Kollár: "If π_{Z,X} is a smooth blow-up, then F and B_Z X are both smooth"
[Kol07, Notation 19], the sentence for F = π⁻¹(Z), stated there without proof. Setting: X
smooth over the perfect field k of relative dimension n, V(Z) smooth of relative dimension
n − r, r ≤ n. Proved here: F → Spec k is smooth of relative dimension n − 1, F → Z is
smooth of relative dimension r − 1, and so is every fibre F_z → Spec κ(z).
Why the theorems hold. At every closed point x of V(Z) there is a chart U ∋ x of étale
coordinates adapted to Z (EtaleCoordinatesAdapted), and over U the blow-up is the fibre
product with the model, B_{Z∩U} U ≅ U ×_{𝔸ⁿ} B_L 𝔸ⁿ (BlowUpSmoothChart.lean), so its
exceptional divisor is F_U ≅ U ×_{𝔸ⁿ} F_L (ExceptionalChart.lean). The model's F_L is smooth
of relative dimension n − 1 over k and F_L → L is smooth of relative dimension r − 1
(ExceptionalModel.lean), and both properties pass to F_U by base change along the étale g,
resp. along Z ∩ U → L (ExceptionalChart.lean). Now π⁻¹(U) ≅ B_{Z∩U} U (restrictIso), and
the pieces F ∩ π⁻¹(U) = F_U cover F: a point of F lies over a point of V(Z), which lies in
one of the charts U_x because the charts and X ∖ V(Z) cover the Jacobson space X (the cover
of BlowUpSmooth.lean). Smoothness of relative dimension m is Zariski-local on the source, which
gives the smoothness of F → Spec k (relative dimension n − 1) and of F → Z (relative
dimension r − 1); the fibre of F → Z over z ∈ Z is its base change along Spec κ(z) → Z,
smooth of relative dimension r − 1 over κ(z).
Main declarations #
AlgebraicGeometry.exceptionalRestrictPiece:F_U → F, the open immersion of the exceptional divisor ofB_{Z∩U} Uinto that ofB_Z X, withexists_exceptionalRestrictPiece_eq.AlgebraicGeometry.exceptionalDivisorCover: the open cover ofFby the pieces over the adapted charts at the closed points ofV(Z).AlgebraicGeometry.smoothOfRelativeDimension_exceptional,smooth_exceptional:Fis smooth overkof relative dimensionn − 1.AlgebraicGeometry.smoothOfRelativeDimension_subschemeMap_exceptional:F → Zis smooth of relative dimensionr − 1, over a perfect field (the arbitrary-field form is obtained by descent inExceptionalBaseChange.leanandExceptionalDivisorSmooth.lean).AlgebraicGeometry.smoothOfRelativeDimension_fiberToSpecResidueField_exceptional: the fibres ofF → Zare smooth of relative dimensionr − 1.
The projective-bundle structure of F over Z is in ExceptionalBundle.lean.
Two induced maps of closed subschemes along equal morphisms are equal.
blowUpMap U.ι I : B_{I|_U} U ⟶ B_I X is an open immersion: it is π⁻¹(U) → B_I X up to the
isomorphism restrictIso.
The exceptional divisor of B_I X, pulled back to B_{I|_U} U, is the exceptional divisor of
the latter (blowUpMap U.ι I ≫ π = π_U ≫ U.ι).
The piece of the exceptional divisor over U: F_U → F, the restriction of blowUpMap U.ι I
to the exceptional divisors.
Equations
- AlgebraicGeometry.exceptionalRestrictPiece I U = ((I.comap U.ι).comap (I.comap U.ι).blowUpπ).subschemeMap (I.comap I.blowUpπ) (AlgebraicGeometry.Scheme.Hom.blowUpMap U.ι I) ⋯
Instances For
F_U is the base change of F along blowUpMap U.ι I.
A point of F lying over U is in the image of the piece F_U.
I ≤ (blowUpMap U.ι I ≫ π)_* F_U, the pushforward inequality behind F_U → F → V(I).
A chart of étale coordinates adapted to Z at a closed point of V(Z)
(nonempty_etaleCoordinatesAdapted).
Equations
- AlgebraicGeometry.adaptedChart f n r Z hrn x = Classical.choice ⋯
Instances For
The pieces F_{U_x} over the adapted charts at the closed points x of V(Z) cover F:
a point of F lies over a point of V(Z), which lies in some U_x by the Jacobson cover (the
charts and X ∖ V(Z) cover X, iSup_eq_top_of_forall_isClosed).
The open cover of the exceptional divisor F by the pieces F_{U_x} over the adapted charts
at the closed points of V(Z).
Equations
- One or more equations did not get rendered due to their size.
Instances For
On the piece over a chart: F_{U_x} → F → B_Z X → Spec k is smooth of relative dimension
n − 1 (it is F_{U_x} → B_{Z∩U} U → U → Spec k, ExceptionalChart.lean).
The exceptional divisor of a smooth blow-up is smooth over k of relative dimension n − 1
("if π_{Z,X} is a smooth blow-up, then F … [is] smooth", [Kol07, Notation 19]): étale-locally
the model's F_L, covered by copies of 𝔸^{n-1}, pulled back along the étale F_U → F_L, glued
over the Jacobson cover as in BlowUpSmooth.lean.
In Kollár's words [Kol07, Notation 19]: F is smooth over k.
On the piece over a chart: F_{U_x} → F → Z is smooth of relative dimension r − 1 (it is
F_{U_x} → Z ∩ U → Z, ExceptionalChart.lean).
Over a perfect field, F → Z is smooth of relative dimension r − 1 ([Kol07, Notation 19];
the projective bundle of [Hau14, Definition 4.8]): on the piece over a chart it is the base change
of the model's F_L → L along Z ∩ U → L, glued over the Jacobson cover.
For z ∈ Z the fibre F_z = F ×_Z Spec κ(z) of F → Z is smooth over Spec κ(z) of
relative dimension r − 1 (the base change of smoothOfRelativeDimension_subschemeMap_exceptional
along Spec κ(z) → Z).