The exceptional divisor over a chart of adapted coordinates #
f : X ⟶ Spec k, Z an ideal sheaf on X, and a chart E : EtaleCoordinatesAdapted f n r Z x:
an affine open U ∋ x with étale g = toAffineSpace f U v : U ⟶ 𝔸ⁿ_k and Z ∩ U = g⁻¹(L),
L = coordinateSubspace k n r. The chart computation of
Hironaka/Scheme/Smooth/BlowUpSmoothChart.lean gives a cartesian square IsPullback φ π_U π_L g,
B_{Z∩U} U ≅ U ×_{𝔸ⁿ} B_L 𝔸ⁿ. This file does the same for the exceptional divisors: F_U ≅ U ×_{𝔸ⁿ} F_L, and consequently F_U is smooth of relative dimension n − 1 over k and F_U → Z ∩ U is
smooth of relative dimension r − 1, the chart form of "if π_{Z,X} is a smooth blow-up, then F
… [is] smooth" [Kol07, Notation 19].
Why the theorems hold. The exceptional ideal of B_{Z∩U} U is
(Z ∩ U)·𝒪 = (g⁻¹L)·𝒪 = (π_U ≫ g)⁻¹L = (φ ≫ π_L)⁻¹L = φ⁻¹(F_L): inverse images of ideal
sheaves compose (IdealSheafData.comap_comp) and the square commutes
(comap_π_eq_comap_of_isPullback). The closed subschemes of an ideal sheaf and of its inverse
image form a cartesian square over the morphism (Mathlib's isPullback_of_isClosedImmersion),
and pasting it on top of the square of BlowUpSmoothChart.lean gives F_U ≅ U ×_{𝔸ⁿ} F_L
(exists_isPullback_exceptional). The projection ψ : F_U → F_L is then a base change of the
étale g, hence étale; so F_U → Spec k = ψ ≫ (F_L → Spec k) is smooth of relative dimension
0 + (n − 1) by the model (smoothOfRelativeDimension_exceptional_comap). Cancelling the bottom
square Z ∩ U = U ×_{𝔸ⁿ} L (adaptedness) from the big square shows F_U → Z ∩ U is the base
change of F_L → L along Z ∩ U → L, hence smooth of relative dimension r − 1
(smoothOfRelativeDimension_subschemeMap_exceptional_comap); composing with the open immersion
Z ∩ U → Z keeps the relative dimension.
Main declarations #
AlgebraicGeometry.isPullback_subschemeMap_of_isPullback: closed subschemes of an ideal sheaf and its inverse image, pasted onto a cartesian square.AlgebraicGeometry.subschemeMap_comp_subschemeMap: composition of induced maps of subschemes.AlgebraicGeometry.comap_π_eq_comap_of_isPullback(the ideal),exists_isPullback_exceptional(the schemes),etale_exceptionalMapOfIsPullback(the projectionF_U → F_Lis étale).AlgebraicGeometry.smoothOfRelativeDimension_exceptional_comap:F_U → Spec kis smooth of relative dimensionn − 1.AlgebraicGeometry.smoothOfRelativeDimension_subschemeMap_exceptional_comap,smoothOfRelativeDimension_subschemeMap_exceptional_comap_comp:F_U → Z ∩ UandF_U → Zare smooth of relative dimensionr − 1.
Hironaka/Scheme/Smooth/ExceptionalDivisor.lean glues these chart statements over the Jacobson
cover.
Pasting of closed subschemes: for a cartesian square IsPullback φ p q g and an ideal sheaf
J on X with inverse image K = J.comap φ on P, the closed subschemes V(K) → Y, V(J) → S
form a cartesian square over g (Mathlib's isPullback_of_isClosedImmersion pasted on top).
Composition of the induced maps of closed subschemes.
In a cartesian square IsPullback φ π_U π_L g as in exists_isPullback_blowUp, the
exceptional ideal of B_{Z∩U} U is the inverse image along φ of the model's exceptional ideal:
Z ∩ U = g⁻¹(L) and π_U ≫ g = φ ≫ π_L.
The model's exceptional ideal pushes forward along φ to contain the chart's.
The projection ψ : F_U → F_L of the exceptional divisors, the restriction of φ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
F_U ≅ U ×_{𝔸ⁿ} F_L: the square of the exceptional divisors over g, pasted onto the
cartesian square of the blow-ups, is cartesian.
F_U ≅ U ×_{𝔸ⁿ} F_L, in existential form: a map ψ : F_U → F_L over φ making the square of
the exceptional divisors over g cartesian.
The projection ψ : F_U → F_L is étale, being a base change of the étale g (as
etale_of_isPullback_blowUp).
F_U → Spec k is smooth of relative dimension n − 1, the composite of the étale ψ with the
model's F_L → 𝔸ⁿ → Spec k (the smoothness of the exceptional divisor of [Kol07, Notation 19],
over a chart).
Adaptedness as a pushforward inequality: L ≤ g_*(Z ∩ U).
Adaptedness as a cartesian square: Z ∩ U = U ×_{𝔸ⁿ} L.
The square F_U → F_L, F_U → Z ∩ U, F_L → L, Z ∩ U → L is cartesian: cancel the
adaptedness square from the bottom of the square F_U ≅ U ×_{𝔸ⁿ} F_L.
F_U → Z ∩ U is smooth of relative dimension r − 1, the base change of the model's F_L → L
along Z ∩ U → L.
Z ∩ U → Z is an open immersion (the base change of U → X).
Z ≤ (π_U ≫ U.ι)_* F_U, the pushforward inequality behind F_U → Z.
Composed with the open immersion Z ∩ U → Z: F_U → Z is smooth of relative dimension
r − 1.