Descent of blow-up sequences along an open cover: the recursion of the proof of Proposition 37 #
The proof of [Kol07, Proposition 37] descends the blow-up sequence B(X') on the disjoint union
X' = ∐ᵢ Uᵢ of a finite affine open cover (coverScheme of
Hironaka/Resolution/Algebraic/Kol07/Prop37/Prop37Setting.lean, with g = coverDesc : X' → X and
the two projections τ₁, τ₂ : X'' = X' ×_X X' → X') to a blow-up sequence on X. This module
proves the parts of the argument that concern sequences as such, without the order condition of
[Kol07, Definition 66], which Hironaka/Resolution/Algebraic/Kol07/Prop37/Prop37Local.lean adds
stage by stage.
- The compatibility (37.1). Since
Bcommutes with the smooth surjectionsτᵢ, andX''carries the pullback data ofX'along both (coverPairTriple_isPullbackOf_fst/_snd),τ₁^* B(X') = B(X'') = τ₂^* B(X')as whole sequences (OrderSeqAssignment.pullback_coverFst_eq_pullback_coverSnd); for the first center this isτ₁^*(Z₀') = τ₂^*(Z₀'), read off byconsinjectivity (center_zero_comap_eq). - (37.1) is (37.2) on the pieces. The kernel pair
X' ×_X X'is covered by the open piecesUᵢ ×_X Uⱼ(Mathlib'sScheme.Pullback.openCoverOfLeftRightof the twoSigma.ιcovers), the pieceUᵢ ×_X Uⱼ → X' ×_X X'beingpullback.mapalong the two inclusions (Triple.piecePairMap). An ideal sheaf onX''is determined by its restrictions to the pieces (ext_of_openCover), and so is a blow-up sequence (eq_of_pullback_of_covers, on a nonempty index type; for the empty coverX''is empty andτ₁ = τ₂outright). Henceτ₁^* D = τ₂^* DiffD|_{Uᵢ}andD|_{Uⱼ}agree on everyUᵢ ×_X Uⱼ(Triple.comap_coverFst_eq_comap_coverSnd_iff), andτ₁^* S = τ₂^* Siff the restrictionsS|_{Uᵢ}agree on the overlaps (Triple.pullback_coverFst_eq_pullback_coverSnd_iff; the predicateBlowUpSequence.AgreeOnOverlaps). - Gluing the first center. Compatible ideal sheaves on the members of an open cover glue
(
IdealSheafData.glue,glue_comap): the gluedZ₀satisfiesg^* Z₀ = Z₀', checked piece by piece (Triple.exists_comap_coverDesc_eq);g^*is injective because the pieces coverX(Triple.comap_coverDesc_injective). - The recursion. "We can repeat the above argument … and eventually get the whole blow-up
sequence for
X", in the form of a family: a family of blow-up sequencesS ion a covering family of open immersionsι i : W i → Xagreeing on the overlaps is the family of pullbacks of one sequenceS₀onX(exists_pullback_eq_of_agreeOnOverlaps). The proof is an induction on the common length: the first centersD iagree on the overlaps (consinjectivity) and glue toZ₀withZ₀|_{W i} = D i; the tails, transported toblowUp (W i) (Z₀|_{W i})along that equality (cons_eq_cons_pullback_eqToHom), form a family on the lifted covering familyblowUpMap (ι i) Z₀ : blowUp (W i) (Z₀|_{W i}) → Z₀.blowUp(open immersions; covering, by the cartesian square of the blow-up maps), and they agree on the lifted overlaps because the overlap of two lifted pieces is the blow-up of the overlap of the pieces (isPullback_blowUpMap_of_isPullback, the base-change squares pasted), so that the hypothesis on the tails transports along the identification (pullback_injective_of_isIso,pullback_eqToHom_heq). The induction hypothesis descends the tails toS₁onZ₀.blowUp, andS₀ := cons X Z₀ S₁. Kollár's form on the affine cover (Triple.exists_pullback_coverDesc_eq) is the family form for the piecesUᵢcomposed with the previous item, the descended sequence pulling back to the given one onX'by locality on the coverSigma.ι; whenXis empty (X'too, no pieces),gis a morphism between initial objects and the descent is the pullback along its inverse. Uniqueness is the injectivity of pullback along a surjective flat morphism (Triple.pullback_coverDesc_injective; "ifhis surjective thenh^* BdeterminesBuniquely", [Kol07, 30.1]). - No empty blow-ups. The centers of
g^* Sare the inverse images of the centers ofSunder the stage lifts (center_pullback) andcomap ⊤ = ⊤along any morphism, so an empty center ofSwould be an empty center ofg^* S(NoEmptyCenters.of_pullback).
Transport lemmas for the recursion #
Pulling a sequence back along an eqToHom is a transport of its base: heterogeneously it is
the sequence itself.
Pullback along an isomorphism is injective on sequences: the inverse pulls back to the
inverse (pullback_comp, pullback_id).
A sequence of length 0 is the empty sequence.
A sequence of length n + 1 is a cons with a tail of length n.
The transported tail of cons_inj is heterogeneously equal to the tail.
Rewriting the center of a cons along an equality of ideal sheaves: the tail is transported
by pullback along the eqToHom of the blow-ups.
The first center of (37.1) #
Equal pullbacks of a cons along τ₁, τ₂ have equal inverse images of the first center (the
compatibility (37.1) of the proof of [Kol07, Proposition 37]): cons injectivity.
No empty blow-ups #
A sequence whose pullback along g has no empty centers has none (the empty blow-up
convention of [Kol07, 32] descends): the center of the pullback at stage i is the inverse image
of the center of S under the stage lift, and the inverse image of ⊤ is ⊤.
The descent recursion, for sequences #
The open cover of X by a covering family of open immersions ι i : W i ⟶ X (Mathlib's
Cover.mkOfCovers); a named definition so that the gluing of ideal sheaves can be applied to a
family without unfolding the cover's fields.
Equations
- Hironaka.Sequence.familyCover ι hcov = AlgebraicGeometry.Scheme.Cover.mkOfCovers σ W ι hcov ⋯
Instances For
Gluing of ideal sheaves for a covering family of open immersions: ideal sheaves on the
members agreeing on the pairwise fibre products glue to an ideal sheaf on X restricting to
them.
The lifted covering family: the blowUpMap (ι i) Z₀ : blowUp (W i) (Z₀|_{W i}) → Z₀.blowUp
cover the blow-up when the ι i cover X; a point over the range of ι i comes from
blowUp (W i) (Z₀|_{W i}) (exists_blowUpMap_eq, the cartesian square of the blow-up maps).
The tails of two cons sequences with restricted first centres, agreeing on the overlap
W i ×_X W j, agree after pullback to the blow-up of the overlap along the restricted centre — the
tail of the hypothesis (cons_inj), transported along the equality of the two restrictions of
the centre to the overlap (heq_of_transport_eq, pullback_eqToHom_heq).
The tails of a family of cons sequences with a common (restricted) first center agreeing on
the overlaps agree on the lifted overlaps: the overlap of two lifted pieces is the blow-up of the
overlap of the pieces (isPullback_blowUpMap_of_isPullback, the base-change squares pasted),
along which identification (pullback_injective_of_isIso) the hypothesis on the tails transports
(pullback_blowUpMap_fst_eq_of_agree).
The recursion of the proof of [Kol07, Proposition 37] on the common length n of the family:
a family of sequences on a covering family of open immersions, agreeing on the overlaps, is the
family of pullbacks of one sequence.
"We can repeat the above argument … and eventually get the whole blow-up sequence for X"
(the proof of [Kol07, Proposition 37]): a family of blow-up sequences on a covering family of open
immersions agreeing on the overlaps is the family of pullbacks of one blow-up sequence on X.
The members have a common length when the index type is nonempty (length_pullback on the
overlaps); when it is empty the conclusion is vacuous.
The descent datum (37.1) for whole sequences #
"Since B commutes with the τᵢ" (the proof of [Kol07, Proposition 37]): for a functor on
the affine class commuting with smooth surjections, τ₁^* B(X') = B(X'') = τ₂^* B(X'), because
X'' carries the pullback data of X' along both projections
(coverPairTriple_isPullbackOf_fst/_snd) and both are smooth surjections.
The descent datum (37.1) for marked functors.
The kernel pair and its pieces #
The piece Uᵢ ×_X Uⱼ of the kernel pair X' ×_X X' (Kollár's X'' = ∐_{i ≤ j} Uᵢ ∩ Uⱼ in the
proof of [Kol07, Proposition 37]): the map induced by the two inclusions Uᵢ, Uⱼ → X'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The piece map followed by τ₁ is the first projection of the piece followed by the inclusion
of Uᵢ.
The piece map followed by τ₂ is the second projection of the piece followed by the inclusion
of Uⱼ.
The open cover of the kernel pair X' ×_X X' by the pieces Uᵢ ×_X Uⱼ (Mathlib's cover of a
fibre product by the fibre products of the members of covers of the two factors), indexed by
pairs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The member (i, j) of the pieces cover, written out: Mathlib's pullback.map along the two
inclusions Uᵢ, Uⱼ → X' over 𝟙 X, from the piece computed with Sigma.ι ≫ g (definitionally
T.coverPairCover.f (i, j); the explicit form keeps the source scheme syntactic for rewriting).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The member (i, j) of the pieces cover is the piece map.
The piece map followed by τ₁: the first projection of the piece followed by the inclusion of
Uᵢ.
The piece map followed by τ₂.
The piece Uᵢ ×_X Uⱼ computed with Sigma.ι ≫ g and the one computed with the member maps
(ι_comp_coverDesc) are identified by pullback.congrHom; the first projections correspond.
The second projections of the two computations of the piece correspond.
The restriction of τ₁^* D to the piece (i, j) is the restriction of D|_{Uᵢ} to
Uᵢ ×_X Uⱼ, transported along the identification of the piece.
The restriction of τ₂^* D to the piece (i, j).
(37.1) is (37.2) for ideal sheaves (the proof of [Kol07, Proposition 37]): for an ideal sheaf
on X' = ∐ Uᵢ, its two pullbacks to X' ×_X X' agree iff, for all i, j, its restrictions to
Uᵢ and Uⱼ agree on Uᵢ ×_X Uⱼ, the pieces covering the kernel pair.
When the affine cover has no members, X' is empty.
When the affine cover has no members, so is the kernel pair.
The pullback of τ₁^* S to the piece (i, j) is the pullback of S|_{Uᵢ} to
Uᵢ ×_X Uⱼ, transported along the identification of the piece.
The pullback of τ₂^* S to the piece (i, j).
(37.1) is (37.2) for sequences: a sequence on X' = ∐ Uᵢ has equal pullbacks along τ₁, τ₂
iff its restrictions to the Uᵢ agree on the overlaps Uᵢ ×_X Uⱼ; the pieces cover the kernel
pair and sequences are determined by their pullbacks to a nonempty covering family
(eq_of_pullback_of_covers); with no pieces, τ₁ = τ₂.
Gluing the first center #
The restriction to the piece Uᵢ of the inverse image along g is the inverse image along
the member map Uᵢ → X.
"The subschemes Z₀ᵢ' ⊂ Uᵢ glue together to a subscheme Z₀ ⊂ X" (the proof of
[Kol07, Proposition 37]): an ideal sheaf on X' with agreeing pullbacks to X'' is the inverse
image of an ideal sheaf on X; the gluing of ideal sheaves along the affine cover, the
compatibility being (37.2); g^* Z₀ = D is checked on the pieces of X'.
The glued ideal sheaf is unique: inverse image along g is injective, the pieces covering
X.
The descent along the affine cover, and uniqueness #
Kollár's form of the descent on the affine cover (the proof of [Kol07, Proposition 37]): a
blow-up sequence on X' with τ₁^* S' = τ₂^* S' descends to X, that is, it is g^* S for a
sequence S on X. The restrictions to the pieces agree on the overlaps
(pullback_coverFst_eq_pullback_coverSnd_iff), the family form of the recursion descends them
to S, and g^* S = S' on the cover Sigma.ι of X' (eq_of_pullback_of_covers). With no
pieces, X and X' are empty, g is a morphism of initial objects, and S is the pullback of
S' along its inverse.
"If h is surjective then h^* B determines B uniquely" [Kol07, 30.1], the uniqueness in
Proposition 37: pullback along the smooth (hence flat) surjection g : X' → X is injective on
sequences (pullback_injective_of_surjective).