The componentwise blow-up lemma #
A disjoint union of smooth centers blown up component by component, in a fixed order, gives a
sequence with the same composite as the single blow-up ([Kol07, Remark 33]). The mathematics is
the composition of blow-ups [TSPA, Tag 080A] iterated: the blow-up of X' = B_{D 0} X along the
inverse image of D 1 followed by π_{D 0} is a blow-up of X along D 0 · D 1
(IsBlowUp.comp), and blow-ups of the same center are canonically isomorphic over X
(IsBlowUp.exists_iso; the
uniqueness of [Hau14, Remark 4.5]). So the composite of ofCenters c D is a blow-up along
∏ i, D i for any list of centers; disjointness enters only when the product is identified with
the center Z one started from: a regular closed subscheme V(Z) is the product of its
irreducible components (componentFamily), because its stalks are domains (regular local rings),
so that Z_x is prime, has one minimal prime, and one component passes through x (the
correspondence of Hironaka/Resolution/Algebraic/Snc/DictionaryComponents.lean between minimal
primes of Z_x and components through x), while the components not through x have unit stalk
there.
Main declarations #
AlgebraicGeometry.Scheme.BlowUpSequence.isInvertible_comap_stageMap: an invertible ideal sheaf pulls back along everyΠ_iof a blow-up sequence to an invertible one.AlgebraicGeometry.Scheme.BlowUpSequence.center_ofCenters,composite_ofCenters_succ: the recursion ofofCenterson centers and composites.isBlowUp_composite_ofCenters,exists_iso_last_ofCenters(any list of centers).eq_of_mem_support_componentFamily,pairwise_disjoint_support_componentFamily,prod_componentFamily_eq(the components of a regular closed subscheme).isBlowUp_composite_componentwiseSeq,exists_iso_last_componentwiseSeq,exceptionalDivisor_comap_eq_prod_componentwiseSeq,pairwise_disjoint_support_exceptionalAt_componentwiseSeq(the same forcomponentwiseSeq).
An invertible ideal sheaf on X pulls back along every partial composite Π_i : X_i ⟶ X of a
blow-up sequence to an invertible ideal sheaf (the pull-back of an invertible ideal along a
blow-up is invertible, [TSPA, Tag 0809], iterated).
The composite of ofCenters (c + 1) D is the composite of the tail followed by π_{D 0}.
The i-th center of ofCenters c D is the inverse image of D i under the composite Π_i
of the earlier blow-ups (the preimage Z_k' of Z_k in the intermediate scheme).
The composite of the componentwise sequence is a blow-up along the product #
The composite of the componentwise sequence of the centers D 0, …, D (c-1) is a blow-up of
X along their product ∏ i, D i, in the sense of the universal property [Hau14, Definition 4.4]:
induction on c with the composition of blow-ups [TSPA, Tag 080A] (IsBlowUp.comp) at each step;
the admissibility clause of the step is the invertibility of the exceptional divisor of π_{D 0}
pulled back along the composite of the later blow-ups (isInvertible_comap_stageMap).
The end result of the componentwise sequence is isomorphic over X to the blow-up along the
product, by a unique morphism over X (IsBlowUp.exists_iso; [Hau14, Remark 4.5]).
The k-th exceptional divisor of the componentwise sequence, pulled up to the end result along
Kollár's Π_{c,k+1} [Kol07, Definition 29], is the inverse image of the k-th center under the
composite Π_c.
The irreducible components of a regular closed subscheme #
At a point of a regular closed subscheme V(Z) the stalk ideal Z_x is prime:
𝒪_{X,x}/Z_x ≅ 𝒪_{V(Z),z} (stalkQuotientEquiv) is a regular local ring, hence a domain.
A point x of a regular closed subscheme V(Z) lies on exactly one irreducible component: two
generic points of V(Z) specializing to x both give the unique minimal prime Z_x of the prime
Z_x (stalkIdeal_vanishingIdeal_mem_minimalPrimes,
eq_of_stalkIdeal_vanishingIdeal_closure_eq).
The support of a member of the component family is the closure of its generic point.
Two members of the component family of a regular closed subscheme with a common point coincide.
The irreducible components of a regular closed subscheme V(Z) are pairwise disjoint.
A regular closed subscheme is the product of its irreducible components (Z = ∐ Z_k), stalk
by stalk: at x ∈ V(Z) the unique component through x has stalk Z_x (the unique minimal prime
of the prime Z_x) and the others have unit stalk; off V(Z) every stalk is the unit ideal.
At a point of an irreducible component of a regular closed subscheme V(Z), the stalk of the
component is the stalk of Z, the unique minimal prime of the prime Z_x.
The closed subscheme of a member of the component family is an irreducible space: its underlying space is the closure of the generic point.
The irreducible components of a regular closed subscheme are regular: their stalks are the
stalks of V(Z) (stalkIdeal_componentFamily_eq).
The componentwise sequence of a regular center #
The composite of the componentwise sequence of a regular center Z is a blow-up of X along
Z: the blow-up π_Z factors as π_{Z_1} ∘ π_{Z_2'} ∘ ⋯ ∘ π_{Z_c'}.
The end result of the componentwise sequence of a regular center is canonically isomorphic to
B_Z X, over X.
The exceptional divisor of π_Z is the disjoint union of the exceptional divisors of the
componentwise blow-ups, the union: under any morphism e over X from the end result of the
componentwise sequence to B_Z X, the exceptional divisor of π_Z pulls back to the product of
the exceptional divisors of the componentwise blow-ups pulled up to the end result.
The exceptional divisor of π_Z is the disjoint union of the exceptional divisors of the
componentwise blow-ups, the disjointness: the exceptional divisors of the componentwise blow-ups,
pulled up to the end result, have pairwise disjoint supports, as they lie over the pairwise
disjoint components.