The proof of Theorem 105: the descent along a coproduct of open immersions and the extension #
The second half of the proof of Kollár's globalization theorem [Kol07, Theorem 105]: for the
class of open immersions, Proposition 37 showed that the first centers Z₀' ∩ Uₓᵢ glue to a
center Z₀ ⊂ X, and one can "repeat the above argument" to obtain the whole blow-up sequence for
(X, I, E); the conclusion is that B extends uniquely to a blow-up sequence functor B̄ on
GT commuting with the surjections in M. This module proves it for
the class openImmersionCoprods of coproducts of open immersions. The first half (the local
cover, the kernel pair, uniqueness) is Hironaka/Resolution/Algebraic/Kol07/Globalize.lean; the
global case of the proof of Theorem 103 [Kol07, 104, Step 3] is the instance of this module for the
maximal contact classes of Hironaka/Resolution/Algebraic/Kol07/MaximalContactGlobalization.lean.
The descent #
Let g : X' → X be a surjective coproduct of open immersions, ιᵢ : Uᵢ → X' its summands, and
S' a blow-up sequence on X' whose two pullbacks to the kernel pair X'' = X' ×_X X' agree.
The summand inclusions composed with g are open immersions ιᵢ ≫ g : Uᵢ → X covering X, and
the restrictions S'|_{Uᵢ} agree on the overlaps Uᵢ ×_X Uⱼ: the overlap maps into X'' (by
the universal property of the kernel pair, with the two projections restricting to the
projections of the overlap), and the agreement on X'' restricts. This is exactly the descent
datum of the proof of Proposition 37 (AgreeOnOverlaps,
Hironaka/Resolution/Algebraic/Kol07/Prop37/Prop37Descent.lean), so
exists_pullback_eq_of_agreeOnOverlaps descends the family to a sequence S₀ on X with S₀|_{Uᵢ} = S'|_{Uᵢ}; then g^* S₀ = S' because two sequences on X' agreeing on a nonempty covering family
of open immersions are equal (eq_of_pullback_of_covers). When X' is empty, g is an isomorphism
of empty schemes and S' pulled back along its inverse descends. The order condition and the empty
blow-up convention descend along g: the condition of [Kol07, Definition 66] is local on a covering
family of open immersions (isOrderSeq_of_covers of
Hironaka/Resolution/Algebraic/Kol07/Prop37/Prop37Local.lean, fed the restrictions of S', which
are order sequences by pullback along the open immersions ιᵢ), and a sequence whose pullback has
no empty centers has none (NoEmptyCenters.of_pullback).
The extension #
Two local covers g₁ : T₁ → T, g₂ : T₂ → T of a global triple have a fibre product W that is
a local triple (the hypothesis LocalCoversFibreClosed) with surjective projections in M, and
B commutes with both, so p₁^* B(T₁) = B(W) = p₂^* B(T₂) (pullback_eq_of_localCovers; the
kernel pair is the case T₁ = T₂). Hence the sequence S descended from one local cover
g₀ : T₀ → T satisfies g^* S = B(T') for every local cover g : T' → T: on W = T' ×_T T₀,
p₁^* g^* S = p₂^* g₀^* S = p₂^* B(T₀) = p₁^* B(T'), and pullback along the surjective flat p₁
is injective. This is exists_globalizeSeq; globalize chooses such an S for every nonempty
global triple and takes nil on the empty ones (where every sequence without empty centers is
nil). Its characterising lemma globalize_seq_pullback gives agreement with B on LT ∩ GT
through the identity cover, and commutation with a surjection h : Y → X in M through the
fibre product of the composite cover Y' → Y → X with a cover X' → X, comparing both sides
after pullback along the surjective flat W → Y' → Y.
Descent of a sequence along a surjective coproduct of open immersions #
A sequence on the source of a surjective coproduct of open immersions whose pullbacks to the
kernel pair agree descends to the target (the proof of [Kol07, Theorem 105], "we can repeat the
above argument … and eventually get the whole blow-up sequence"): the descent of Proposition 37
on the summand family, then locality on X'.
The descended sequence is a smooth blow-up sequence of order m #
The descended sequence is a smooth blow-up sequence of order m for T (the condition of
[Kol07, Definition 66] is local on the summand family, isOrderSeq_of_covers, the restrictions
of S' being order sequences by pullback along the open immersions ιᵢ) with no empty centers
(NoEmptyCenters.of_pullback).
The fibre product of two local covers #
The fibre product of two local M-covers of a global triple, as a local triple (the
hypothesis LocalCoversFibreClosed) whose projections are surjective members of M and along
both of which it carries the pullback data; exists_kernelPair is the case T₁ = T₂.
The extension B̄ #
Two local M-covers of a global triple give the same sequence on their fibre product:
p₁^* B(T₁) = B(W) = p₂^* B(T₂) (the compatibility (105.4) of [Kol07, Theorem 105] for two
covers).
The sequence descended along one local cover of a nonempty global triple pulls back to B
along every local cover (compared on the fibre product of the two covers, pullback along the
surjective flat projection being injective), and is a smooth blow-up sequence of order m
without empty centers.
The sequence B̄(T): on a nonempty global triple a sequence of exists_globalizeSeq, on an
empty one nil.
Equations
- Hironaka.OrderSeqAssignment.globalizeSeq D hF B hB T hG = if hne : Nonempty ↥T.X.left then Classical.choose ⋯ else AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left
Instances For
The extension B̄ of B to the global triples [Kol07, Theorem 105]: on a nonempty T, a
sequence descended from B along a local cover (exists_globalizeSeq); on an empty T.X.left,
nil.
Equations
- Hironaka.OrderSeqAssignment.globalize D hF B hB = { seq := Hironaka.OrderSeqAssignment.globalizeSeq D ⋯ B hB, isOrderSeq := ⋯, noEmptyCenters := ⋯ }
Instances For
The characterising property of B̄: along every local M-cover g : T' → T,
g^* B̄(T) = B(T').
B̄ agrees with B on the local triples that are global (the identity is a local cover).
B̄ commutes with the surjections in M [Kol07, Theorem 105]: for a surjection h : Y → X
in M with the pullback data, both B̄(Y) and h^* B̄(X) pull back to B(W) on the fibre
product W of the composite cover Y' → Y → X with a cover X' → X, and pullback along the
surjective flat W → Y' → Y is injective.
The existence statement of [Kol07, Theorem 105]: B̄ := globalize extends B and commutes
with the surjections in M.