Smooth centers of any shape: local coordinates, the chart of the blow-up, nonvanishing #
Kollár's smooth blow-ups [Kol07, Notation 19 and Definition 66 (2)] have a center Z ⊂ X smooth
over k, possibly reducible, its components possibly of different dimensions: the algorithm blows
up the disjoint components of a stratum simultaneously. The theory of the blow-up of a smooth
center elsewhere in this library (Hironaka/Scheme/Smooth/BlowUpSmooth.lean,
Hironaka/Scheme/IdealSheaf/Order/Lemma61.lean) works with a center of pure codimension r
(SmoothOfRelativeDimension (n - r) (Z.subschemeι ≫ f)), but its proofs are assembled from local
cores whose only inputs at a point x ∈ Z are a regular system of parameters of 𝒪_{X,x} an
initial segment of which generates Z_x. This module produces those inputs for a smooth center as
such and re-runs the local cores.
Adapted parameters. At x ∈ Z, 𝒪_{X,x} is regular and 𝒪_{X,x}/Z_x ≅ 𝒪_{Z,x} is regular
(from Smooth (Z.subschemeι ≫ f) alone), so a regular system of parameters y_0, …, y_{m-1} of
𝔪_x, m = dim 𝒪_{X,x}, can be chosen with Z_x = (y_0, …, y_{c-1}) [TSPA, Tag 00NR], c the
codimension of Z at x, which the statement carries instead of assuming.
The chart of the blow-up at a point. With these parameters, at a point q of B_Z X over
x ∈ Z the stalk 𝒪_{B,q} is the localization of the chart ring 𝒪_{X,x}[y_i/y_ρ] at a prime
over 𝔪_x, compatibly with π^♯ (exists_stalk_equiv_localization_chart_of_smooth); once the
parameters are chosen the proof is local (the chart cover of the local blow-up, and the
identification of the affine blow-up algebra with the chart ring).
Consequences. π^♯ : 𝒪_{X,x} → 𝒪_{B,q} is injective (the chart ring is a subring of
𝒪_{X,x}[1/y_ρ], y_ρ ≠ 0 in the domain 𝒪_{X,x}, and localizations of domains are injective),
so the total transform of an ideal sheaf nonzero at x is nonzero at q; off the exceptional
divisor the blow-up is an isomorphism and the order is unchanged
(ord_controlledTransform_le_of_notMem). Hence π^* I and its controlled transforms are nonzero
everywhere when I is. At a generic point η of an irreducible component of X the only
generization of η is η, so Spec 𝒪_{X,η} is a point and the domain 𝒪_{X,η} is a field; a
center of order ≥ m ≥ 1 therefore contains no component (I_η ⊆ 𝔪_η = 0 would contradict
nonvanishing), Kollár's remark after Lemma 62. Finally the blow-up of an equidimensional smooth
scheme along a smooth center of any shape is smooth of the same relative dimension
(smoothOfRelativeDimension_blowUpπ_comp_of_smooth, [Kol07, Notation 19]), by gluing over the
complement of the center and the charts of adapted étale coordinates at the closed points of the
center, each with its own codimension. These are the facts that make the transform of a triple a
triple (Hironaka/Scheme/BlowUpSequence/Triple.lean).
Adapted parameters at any point x of a smooth center: a regular system of parameters y of
𝒪_{X,x} whose first c members generate Z_x, c the local codimension of Z at x
[TSPA, Tag 00NR].
The chart of the blow-up at a point q of B_Z X over z ∈ Z, for a smooth center of any
shape: the stalk 𝒪_{B,q} is the localization of the chart ring 𝒪_{X,z}[y_i/y_ρ] at a prime
𝔮 lying over 𝔪_z, compatibly with π^♯, for adapted parameters y with Z_z = (y_0, …, y_ρ).
The proof is that of AlgebraicGeometry.exists_stalk_equiv_localization_chart with
exists_adaptedParameters_of_smooth in place of the pure-codimension adapted parameters.
π^♯ : 𝒪_{X,π q} → 𝒪_{B,q} is injective at every point q over the center: through the chart
bridge it is 𝒪_{X,x} → 𝒪_{X,x}[y_i/y_ρ] → 𝒪_{X,x}[y_i/y_ρ]_𝔮, the inclusion of a domain into a
localization at a nonzero element followed by a localization of a domain.
Nonvanishing under one blow-up, at the level of controlled transforms: if I is nonzero at
every point of X, every controlled transform (π^* I : F^m) is nonzero at every point of
B_Z X; over the center by injectivity of π^♯, off it because π is an isomorphism there and
the order is finite. Condition (2) of [Kol07, Notation 64] is thereby preserved.
Generic points of irreducible components #
The only generization of a generic point of an irreducible component is the point itself:
closure {ξ} ⊇ W is irreducible, so equals W by maximality, and W has one generic point.
Spec 𝒪_{X,η} is a point when η is a generic point of an irreducible component: its points
are the generizations of η (range_fromSpecStalk), and Spec 𝒪_{X,η} → X is injective.
At a generic point of an irreducible component, a domain stalk is a field: its spectrum is a
point, so its Krull dimension is 0.
A generic point of an irreducible component of X lying in a closed Z is a generic point of
Z (in the sense of Closeds.genericPoints).
On a smooth X, a closed subscheme Z along which an everywhere-nonzero I has order
≥ m ≥ 1 contains no irreducible component of X: at the generic point of such a component the
stalk is a field, so I_η ⊆ 𝔪_η^m = 0. This is why codimension-one components of the cosupport
need separate treatment, Kollár's remark after [Kol07, Lemma 62].
The blow-up of a smooth center of any shape is smooth #
Adapted coordinates at a closed point of a smooth center: n parameters generating 𝔪_x,
the first c generating Z_x.
Étale coordinates adapted to a smooth center at a closed point, with the local codimension:
the proof of nonempty_etaleCoordinatesAdapted from exists_adaptedCoordinates_of_smooth.
The blow-up of an equidimensional smooth scheme along a smooth center of any shape is smooth
of the same relative dimension ("if π_{Z,X} is a smooth blow-up, then F and B_Z X are both
smooth", [Kol07, Notation 19]). Smoothness is Zariski local on the source; it is checked over the
complement of the center and on the charts of adapted étale coordinates at the closed points of
the center, each with its own codimension.
B_Z X is smooth over k for a smooth center of any shape [Kol07, Notation 19].