Proposition 37: the extension of a blow-up sequence functor from affine schemes #
Kollár's Proposition 37 [Kol07, Proposition 37]: a blow-up sequence functor B defined on affine
schemes over k and commuting with smooth surjections has a unique extension B̄ to all schemes
of finite type over k (here, to all triples), commuting with smooth surjections. This module
defines the extension OrderSeqAssignment.extendFromAffine, proves its specification, and proves
Proposition 37 as stated (existence, OrderSeqAssignment.exists_extension; uniqueness,
OrderSeqAssignment.extension_unique), with the versions for marked triples. The proof of
[Kol07, Theorem 36] uses it to pass from the resolution of affine schemes to that of all schemes.
- The extension (
extendSeq,extendFromAffine): on a tripleT,B̄(T)is the sequence onXdescended fromB(X', g^* I, g^{-1} E)along the affine coverg : X' = ∐ Uᵢ → XofHironaka/Resolution/Algebraic/Kol07/Prop37/Prop37Setting.lean:Triple.exists_isOrderSeq_pullback_coverDesc_eq(Hironaka/Resolution/Algebraic/Kol07/Prop37/Prop37Local.lean) applied to the descent datumτ₁^* B(X') = τ₂^* B(X')(OrderSeqFunctor.pullback_coverFst_eq_pullback_coverSnd), the witness chosen; it is a smooth blow-up sequence of ordermfor(X, I, E)by the descent, and has no empty centers because its pullbackB(X')has none (NoEmptyCenters.of_pullback). Its defining property isg^* B̄(X) = B(X')(extendFromAffine_pullback_coverDesc). - Restriction to the affine triples (
extendFromAffine_restrict): forXaffine,gitself is a smooth surjection between affine triples, soB(X') = g^* B(X)by the hypothesis onB, andg^*is injective (pullback_coverDesc_injective):B̄(X) = B(X). - Commutation with smooth surjections (
extendFromAffine_commutesWithSmoothSurjections): for a smooth surjectionh : Y → Xbetween triples withYcarrying the pullback data, compare on the fibre product of the two affine covers,P := X' ×_X Y'(comparisonScheme), affine sinceg : X' → Xis an affine morphism andY'is affine, whose projectionsq : P → X',p : P → Y'are smooth surjections between affine triples carrying the pullback data of both cover triples (comparisonTriple,comparisonTriple_isPullbackOf_fst/_snd): the hypothesis onBgivesp^* B(Y') = B(P) = q^* B(X'), andq^* B(X') = q^* g^* B̄(X) = p^* (g_Y ≫ h)^* B̄(X), soB(Y') = (g_Y ≫ h)^* B̄(X)by injectivity along the surjectivep, and thenB̄(Y) = h^* B̄(X)by injectivity alongg_Y. This replaces Kollár's refinement of the cover ofYby the fibre product, which needs no refinement. - Uniqueness (
extension_unique): two extensions commuting with smooth surjections agree after pullback alongg(both equalB(X')), hence agree.
The fibre product of the two affine covers over a smooth surjection #
g : X' → X is an affine morphism: X' and Spec k are affine and X → Spec k is separated
(the argument for the affineness of the kernel pair).
The composite Y' → Y → X of the affine cover of Y with a surjection is surjective.
q : P → X' is surjective (base change of the surjective g_Y ≫ h).
P is a scheme over k through p : P → Y'.
Equations
- One or more equations did not get rendered due to their size.
P is smooth over k of the relative dimension of Y.
The triple of P is affine.
The triple of P carries the pullback data of the triple of Y' along p.
The triple of P carries the pullback data of the triple of X' along q as well, when Y
carries the pullback data of X along h: (g_Y ≫ h ≫ p)^* I = (g ≫ q)^* I.
The extension: the sequence descended from B(X') along g #
The value of the extension of [Kol07, Proposition 37] on a triple T: the blow-up sequence on
X descended along g : X' → X from B(X', g^* I, g^{-1} E)
(exists_isOrderSeq_pullback_coverDesc_eq at the descent datum
pullback_coverFst_eq_pullback_coverSnd), the witness chosen.
Equations
- B.extendSeq hB T = Classical.choose ⋯
Instances For
The descended sequence is a smooth blow-up sequence of order m for (X, I, E).
The defining property of the extension: g^* B̄(X) = B(X').
The empty blow-up convention [Kol07, 32] for the extension: B̄(X) has no empty centers,
because B(X') has none.
The extension B̄ of [Kol07, Proposition 37] of B to all triples: B̄(X, I, E) is the
sequence descended from B(X', g^* I, g^{-1} E) along the affine cover g.
Equations
- B.extendFromAffine hB = { seq := fun (T : AlgebraicGeometry.Triple k) (x : True) => B.extendSeq hB T, isOrderSeq := ⋯, noEmptyCenters := ⋯ }
Instances For
The specification of the extension: g^* B̄(X) = B(X') ("B(X') descends to a blow-up
sequence of X", the proof of [Kol07, Proposition 37]).
On the affine triples B̄ is B (it is an extension, [Kol07, Proposition 37]): g : X' → X
is a smooth surjection between affine triples, so B(X') = g^* B(X), and g^* is injective.
The extension "commutes with smooth surjections" [Kol07, Proposition 37]: for a smooth
surjection h : Y → X between triples, Y carrying the pullback data of X, B̄(Y) = h^* B̄(X);
compared on the fibre product P = X' ×_X Y' of the two affine covers, where
p^* B(Y') = B(P) = q^* B(X') = q^* g^* B̄(X) = p^* (g_Y ≫ h)^* B̄(X), then injectivity along the
surjective smooth p and along g_Y.
The existence statement of [Kol07, Proposition 37]: a blow-up sequence functor of order m on
the affine triples commuting with smooth surjections extends to a blow-up sequence functor of
order m on all triples that commutes with smooth surjections (the extension
extendFromAffine).
The uniqueness statement of [Kol07, Proposition 37]: two blow-up sequence functors on all
triples that restrict to B on the affine triples and commute with smooth surjections are equal;
g^* B₁(X) = B(X') = g^* B₂(X), and pullback along the surjective g is injective.
The marked version #
The marked triple of P = X' ×_X Y': the pullback of the marked triple of Y' along p.
Equations
Instances For
The marked triple of P is affine.
The marked triple of P carries the pullback data of the marked triple of Y' along p.
The marked triple of P carries the pullback data of the marked triple of X' along q.
The value of the extension on a marked triple.
Equations
- B.extendSeq hB T = Classical.choose ⋯
Instances For
The extension of [Kol07, Proposition 37] for marked functors.
Equations
- B.extendFromAffine hB = { seq := fun (T : Hironaka.MarkedTriple k) (x : True) => B.extendSeq hB T, isOrderGeSeq := ⋯, noEmptyCenters := ⋯ }
Instances For
The specification of the marked extension: g^* B̄(X) = B(X').
On the affine marked triples B̄ is B.
The marked extension commutes with smooth surjections (the fibre-product comparison).
The existence statement of [Kol07, Proposition 37] for marked functors.
The uniqueness statement of [Kol07, Proposition 37] for marked functors.