The exceptional divisor of the model blow-up is smooth #
The model case of the smoothness of the exceptional divisor of a smooth blow-up: the blow-up
B_L 𝔸ⁿ_A of 𝔸ⁿ_A = Spec A[x_0, …, x_{n-1}] along the coordinate subspace
L = V(x_0, …, x_{r-1}), with exceptional divisor F_L = π⁻¹(L) (the blow-up via the Rees
algebra, [Hau14, Definition 4.7]). Kollár's sentence "if π_{Z,X} is a smooth blow-up, then F …
[is] smooth" [Kol07, Notation 19] is stated without proof;
Hironaka/Scheme/Smooth/ExceptionalChart.lean and ExceptionalDivisor.lean reduce it to the model,
and this file proves the model.
Why the theorems hold. In the chart U_j (j < r) the exceptional ideal pulls back along the
chart U_j ≅ 𝔸ⁿ_A to the ideal (x_j), so F_L ∩ U_j = V(x_j) = Spec A[x]/(x_j) ≅ 𝔸^{n-1}_A,
smooth over A of relative dimension n − 1 (smoothOfRelativeDimension_quotient_span_X); and
through the chart map π_j (x_i ↦ x_i x_j for i < r, i ≠ j) the ring A[x]/(x_j) is the
polynomial ring over 𝒪(L) = A[x]/I in the r − 1 variables x_i, i < r, i ≠ j
(fibreAlgEquivOverCenter), so V(x_j) → L is smooth of relative dimension r − 1 (cf. Hau14,
Example 5.9). The charts U_j, j < r, cover B_L 𝔸ⁿ, hence the pieces
F_L ∩ U_j cover F_L, and both smoothness statements are Zariski-local on the source. Two
bookkeeping identifications make this a proof about the glued blow-up: the closed subscheme of
the ideal sheaf of an ideal J on Spec S is Spec (S/J) (specQuotientToSubscheme, an
isomorphism because both are closed immersions with the same kernel), and the glued blow-up
blowUp (coordinateSubspace k n r) is identified with the affine model over 𝔸ⁿ by the
uniqueness of blow-ups (exists_iso_blowUp_coordinateSubspace), which carries the exceptional
divisors and the maps to L along (prop_subschemeι_comp_iff_of_eq_comap,
prop_subschemeMap_iff_of_eq_comap).
Main declarations #
AlgebraicGeometry.specQuotientToSubscheme:Spec (R/I) ≅ V(I)overSpec R, and the transport lemmasprop_subschemeι_comp_iff_of_eq_specIdealSheaf,prop_subschemeMap_iff_of_eq_specIdealSheaf(a morphism property ofV(J) → Y, or of the inducedV(J) → V(I), read onSpec (S/J) → Y, or onSpec (S/J) → Spec (R/I)).AlgebraicGeometry.isIso_subschemeMap_comap_of_isIso,prop_subschemeι_comp_iff_of_eq_comap,prop_subschemeMap_iff_of_eq_comap: the same along an isomorphism of ambient schemes.AlgebraicGeometry.CoordinateSubspace.exceptionalCover: the open cover ofF_Lby the piecesF_L ∩ U_j,j < r.AlgebraicGeometry.CoordinateSubspace.smoothOfRelativeDimension_exceptionalIdeal_modelBlowUp:F_L → Spec Ais smooth of relative dimensionn − 1.smoothOfRelativeDimension_subschemeMap_exceptionalIdeal_modelBlowUp(same namespace):F_L → Lis smooth of relative dimensionr − 1.AlgebraicGeometry.smoothOfRelativeDimension_exceptional_coordinateSubspace,AlgebraicGeometry.smoothOfRelativeDimension_subschemeMap_exceptional_coordinateSubspace: the two statements for the gluedblowUp (coordinateSubspace k n r).
The closed immersion Spec (R/I) → Spec R factored through the closed subscheme V(I) of the
ideal sheaf specIdealSheaf I of I: an isomorphism, both being closed immersions with kernel
the ideal sheaf of I.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The exceptional ideal of the affine blow-up contains the pullback of the center's ideal sheaf:
I·𝒪_B is the inverse image of I, so I ≤ π_*(I·𝒪_B) (Mathlib's le_map_comap, stated with
the exceptional ideal's name so that subschemeMap terms carry a syntactically matching proof).
A morphism property of V(J) → Y, for J the ideal sheaf of an ideal I on Spec R, is read
on Spec (R/I) → Y.
A morphism property of the map of closed subschemes V(J) → V(I) induced by
Spec φ : Spec S → Spec R (φ : R → S carrying I into J) is read on
Spec (R/I → S/J).
The closed subscheme of the inverse image of J along an isomorphism maps isomorphically onto
V(J) (Mathlib's isPullback_of_isClosedImmersion).
A morphism property of V(K) → Y transports along an isomorphism e : B ≅ B' carrying K
to J (K = J.comap e).
A morphism property of the induced map V(K) → V(L) transports along an isomorphism
e : B ≅ B' carrying K to J.
The piece F_L ∩ U_j of the model's exceptional divisor over the chart U_j, as the closed
subscheme of the inverse image ideal, mapping into F_L (an open immersion).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pieces F_L ∩ U_j, j < r, cover F_L (the charts cover B_L 𝔸ⁿ,
iSup_opensRange_modelChart).
The open cover of the model's exceptional divisor F_L by its chart pieces F_L ∩ U_j,
j < r.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Over Spec A the chart U_j is Spec A[x] → Spec A (the chart map is an A-algebra map).
On the chart U_j: the piece F_L ∩ U_j = Spec A[x]/(x_j) ≅ 𝔸^{n-1}_A is smooth over A of
relative dimension n − 1.
The exceptional divisor F_L of B_L 𝔸ⁿ_A is smooth over A of relative dimension n − 1
(the model case of [Kol07, Notation 19]): on the piece F_L ∩ U_j = Spec A[x]/(x_j) ≅ 𝔸^{n-1}_A
by the chart computation, and smoothness is Zariski-local on the source.
In the chart U_j: V(x_j) → L, Spec of the map A[x]/I → A[x]/(x_j) induced by the chart
map, is smooth of relative dimension r − 1, A[x]/(x_j) being the polynomial ring over 𝒪(L)
in the r − 1 variables x_i, i < r, i ≠ j (cf. [Hau14, Example 5.9]).
On the chart U_j: the piece F_L ∩ U_j → L of F_L → L is Spec (A[x]/I → A[x]/(x_j)),
smooth of relative dimension r − 1.
F_L → L is smooth of relative dimension r − 1: on the piece F_L ∩ U_j it is
Spec (A[x]/I → A[x]/(x_j)), and smoothness is Zariski-local on the source.
Under the identification e of the glued blowUp (coordinateSubspace k n r) with the model
(exists_iso_blowUp_coordinateSubspace), the exceptional divisor F_L of the glued blow-up is the
inverse image of the model's exceptional ideal.
The exceptional divisor of the glued blowUp (coordinateSubspace k n r) is smooth over k of
relative dimension n − 1.
F_L → L is smooth of relative dimension r − 1 for the glued
blowUp (coordinateSubspace k n r).