The stalks of B_Z X along the exceptional divisor are localizations of the chart ring #
Kollár's proof of Lemma 61 "chooses local coordinates as above" at a point of the exceptional
divisor ([Kol07, Lemma 61]): in adapted parameters y at z = π(q) ∈ Z with Z_z = (y_0, …, y_ρ),
the point q lies in the chart of some y_j, j ≤ ρ, of the local blow-up of Spec 𝒪_{X,z}
along Z_z (the cartesian square of LocalBlowUp.lean), whose stalks are those of B_Z X
(LocalBlowUpStalk.lean), and the chart is Spec of the affine blow-up algebra
𝒪_{X,z}[Z_z/y_j], which is the chart ring chartRing y' ρ of Kollár's coordinates (60.2) once
the parameters are permuted so that y_j is the last center coordinate
(affineBlowUpAlgebra_span_eq_chartRing, ChartRing.lean). So 𝒪_{B,q} is the localization of
the chart ring at a prime 𝔮 of the fibre over 𝔪_z, compatibly with π^♯
(exists_stalk_equiv_localization_chart): the identification
exists_stalk_equiv_localization_chartOrigin_of_isIso at the origin of the chart, extended to
every point over z (Hauser's local blow-up at any point of the fibre, [Hau14, Definition 4.16]).
The steps: hasChartData_of_chart runs the identification from a given point of a chart instead
of its origin (the chart data packaged as the predicate HasChartData), exists_hasChartData
finds the chart of some generator y_j containing the point (the charts cover the affine
blow-up), and the main theorem permutes the parameters and identifies the algebra with chartRing
by two transports of the packaged data.
Used for the order of an ideal at a point of the exceptional divisor
(Hironaka/Scheme/IdealSheaf/Order/Lemma61.lean) and for the transform of a smooth center
(Hironaka/Scheme/BlowUpSequence/SmoothCenter.lean).
The chart data at a point q of B_Z X over x, for a subalgebra C ⊆ 𝒪_{X,x}[1/a]: a prime
𝔮 of C lying over 𝔪_x and an isomorphism 𝒪_{B,q} ≅ C_𝔮 compatible with π^♯ on germs.
(Packaged as a predicate so that the identifications of the generator and of the chart algebra are
cheap transports.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
The chart data at a chart point of the local blow-up (the identification of LocalBlowUp.lean
run from a given point of the chart instead of its origin): for a point p of the chart of a
lying over 𝔪_x, 𝒪_{B,φ(chart p)} is the localization of the affine blow-up algebra at p.
The chart at a point of the fibre: for q ∈ B_Z X over x and adapted parameters y with
Z_x = (y_0, …, y_ρ), the point q lies in the chart of some y_j, j ≤ ρ, of the local
blow-up (the charts cover the affine blow-up), and the chart data of hasChartData_of_chart hold
there.
The identification with PRESCRIBED adapted parameters: at q ∈ B_Z X over z = π(q), for any
y with Z_z = (y_0, …, y_ρ) = chartCenter y ρ, the point q lies in the chart of some y_j,
j ≤ ρ, and after the transposition (j ρ), which keeps the center, 𝒪_{B,q} is the
localization of the chart ring 𝒪_{X,z}[y_i/y_j] at a prime 𝔮 lying over 𝔪_z, compatibly
with π^♯.
At a point q of B_Z X over z ∈ Z, for suitable adapted parameters y at z with
Z_z = (y_0, …, y_ρ), the stalk 𝒪_{B,q} is the localization of the chart ring 𝒪_{X,z}[y_i/y_ρ]
at a prime 𝔮 lying over 𝔪_z, compatibly with π^♯ ("choose local coordinates as above", the
proof of [Kol07, Lemma 61]; Hauser's local blow-up, [Hau14, Definition 4.16]).