Refinement of a blow-up sequence to irreducible centers #
Clause (i) of Hironaka's Main Theorem II [Hir64, Main Theorem II] asks for irreducible centers,
while Kollár's smooth centers [Kol07, Definition 66] may be disconnected. This module shows that a
smooth blow-up sequence of order d refines to one with regular irreducible centers, of length
∑ᵢ rᵢ (rᵢ the number of irreducible components of the i-th center), with the same composite,
the same final weak transform J_r and the same final boundary E_r
(IsOrderSeq.exists_refineIrreducible). The refinement is built stage by stage: the center Z_0
is replaced by its componentwise sequence
(Hironaka/Resolution/Algebraic/Kol07/ComponentwiseBlowUp.lean, ComponentwiseTransforms.lean),
and the refinement of the tail, a sequence on B_{Z_0} X by the induction hypothesis, is carried
across the canonical isomorphism of the end results (pullback along an isomorphism) and
concatenated (Hironaka/Scheme/BlowUpSequence/ConcatApi.lean). The simple normal crossing
conditions are transported through the subdivision relation of
Hironaka/Resolution/Algebraic/Kol07/RefineFamily.lean.
The module also holds the transport lemmas along isomorphisms that the induction uses (the stage
lifts of an isomorphism are isomorphisms, Hironaka's boundaries pull back along isomorphisms), and
the subdivision of the total transforms along a componentwise sequence
(subdivides_totalTransformSeq_ofCenters_last), proved locally on the open sets missing all
components but one and glued as in the proof of [Kol07, Proposition 37].
The stage lifts of an isomorphism along a blow-up sequence are isomorphisms (the cartesian
squares isPullback_pullbackStageHom, isomorphisms being stable under base change).
Hironaka's boundaries pull back along an isomorphism of the base: red(f_i⁻¹(E_i) ∪ f_i⁻¹(D_i))
is a vanishing ideal, and the inverse image of a vanishing ideal along an isomorphism is the
vanishing ideal of the preimage (comap_vanishingIdeal_of_isIso), the squares of blowUpMap
(blowUpMap_π) matching the preimages.
Total transforms along the componentwise sequence #
A componentwise equality of families along an injection of index sets is a subdivision.
((J ∘ ψ) ∘ π : K^∞) = (J ∘ (π ≫ ψ) : K^∞) (comap_comp).
((J : K^∞) ∘ ψ) = ((J ∘ ψ) : (K ∘ ψ)^∞) along a flat ψ (saturate_comap_of_flat with
comap_comp).
The total transform along π of the inverse image of a family along ψ has the components of
the total transform along π ≫ ψ (strictTransformAlong_comap_left); the distinguished divisor
is unchanged. (The proof goes through explicit intermediate terms: the kernel must never compare
two total transforms argumentwise.)
Along a flat ψ the inverse image of a total transform along π with invertible distinguished
divisor K has the components of the total transform along ψ ≫ π with distinguished divisor
K.comap ψ (comap_strictTransformAlong_of_flat).
The total transform under the blow-up of the unit ideal subdivides the inverse image of the
family: the exceptional divisor is the unit ideal and passes through no point, and every strict
transform has the stalk of the inverse image (stalkIdeal_strictTransformAlong_of_notMem_support,
every point lying off the exceptional divisor).
A family subdivides the inverse image, along a section e of a blow-up π of the unit ideal
(an isomorphism), of its total transform along π: the strict transforms come back to the
components (saturate_top) and the exceptional divisor is the unit ideal.
Along a componentwise sequence of unit centers (isomorphisms), the total transform of F at
the end subdivides the inverse image of F under the composite: each step adds a unit exceptional
divisor (subdivides_totalTransform_of_eq_top).
Along a componentwise sequence with a single non-unit center D k₀ (the restriction of the
componentwise sequence of ⊔ Z_k to the open set missing the other components), the total
transform of a family F subdividing G subdivides the inverse image, along the canonical map e
to any blow-up π of ∏ D, of the total transform of G along π. By induction on the length: a
unit center before k₀ is an isomorphism, absorbed into π (IsBlowUp.comp_iso); at k₀ the
canonical map is the composite of the remaining unit blow-ups
(subdivides_totalTransformSeq_ofCenters_last_of_forall_top), by uniqueness of the lift
(IsBlowUp.exists_iso). Stated for a variable sequence S equal to the componentwise sequence and
a variable last index i, so that it applies to pulled-back sequences.
The case of at least one center of subdivides_totalTransformSeq_ofCenters_last, by the cover
argument on the open sets X ∖ ⋃_{l ≠ k} V(D l).
Along the componentwise sequence of pairwise disjoint centers D, the total transform at the
end of a family F subdividing G subdivides the inverse image, under the canonical map e to
any blow-up π of ∏ D, of the total transform of G along π. The relation is local
(subdivides_of_cover), and the sequence pulls back along open immersions as in [Kol07, 30.1]; on
the open set X ∖ ⋃_{l ≠ k} V(D l) only the center D k survives (comap_ι_eq_top_of_disjoint),
the pulled-back sequence is the componentwise sequence of the restricted centers
(pullback_ofCenters), its total transforms are the inverse images of those of X
(totalTransformSeq_pullback), and the blow-up of the restricted center maps to B by the open
immersion blowUpMap followed by the canonical isomorphism, through which the single-center case
subdivides_totalTransformSeq_of_single applies.
Transport along isomorphisms and along equal indices #
The stage map at an index equal to another one, through the equality of the stages.
The composite as the stage map at an index equal to the last one.
The closed subscheme of the inverse image of Z along an isomorphism is irreducible when
V(Z) is (the isomorphism V(Z ∘ e) ≅ V(Z), isIso_subschemeMap_comap_of_isIso).
The closed subscheme of the inverse image of Z along an isomorphism is regular when V(Z)
is: the stalks correspond under the isomorphism V(Z ∘ e) ≅ V(Z)
(IsRegularLocalRing.of_ringEquiv).
boundarySeq_ofCenters_last' for an E₀ equal to the vanishing ideal of its support: the
form in which the reducedness of E₀ enters (radical_eq_self_of_isReduced_subscheme), and the
form Hironaka's boundaries themselves have (reducedTransform is a vanishing ideal).
boundarySeq_componentwiseSeq_last for an E₀ equal to the vanishing ideal of its
support.
The inverse image along a fourfold composite, as nested inverse images (comap_comp).
The refinement #
The refinement to irreducible centers, the induction: a smooth blow-up sequence S of order
d for (X, J, E) [Kol07, Definition 66] refines, for every subdivision F of E, to a sequence
S' of order d for (X, J, F) with regular irreducible centers, of length ∑ᵢ rᵢ, with the
same composite, weak transform and boundaries (for E₀ a vanishing ideal) across an isomorphism
S'.last ≅ S.last. Induction on S: the first center Z is replaced by its componentwise
sequence T (isOrderSeq_componentwiseSeq, exists_iso_last_componentwiseSeq), the tail is
refined by the inductive hypothesis for the subdivision (T.totalTransformSeq F).comap e₁⁻¹ of
E.totalTransform Z (subdivides_totalTransformSeq_ofCenters_last), carried across e₁ by
pullback (IsOrderSeq.pullback), and the two are concatenated (isOrderSeq_concat); the
conditions at the last stage follow from the concatenation, componentwise and pullback transport
lemmas.
Refinement to irreducible centers: a smooth blow-up sequence of order d for (X, J, E)
[Kol07, Definition 66] refines to one with regular irreducible centers, as clause (i) of
[Hir64, Main Theorem II] demands, of length ∑ᵢ rᵢ, with the same composite, the same J_r and
the same E_r (the boundary for every reduced E₀) across the canonical isomorphism of the last
stages. This is exists_refineIrreducible_aux for the trivial subdivision E of itself, a reduced
E₀ being the vanishing ideal of its support (radical_eq_self_of_isReduced_subscheme).
The order statements with the binders in the order of the main theorems #
The four theorems below duplicate isOrderSeq_ofCenters, weakTransformSeq_ofCenters_last
(Hironaka/Resolution/Algebraic/Kol07/ComponentwiseTransport.lean, ComponentwiseTransforms.lean),
isOrderSeq_componentwiseSeq and weakTransformSeq_componentwiseSeq_last
(ComponentwiseTransforms.lean), differing only in the order and explicitness of the binders:
{k} [Field k] {X} [IsNoetherian X] [CharZero k] (f) (n) [SmoothOfRelativeDimension n f], the
Noetherian hypothesis present in every statement, which is the order in which the proof of Main
Theorem II supplies them.
Hironaka.Sequence.isOrderSeq_ofCenters with the binders in the order of the main theorems;
a duplicate kept for the proofs that supply the hypotheses in this order.
Hironaka.Sequence.weakTransformSeq_ofCenters_last with the binders in the order of the main
theorems; a duplicate kept for the proofs that supply the hypotheses in this order.
Hironaka.Sequence.isOrderSeq_componentwiseSeq with the binders in the order of the main
theorems; a duplicate kept for the proofs that supply the hypotheses in this order.
Hironaka.Sequence.weakTransformSeq_componentwiseSeq_last with the binders in the order of the
main theorems; a duplicate kept for the proofs that supply the hypotheses in this order.