Smooth blow-ups of order m are Zariski-local: descent of Definitions 65 and 66 #
The proof of [Kol07, Proposition 37] glues the first centers Z₀ᵢ' ⊂ Uᵢ of the local sequences
to a center Z₀ ⊂ X and continues "this way we obtain X₁ := B_{Z₀} X"; that the glued center
is again a smooth blow-up of order m for (X, I, E) ([Kol07, Definition 65]: Z₀ smooth
over k, having simple normal crossings with E, with ord_{Z₀} I = m) is left implicit, the
three conditions being local on X. This module proves it, for a covering family of open
immersions ι i : W i → X along which the center and the data are pulled back, and then for the
cover g : X' = ∐ Uᵢ → X of Hironaka/Resolution/Algebraic/Kol07/Prop37/Prop37Setting.lean (where
the conditions on X' first restrict to the pieces Uᵢ by the smooth-pullback lemmas of
Hironaka/Sequence/Pullback*.lean, the inclusions being open immersions). It then shows that the
condition of
[Kol07, Definition 66] on a whole sequence is local, and combines this with the descent of
Hironaka/Resolution/Algebraic/Kol07/Prop37/Prop37Descent.lean.
- Smoothness (
smooth_subschemeι_comp_of_covers):V(Z) → Spec kis smooth when its restrictions to the open piecesV(Z|_{Uᵢ}) = V(Z) ∩ Uᵢare; smoothness is local at the source (Mathlib'sIsZariskiLocalAtSource, applied by hand), the pieces being an open cover ofV(Z)by the base-change squaresAlgebraicGeometry.isPullback_subschemeι_comap. - Simple normal crossings (
hasSncWith_of_covers): condition (4) of [Kol07, Definition 24] is a condition at each pointx ∈ Zon the stalk𝒪_{X,x}; an open immersionιis an isomorphism on stalks, so the coordinates atw ∈ ι⁻¹ Ztransport to coordinates atι w: regular systems of parameters along a ring isomorphism (isRegularSystemOfParameters_comp_ringEquiv), the stalks of the inverse images being the images of the stalks (stalkIdeal_comap). This is the transport of snc data along a smooth morphism in the other direction, available because the stalk map is invertible. - The order (
ordAlongEq_of_covers,leOrdAlong_of_covers):ord_Z Iis computed at the generic points ofZ; a generic point ofZlying inUᵢis a generic point ofZ ∩ Uᵢ(specialisation is reflected by an open embedding,mem_genericPoints_comap_of_isOpenImmersion), and the order at a point is invariant under open immersions (ord_comap_of_isOpenImmersion). - The triples (
Triple.isOrderBlowUp_of_isPullbackOf_covers,Triple.isOrderBlowUp_of_coverDescand the marked versions): the corollaries in the vocabulary of Definition 65 on triples carrying the pullback data (IsPullbackOf), thecoverDescform restricting the hypothesis onX'to the summandsUᵢalong the open immersionsSigma.ιfirst. - Definition 66 is local, stage by stage (
isOrderSeq_of_covers,isOrderGeSeq_of_covers): a blow-up sequence onXis a smooth blow-up sequence of ordermfor(X, I, E)when its pullbacks to the members of a covering family of open immersions are, for the pulled-back data. By induction on the sequence: the first center's three conditions descend (above); then the induced data of the pullbacks are the pullbacks of the induced data (the total transform along any flat morphism; the weak transform because the order along the center is now known onX,weakTransform_comap_of_orderAlong_of_equidim; the marked transform along any flat morphism givenF^m ∣ π^* I), so the tails are pullbacks of the tail onZ₀.blowUpalong the lifted covering family, to which the induction hypothesis applies. - The descent with the order (
Triple.exists_isOrderSeq_pullback_eq_of_agreeOnOverlaps,Triple.exists_isOrderSeq_pullback_coverDesc_eq, marked versions): the descent of the sequence (exists_pullback_eq_of_agreeOnOverlaps,Triple.exists_pullback_coverDesc_eq) followed by the locality of Definition 66; on the affine cover the hypothesis onX'restricts to the summands first (IsOrderSeq.pullback_of_equidim).
Transport of local coordinates along a ring isomorphism #
A regular system of parameters transports along an isomorphism of local rings: the image of the maximal ideal is the maximal ideal (a surjection of local rings is a local homomorphism) and the Krull dimension is invariant.
Descent of the stalk conditions along an open immersion #
The stalk map of an open immersion, as a ring isomorphism 𝒪_{X, ι w} ≃ 𝒪_{W, w}.
Equations
Instances For
The stalk of an ideal sheaf at ι w is the preimage, under the stalk isomorphism, of the stalk
of its inverse image at w (stalkIdeal_comap read backwards).
Coordinates at w transport to coordinates at ι w along the stalk isomorphism.
Equations
- Hironaka.Sequence.transportCoords ι w z i = (Hironaka.Sequence.stalkEquivOfIsOpenImmersion ι w).symm (z i)
Instances For
Simple normal crossings at a point [Kol07, Definition 24] descend along an open immersion:
the coordinates at w transport to coordinates at ι w, the components of E through ι w are
the components of ι⁻¹ E through w, and their stalks correspond (the stalk map being an
isomorphism).
Simple normal crossings of a closed subscheme with a family [Kol07, Definition 24 (4)]
descend along a covering family of open immersions: at a point x = ι i w of Z the coordinates
at w for ι⁻¹ Z, ι⁻¹ E transport to x.
Descent of the order along an open immersion #
A generic point of Z lying in the image of the open immersion ι comes from a generic point
of ι⁻¹ Z: specialisation is reflected by an open embedding, so a generisation of w in ι⁻¹ Z
maps to a generisation of ι w in Z, which is ι w itself.
The order condition ord_Z I = m of [Kol07, Definition 65 (2)] descends along a covering
family of open immersions: every generic point of Z is a generic point of some Z ∩ Uᵢ, where
the order is that of the inverse image.
The marked form: ord_Z I ≥ m descends along a covering family of open immersions.
Descent of smoothness of the centre along an open cover #
Smoothness of the center ([Kol07, Definition 65 (1)] with Notation 19): V(Z) → B is smooth
when its restrictions to the open pieces V(Z|_{Uᵢ}) = V(Z) ∩ Uᵢ of a covering family of open
immersions are; smoothness is local at the source (IsZariskiLocalAtSource, applied by hand),
the pieces forming an open cover of V(Z) by the base-change squares
AlgebraicGeometry.isPullback_subschemeι_comap.
Definition 66 is local: stagewise descent along a covering family of open immersions #
The condition of [Kol07, Definition 66] is local: a blow-up sequence on X is a smooth blow-up
sequence of order m for (X, I, E) when its pullbacks along a covering family of open
immersions are, for the pulled-back data (the recursion of the proof of
[Kol07, Proposition 37]). Induction on the sequence: the first center's conditions descend
(smooth_subschemeι_comp_of_covers, hasSncWith_of_covers, ordAlongEq_of_covers); with the
order along the center known on X, the weak and total transforms commute with the pullbacks
along the lifted family, so the tails are the pullbacks of the tail along the lifted covering
family, and the induction hypothesis applies on Z₀.blowUp.
The marked condition of [Kol07, Definition 66] is local: the marked transform commutes with
the pullbacks along the lifted family for any flat morphism, given F^m ∣ π^* I (from the order
≥ m along the center, now known on X).
Descent of Definition 65 on triples #
If the inverse images of a center Z ⊂ X along a covering family of open immersions
ι i : (Ts i).X.left → T.X.left, the Ts i carrying the pullback data of T, are smooth blow-ups
of order m ([Kol07, Definition 65]) for the Ts i, then Z is one for T: the three conditions
are local on X (smooth_subschemeι_comp_of_covers, hasSncWith_of_covers,
ordAlongEq_of_covers). This is the step left implicit in the proof of
[Kol07, Proposition 37].
The marked version: a center whose inverse images are smooth blow-ups of order ≥ m for the
pieces is one for T.
Descent of Definition 65 along the affine cover #
The members Uᵢ → X of the affine cover form a covering family of open immersions.
A center of X whose inverse image on X' is a smooth blow-up of order m for
(X', g^* I, g^{-1} E) is one for (X, I, E): the three conditions restrict from X' = ∐ Uᵢ to
each summand Uᵢ along the open immersion Sigma.ι i (the smooth-pullback lemmas), and descend
from the summands to X.
The marked version along the affine cover.
The descent with the order #
The descent of the proof of [Kol07, Proposition 37] with the order condition of
[Kol07, Definition 66]: if each S i is a smooth blow-up sequence of order m for the
pullback-data triple Ts i, the descended sequence (exists_pullback_eq_of_agreeOnOverlaps) is
one for T, Definition 66 being local (isOrderSeq_of_covers).
Kollár's form of the descent with the order (the proof of [Kol07, Proposition 37]): a smooth
blow-up sequence of order m for (X', g^* I, g^{-1} E) with τ₁^* S' = τ₂^* S' is g^* S for a
smooth blow-up sequence S of order m for (X, I, E); the descent of the sequence, the
hypothesis restricted to the summands Uᵢ of X' (IsOrderSeq.pullback_of_equidim along the
open immersions Sigma.ι), and the locality of Definition 66.
The marked version of the descent with the order.
The marked version of Kollár's form of the descent, with the order ≥ m.