The one-step descent of agreement through a blow-up #
The inductive step in the proof of [Kol07, Theorem 97] (compare the proof of the gluing lemma
[Wlo05, Lemma 2.9.5]). This file proves agreeOn_blowUpMap: for morphisms f, g : U ⟶ X, a
centre C ⊆ X with f^{-1} C = g^{-1} C =: J and an ideal sheaf M ≤ J on which f, g agree,
the lifts f̃, g̃ : B_J U ⟶ B_C X agree on V(π^{-1}_*(M, 1)); this is the step that the
induction of Hironaka/Resolution/Algebraic/MaximalContact/Theorem97Induction.lean takes as a
hypothesis, in the same spelling. Its corollary step_agreeOn adds the equality of the centres. No
smoothness, étaleness or flatness enters the descent itself; flatness appears only in
step_agreeOn, through the descent of the centres.
The proof #
Kollár's computation is written in local coordinates on a chart of the blow-up. Fix a point u
of V(M'), M' := π^{-1}_*(M, 1); its image π u lies in V(M), so f (π u) = g (π u).
- The chart. Take an affine
V ∋ f (π u); the chartsSpec A[C(V)/c],c ∈ C(V), coverπ_X^{-1} V, sof̃ ulies in the chart of somec. On that chart the exceptional ideal ofB_C Xis generated byπ_X^* c, hence𝒪(F)is generated atubye := π^* f^* c(stalkIdeal_exceptionalDivisor_eq_span). - The defects divided. For
b ∈ C(V)the defectπ^*(f^* b − g^* b)lies inπ^* M, andπ^* M = 𝒪(F) · M', soπ^* g^* b = π^* f^* b − e · d_bwithd_b ∈ M'_u(exists_mem_markedTransform_mul_eq). - The common chart (a step absent from the printed proof). In particular
π^* g^* c = e (1 − d_c)with1 − d_ca unit atu, soπ^* g^* cgenerates𝒪(F)atuas well; reading this on whichever chartc'containsg̃ u, the ratioc / c'is a unit there (two nonzerodivisor generators of a principal ideal differ by a unit), sog̃ ulies in the chart ofctoo (mem_chartOpen_of_stalkIdeal_eq_span, viachart_preimage_chart). - Generators. Choose an affine
W ∋ uinside both chart preimages. The chart algebra is generated as a ring by the image ofA = Γ(X, V)and the ratiosb / c(subring_closure_chart_generators_eq_top). The pulled-back sections of the base functions areπ^* f^* randπ^* g^* r, whose difference lies inπ^* M ≤ M'. For the ratios,a_b · e = π^* f^* banda'_b · π^* g^* c = π^* g^* b, so at every pointwofW ∩ V(M')(whereeis a nonzerodivisor generating𝒪(F)) Kollár's identity(1 − d_c)(a_b − a'_b) = d_b − d_c a_bholds (ratio_identity) anda_b − a'_b ∈ M'_w. OffV(M')the stalk ofM'is the unit ideal. Hence the defects of all generators lie inM'(W)(mem_ideal_of_forall_germ_mem, the local-global principle for ideal membership). - From generators to morphisms. The two lifts of
W ∩ V(M')into the affine chart are equal (ext_of_isAffineand the ring-level generation lemma), sof̃andg̃agree on the affine pieceW ∩ V(M')(eq_comp_of_forall_gen); equality of morphisms is local on the source (hom_ext_of_forall).
Points of the blow-ups are written in Mathlib's coercion spelling φ w; the stalk of Spec A at
q receives A through chartGerm (Mathlib's StructureSheaf.toStalk; the same map as
AlgebraicGeometry.specGerm of Hironaka/Scheme/BlowUp/AffineBlowUp/Universal/Membership.lean),
and every identity between stalk elements is proved by explicit congruences and Eq.trans chains
rather than by rewriting, which would unfold the glued blow-up.
Base points #
Two morphisms agreeing on V(M) take the same value at every point of V(M).
Sections from germs on an affine open #
The local-global principle for ideal membership: a section over an affine open whose germ at
every point lies in the stalk of I lies in I (Mathlib's Ideal.mem_of_localization_maximal,
the stalks at the points of an affine open being its localizations at maximal ideals).
Two generators of a principal ideal #
Two generators of one principal ideal differ by a unit when one of them is a nonzerodivisor.
At a point where 𝒪(F) is generated by e, every element of the stalk of π^* M is e · d
with d in the stalk of π^{-1}_*(M, 1): the identity 𝒪(F) · π^{-1}_*(M, 1) = π^* M read at
the stalk (stalkIdeal_mul).
The pull-back along π of the defect f^* s − g^* s lies in the stalk of π^* M at every
point over V(M): germ_app_sub_germ_app_mem_stalkIdeal transported by stalkIdeal_comap.
The exceptional ideal on a chart is principal, generated by the chart function #
On the chart of c, the exceptional ideal π_X^* C is generated by π_X^* c.
The generator pulled back along a morphism into the blow-up #
Along any morphism φ into the blow-up, at a point mapped into the chart of c, the stalk of
φ^* π_X^* C is generated by the pull-back of π_X^* c.
The chart of c lies over V (chart_image_top_le, in the form of a bound on the preimage).
The stalk of Spec A at q receives A through the germ of global sections #
The ring map A → 𝒪_{Spec A, q}, a ↦ germ_q (a), spelled through the germ of global sections
(the same map as StructureSheaf.toStalk, in the spelling of the stalk of the scheme Spec A).
A duplicate of AlgebraicGeometry.specGerm
(Hironaka/Scheme/BlowUp/AffineBlowUp/Universal/Membership.lean), kept under a local name so that
every stalk identity of this file is spelled through it.
Equations
Instances For
chartGerm is the germ of the global section (the specGerm_apply of
AlgebraicGeometry.specGerm).
a is a unit at q ∈ Spec A iff a ∉ q: Mathlib's IsLocalization.AtPrime.isUnit_to_map_iff
on the stalk.
The chart generator c ∈ A[C(V)/c] is a nonzerodivisor at every point of the chart.
The exceptional ideal pulled back to the chart of c is generated at every point by c
(comap_exceptionalDivisor_chart).
The germ of π_X^* s at a point of the chart of c', read on the chart, is the image of
algebraMap s (appLE_chart_comp_π).
If the exceptional ideal at a point p of the chart of c' is generated by π_X^* c, then on
the chart it is generated by the image of algebraMap c.
Generators of the chart algebra as a ring #
The chart algebra R[I/a] is generated as a ring by the image of R and the ratios b / a,
b ∈ I.
Kollár's y_j x_r = x_j: the ratio identity (b / c) · c = b in the chart algebra
(awayFrac_mul_algebraMap_pow).
The ratio identity transported to the sections of the chart of a in the blow-up: with θ z := (chart.appIso ⊤).inv ((ΓSpecIso _).inv z), θ (b / a) · θ a = θ b.
The converse: a point where the chart function generates lies in the chart #
A point of the blow-up over V at which the exceptional ideal is generated by π_X^* c lies
in the chart of c: on whichever chart c' contains it, the ratio c / c' is a unit there, and
the chart of c meets the chart of c' in the basic open of that ratio.
appLE respects an equality of morphisms.
The germ of a section pulled back along π ≫ f is the composite of the stalk maps applied to
the germ (appLE_comp_appLE, germ_appLE_apply, germ_stalkMap_apply).
Equality of two morphisms into an affine chart on an affine piece of V(N) #
Two morphisms φ, φ' that map an affine open W into the affine chart ch : Spec A ⟶ Y agree
on V(N) ∩ W as soon as the defects of a set of ring generators of A lie in N(W): the
restrictions to V(N) ∩ W factor through the chart, and morphisms into an affine scheme are
determined by their maps on global sections.
The exceptional ideal as the pull-back of the target's exceptional ideal along a lift #
For a lift φ : B_J U ⟶ B_C X over f₀ with f₀^* C = J, the pull-back of the exceptional
ideal of B_C X is the exceptional ideal of B_J U.
The chart function pulled back along a lift, at the stalk #
Along a lift φ over f₀, the germ of π_X^* s on the chart pulls back to the germ of
π^* f₀^* s.
The exceptional ideal at a point of a chart preimage is generated by the chart function #
At a point w of B_J U whose image under the lift lies in the chart of c, the exceptional
ideal of B_J U is generated by π^* f₀^* c.
The transported second lift over the projection #
The second lift, transported to B_{f^{-1} C} U along f^{-1} C = g^{-1} C, lies over g.
The sections of the chart generators pulled back along a lift #
An open of B_J U mapped into the chart of c by a lift over f₀ lies over V.
Kollár's "this is clear if y_j = x_j": the pull-back along a lift of the chart section
θ (algebraMap r) is the section π^* f₀^* r (appLE_chart_eq, appLE_comp_appLE).
Kollár's ψ^*_{i+1}(y_j) · ψ^*_{i+1}(x_r) = ψ^*_{i+1}(x_j): the pull-back along a lift of the
chart section θ (b / c) times π^* f₀^* c is π^* f₀^* b.
The local step: an affine neighbourhood of a point of V(M') on which the lifts agree #
The local step of the descent: every point u of V(M'), M' = π^{-1}_*(M, 1), has an affine
neighbourhood W such that the two lifts f', g' agree on V(M') ∩ W. This is steps 1–5 of the
proof described in the module docstring.
The descent #
One-step descent of agreement through a blow-up. For morphisms f, g : U ⟶ X, a centre
C ⊆ X with f^{-1} C = g^{-1} C, and an ideal sheaf M ≤ f^{-1} C on which f and g agree,
the lifts f̃, g̃ : B_{f^{-1} C} U ⟶ B_C X (the second transported along f^{-1} C = g^{-1} C)
agree on V(π^{-1}_*(M, 1)). The inductive step of the proof of [Kol07, Theorem 97]; equality of
morphisms is local on the source, and exists_affineOpens_eq_comp gives it locally.
The step assembled #
The three assertions of the induction in the proof of [Kol07, Theorem 97] at stage i + 1:
with flat ψ, ψ', equal pulled-back centres, centres in the images and M ≤ ψ^{-1} Z on which
ψ, ψ' agree, the centres are equal (assertion (3)) and, Z' substituted by Z (assertion (1)),
the lifts agree on V(π^{-1}_*(M, 1)) (assertion (2), agreeOn_blowUpMap), the second lift
transported along the equality of the pulled-back centres.