Hironaka's Corollary 1: simultaneous trivialization of a finite system of ideal sheaves #
Corollary 1 of Main Theorem II [Hir64, Corollary 1, pp. 143–144]: given nonzero ideal sheaves
J_1, …, J_e on a non-singular X, there is a finite succession of monoidal transformations with
non-singular irreducible centers such that (1) every weak transform J_j(i) has constant positive
order along the center D(i), and (2) at every point of the end result at least one J_j(r) is
the unit ideal. Hironaka calls this the trivialization of a system of coherent sheaves of ideals.
The proof, following Hironaka's. Let J := ∏ J_j, T_0 := ⋂ |J_j| and, if T_0 ≠ ∅,
d := max {ν(J_x) : x ∈ T_0} (finite since J is nonzero everywhere on a Noetherian scheme).
Hironaka's loci are T := {ν(J) ≥ d}, S := T ∖ T_0 and T ∖ S = T ∩ T_0. The last is closed
(trivializationLoci_closed); S is closed too, Hironaka's "we can prove that T, S and
T − S are all closed", proved here by upper semicontinuity and additivity of the orders
(isClosed_trivialLocus): around a point q ∈ T ∖ S, where ν(J_q) = d and every
ν((J_j)_q) ≥ 1, the open set {ν(J) ≤ d} ∩ ⋂_j {ν(J_j) ≤ ν((J_j)_q)} misses S, since a point
of S in it would have some ν(J_{j_0}) = 0 and hence ν(J) ≤ d − 1; and {ν(J) < d} misses
S outright. Main Theorem II (one round of order reduction, exists_orderReductionRound) applied
to (X̄ := X ∖ S, J|_{X̄}, ∅), whose max-ord is exactly d, gives a smooth blow-up sequence with
regular irreducible centers of order d whose last weak transform has max-ord < d; by clause
(ii) of Main Theorem II the centers lie over T ∖ S. The sequence extends across S
(Hironaka/Resolution/Algebraic/Hir64/ExtendOpen.lean), the extension S₁ on X having
S₁.pullback u = S̄ and centers in the ranges of the stage lifts, along which regularity,
irreducibility, smoothness and the weak transforms transport
(Hironaka/Scheme/BlowUpSequence/OpenTransport.lean). Along S̄ the weak transform of the product
is the product of the weak transforms and each factor has constant order on each center; the
constants are positive because the order of a weak transform at a point over the center never
exceeds the order at the image (Hironaka's (B*) [Hir64, p. 143]; [Kol07, Lemma 61] read pointwise
along a center of constant order, ord_weakTransform_le_ord_of_forall_ord_eq), the image lies in
T ∖ S where every factor has order ≥ 1, and the orders add up to d on both sides. Over S
the transforms are unchanged (ord_weakTransformSeq_of_stageMap_notMem), so on the end result the
factors are simultaneously nontrivial only over X̄, where the product has order < d. Induction
on d and concatenation (concat, with the per-stage clauses of
Hironaka/Scheme/BlowUpSequence/ConcatClauses.lean) finish; at T_0 = ∅ the empty sequence does.
ℕ∞ bookkeeping #
Kollár's Lemma 61 pointwise along a center of constant order #
Hironaka's (B*) [Hir64, p. 143]; [Kol07, Lemma 61] read pointwise: along a smooth center Z
on which I has constant order m at every point, the weak transform of I has order at most
m = ord_{π q} I at every point q over the center. This is the argument of
ord_controlledTransform_le_of_smooth with the global hypothesis max-ord I = m replaced by the
constancy on Z (the only use of max-ord there was ord_{π q} I ≤ m). Off the center the
blow-up is an isomorphism and the orders agree.
Used for the positivity in condition (1) of [Hir64, Corollary 1].
Orders along a smooth sequence: monotonicity, the unchanged region, the product #
Along a smooth sequence whose induced ideals have constant order on every center, the order of
the i-th induced ideal at any point is at most the order of the original ideal at its image;
ord_weakTransform_le_ord_of_forall_ord_eq stage by stage.
Over a point outside a closed set C containing the images of all the centers, the order of
every induced ideal is the order of the original: each blow-up is an isomorphism there
(ord_weakTransform_of_notMem). In the proof of [Hir64, Corollary 1] this is the observation that
over S the transforms are unchanged.
Along a smooth sequence with irreducible centers on which the induced ideals of the product
∏ J_l have constant order d, the induced ideal of the product at every stage is the product of
the induced ideals of the factors; weakTransform_prod_of_smooth stage by stage, the constancy of
each factor's order on the center being ord_factors_const_on_center_of_smooth.
Condition (1) of [Hir64, Corollary 1] without positivity: along a smooth sequence with
irreducible centers on which the induced ideals of ∏ J_l have constant order d, every factor's
induced ideal has constant order on every center.
Along a smooth sequence the induced ideals of an ideal nonzero on every component are nonzero on every component.
A finite product of ideal sheaves nonzero on every component is nonzero on every component of
a smooth k-scheme (the orders add and are finite).
"We can prove that T, S and T − S are all closed" [Hir64, Corollary 1, proof], the case
of S: in Hironaka's notation T := {ν(J) ≥ d}, the set S := T ∖ ⋂_j |J_j| is closed when d
bounds ν(J) on ⋂_j |J_j|. The complement is open: around a point of order < d by upper
semicontinuity, and around a point q of order ≥ d with all J_j nontrivial (so ν(J_q) = d)
the open set {ν(J) ≤ d} ∩ ⋂_j {ν(J_j) ≤ ν((J_j)_q)} misses S, a point of S in it having some
ν(J_{j₀}) = 0 and hence ν(J) ≤ d − 1.
One round of Hironaka's argument #
The trivial case of [Hir64, Corollary 1] ("if otherwise, the assertion is trivial"): when at
every point some J_j is the unit ideal, the empty sequence does.
One round of Hironaka's argument for [Hir64, Corollary 1], as described in the module
docstring, at the maximal order d ≥ 1 of ∏ J_j on ⋂_j |J_j| ≠ ∅: a smooth sequence on X
with regular irreducible centers, every factor of constant positive order on every center
(condition (1)), and ν(∏_j J_j(r)) < d at every point of the end result where all the J_j(r)
are nontrivial.
Induction on d and assembly #
[Hir64, Corollary 1] for every system whose product has order at most d on the common
support ("either the integer d gets reduced, or (2) is achieved"): induction on d, one round
(exists_round) followed by the induction hypothesis at the end result, the two sequences
concatenated.
Hironaka's Corollary 1 [Hir64, Corollary 1, pp. 143–144], the trivialization of a system
of coherent sheaves of ideals: a finite succession of monoidal transformations with
non-singular irreducible centers such that (1) every weak transform J_j(i) has constant positive
order along the center D(i), and (2) at every point of the end result at least one J_j(r) is
the unit ideal. This is exists_corollary1_seq_of_maxOrdAlong_le at the (finite) maximal order of
∏ J_j on ⋂_j |J_j|. Hironaka's non-singularity of X is not a hypothesis: the proof runs the
order reduction of Main Theorem II on X, which is smooth of a single relative dimension over the
field k of characteristic zero (hN; the restriction is lifted in ComponentwiseCorollaries),
and smoothness over the perfect field k gives the regularity of the local rings.