Blow-up sequences: stages, composites, smoothness, and the deletion of empty blow-ups #

A blow-up sequence on a scheme X in the sense of [Kol07, Definition 29] is a chain X_r → X_{r-1} → ⋯ → X_1 → X_0 = X of blow-ups π_i : X_{i+1} → X_i with centers Z_i ⊆ X_i and exceptional divisors F_{i+1} ⊆ X_{i+1}. In this library it is a term of the inductive family AlgebraicGeometry.Scheme.BlowUpSequence X: nil X, and cons X D rest with rest : BlowUpSequence (D.blowUp). Everything Kollár attaches to a sequence is a recursive function of that list of centers: the stages X_i, the centers Z_i, the composites Π_i, the deletion of empty blow-ups, and the notions this module defines — the blow-up maps π_i (step), the composites Π_{ij} = π_j ∘ ⋯ ∘ π_{i-1} (stageMapBetween), the exceptional divisors F_{i+1} (exceptionalAt), the predicates "smooth" (IsSmooth, IsSmoothOfRelativeDimension), "trivial" (IsTrivialAt) and "empty" (IsEmptyAt, NoEmptyCenters), and the marked transforms (I_i, m) along the sequence (markedTransformSeq). This module proves the basic identities about them.

The recursion. Every proof here is an induction on the sequence and, on the shape cons X D rest, a case split on the index: index 0 speaks about the first blow-up, X_0 = X, Z_0 = D, π_0 = D.blowUpπ, F_1 = D.comap π_0; index j + 1 speaks about the tail rest, a sequence on D.blowUp, to which the induction hypothesis applies with the structure morphism D.blowUpπ ≫ f in place of f. Two features of the inductive definition drive the bookkeeping. First, S.stage 0 is X only after S is split into nil or cons (stage_zero); so the equalities Π_0 = 𝟙 and Π_{i0} = Π_i are proved on the constructor shapes, and π_0 on the cons shape carries the cast eqToHom (stage_zero rest) (step_cons_zero). Second, the composite Π_{i+1} = Π_i ∘ π_i (stageMap_succ) and the cocycle Π_{jl} ∘ Π_{ij} = Π_{il} (stageMapBetween_comp) are the associativity of composition threaded through the recursion. The inductions are run with the indices in the form ⟨j, h⟩, where the recursive definitions unfold; the Fin.succ/Fin.castSucc forms of the statements are recovered at the end by definitional unfolding.

Smoothness ([Kol07, Notation 19 and Definition 29]). A sequence is smooth when each center Z_i ⊆ X_i is smooth over k (IsSmooth). In the equidimensional form (IsSmoothOfRelativeDimension: X of pure relative dimension n, each Z_i of pure codimension r_i ≤ n) the stages are smooth of relative dimension n, because the blow-up of a smooth center of pure codimension is (AlgebraicGeometry.smoothOfRelativeDimension_blowUpπ_comp), and the exceptional divisors are smooth of relative dimension n − 1, because the exceptional divisor of such a blow-up is (AlgebraicGeometry.smoothOfRelativeDimension_exceptional), by induction along the sequence.

Trivial and empty blow-ups ([Kol07, Warning 20 and 32]). A trivial blow-up has an invertible center and its π_i is an isomorphism (AlgebraicGeometry.Scheme.IdealSheafData.blowUp.isIso_π_of_isInvertible); the empty blow-up, center ⊤, is trivial with exceptional divisor ⊤.comap π_i = ⊤, and under the isomorphism the exceptional divisor of a trivial blow-up is the center (Warning 20 (2): comap_inv_step_exceptionalAt). eraseEmpty deletes the empty blow-ups by carrying each tail back along the inverse of its empty blow-up through pullback; pulling back along an isomorphism neither creates nor removes empty centers (noEmptyCenters_pullback_iff, from the pullback square of blow-up maps AlgebraicGeometry.isPullback_blowUpMap and comap_eq_top_iff_of_isIso), which gives noEmptyCenters_eraseEmpty, eraseEmpty_eq_self_iff, idempotence, and the length count r' + #{i : Z_i = ∅} = r (length_eraseEmpty_add_card).

length_pullback (pulling back does not change the length) is proved here because that count needs it; the theory of the pullback is in Hironaka/Scheme/BlowUpSequence/Pullback.lean.

Blow-up sequences: stages, composites, smoothness, and the deletion of empty blow-ups #

The blow-up maps, predicates and marked transforms of a sequence #

The stages and composites of Definition 29 #

Smooth blow-up sequences #

Trivial and empty blow-ups #

The exceptional divisor of a trivial blow-up is its center #

Pullback along an isomorphism #

Deleting the empty blow-ups #

A sequence is more than its end result #

The composite along an equality of sequences #