Hironaka's Main Theorems II and II(N) for every smooth scheme #
Hironaka's Main Theorem II [Hir64, Main Theorem II, pp. 142–143] and Main Theorem II(N)
[Hir64, Main Theorem II(N), p. 176] are stated for a non-singular algebraic scheme, whose
irreducible components may have different dimensions; the order reduction of the library
(exists_orderReductionRound, Kollár's BO_d of [Kol07, Theorem 68] with irreducible centres) runs
on a scheme smooth of a single relative dimension, Kollár's Notation 64. This module derives the
theorems for every scheme smooth and of finite type over the field from that case.
- One round, by components (
exists_orderReductionRound_smooth). The irreducible components of a smooth Noetherian scheme are pairwise disjoint, open and closed, and each, as an open subscheme, is irreducible and hence smooth of one relative dimension. The round of orderdis run on the component opens meeting the maximal order one after another: on a component the Triple round gives a succession with constant orderdalong its centres, with the order of the weak transform at mostdat every stage and less thandat the end (exists_orderReductionRound_opens); it is extended to the whole scheme by the unit ideal on the complement (Hironaka/Resolution/Algebraic/Hir64/ExtendOpen.lean) and its clauses transport along the stage lifts and, over the untouched complement, along the isomorphisms of the stage maps (Hironaka/Resolution/Algebraic/Hir64/OpenPieceTransport.lean); the successions of the components are concatenated. The induction (exists_orderReductionRound_extend_aux) runs over the closed opensOofXon the number of components ofXmeetingO, and produces the succession on any schemeZcontainingOas an open and closed subscheme, so that the induction hypothesis applies directly to the last stage of the previous component's round. The clauses of Hironaka's theorem are pointwise, on the centres, their supports and the points of the stages, and this is what makes the assembly possible. - Main Theorem II (
AlgebraicGeometry.exists_blowUpSequence_ord_weakTransformSeq_lt, below): for0 < d, one round of orderd(exists_orderReductionRound_smooth); ford = 0, blowing up the irreducible components one after another (Hironaka.Sequence.exists_blowUpSequence_isEmpty_last_of_smooth). - Main Theorem II(N) (
AlgebraicGeometry.exists_blowUpSequence_weakTransformSeq_eq_top, below): induction on the maximal orderdofJ, not Hironaka's route (he deduces II(N) from his fundamental theorem II₂^N, [Hir64, pp. 176–177]). Ford = 0the ideal is the unit ideal and the empty succession does; otherwise one round of orderdof the general Main Theorem II has all its centres of order exactlyd, the maximal order of the weak transform at every stage, so clause (2) of Main Theorem II(N) holds along it with thatd; its last stage is again smooth and of finite type over the field, the weak transform there has maximal order less thand, and the induction hypothesis continues with the last weak transform and boundary; the rounds concatenate (isHironakaIIN_concat). This is the induction ofexists_isHironakaIIN_of_maxOrd_leon triples, run at the level of the main theorem so that the equidimensionality of the triples never enters.
Definition 2 at a point #
Hironaka's Definition 2 [Hir64, Ch. 0, §5, Definition 2] at one point, without a second
subscheme: some regular system of parameters of 𝒪_{X,x} contains a generator of the ideal of each
irreducible component of E through x. IsSncBoundary E is this at every point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
E has only normal crossings iff it has only normal crossings at every point (the clause on
the zero ideal sheaf in IsSncBoundaryWith E ⊥ is satisfied by the empty set of
parameters).
Definition 2 at a point in the range of an open immersion, from Definition 2 at the preimage for the inverse image.
Definition 2 descends along an open immersion: at the preimage y of a point u y, for the
inverse image ideal sheaf.
Boundaries and smooth sequences along a concatenation #
Hironaka's boundaries are reduced: E₀ is, and every later boundary is a vanishing ideal
sheaf.
A smooth sequence followed by a sequence smooth over the composite of the first is a smooth sequence.
One round on an irreducible open #
One round of order reduction of order d on an irreducible open subscheme U of a smooth
scheme (smooth of one relative dimension, since irreducible), packaged with every clause the
assembly reads off it: the succession is smooth over k, its centres are regular and irreducible
with the weak transform of constant order d along them, the weak transform has order at most d
at every point of every stage and less than d at the end, and Hironaka's boundaries have only
normal crossings with the centres and at the end. If the order d is not attained on U the empty
succession does; otherwise it is the Triple round exists_orderReductionRound of
[Kol07, Theorem 68], its clauses read through IsOrderSeq.ord_eq_of_mem_center,
ord_weakTransformSeq_le_ord_stageMap and IsOrderSeq.hironakaClauses.
The clauses of one round, relative to a set over which the centres lie #
The clauses of one round of order reduction of order d for (J, E) on Z, read on the
centres, on the points of the stages, and, for the final clauses, on the points of the last stage
lying over the set R ⊆ Z over which the centres lie: the centres are regular and irreducible
(Main Theorem II (i)) and lie over R; the weak transform has order d along them (ii) and order
at most d at every point of every stage; the boundaries have only normal crossings with them
(iii); the succession is smooth over k; and at the points of the last stage over R the weak
transform has order less than d and the boundary has only normal crossings (iv).
- center (i : Fin S.length) : AlgebraicGeometry.IsRegular (S.center i).subscheme ∧ IrreducibleSpace ↥(S.center i).subscheme
- nc (i : Fin S.length) : (S.boundarySeq E i.castSucc).IsSncBoundaryWith (S.center i)
- isSmooth : S.IsSmooth g
- nc_last (z : ↥S.last) : S.composite z ∈ R → IsSncBoundaryAt (S.boundarySeq E (Fin.last S.length)) z
Instances For
The empty succession is a round over the empty set: only the order bound at the single stage is to be checked.
Two rounds concatenate: a round S₁ on Z over R₁ followed by a round S₂ on its last
stage, for the last weak transform and boundary, over R₂, is a round over any R ⊇ R₁ such that
R₂ lies over R and every point of the last stage of S₁ over R is in R₂ or over R₁. The
clauses on the centres pass through forall_center_concat, forall_stage_concat and
forall_center_concat_mem; the final clauses at a point over R₂ are those of S₂, and at a
point not over R₂ the data of S₂ is the inverse image of the last data of S₁
(ord_weakTransformSeq_of_stageMap_notMem, boundarySeq_comap_ι_preimage), for which the final
clauses of S₁ hold.
The round on a component, extended to an ambient scheme #
The image of the range of the inclusion U ⟶ O of opens under an open immersion w with
closed range is closed when U is closed in X: the range of the inclusion is the preimage of U
under O.ι, and w is a closed embedding.
One round of order reduction on an irreducible open subscheme U of X, closed in X and
contained in the open O, carried out inside an ambient scheme Z containing O as an open
subscheme with closed range along w: the round of exists_orderReductionRound_opens on U is
extended across the complement (exists_extend_of_isOpenImmersion), and its clauses are read on
Z for the ideal J_Z and boundary E_Z restricting to J and E₀ on O. Along the stage
lifts of the pull-back (which contain the centres) the weak transforms and boundaries are the
pull-backs (weakTransformSeq_pullback_of_centersInRange, boundarySeq_pullback), so the clauses
on the centres, the order bound ≤ d at points over U and the final clauses at points over U
transport; off the range of the lifts the weak transform has the order of J_Z at the image
(ord_weakTransformSeq_of_stageMap_notMem), which is ≤ d by hypothesis.
The untouched piece embeds into the last stage. Let U and V be disjoint closed opens of
X inside the open O, w : O ⟶ Z an open immersion with closed range, and S₁ a succession
on Z whose centres lie over w(U). Then V embeds into the last stage of S₁ by an open
immersion w' over w, with range the preimage of w(V) under the composite, closed, along
which the last weak transform of any J_Z and the last boundary of any reduced E_Z restrict to
the restrictions of J_Z and E_Z to V (weakTransformSeq_comap_ι_preimage,
boundarySeq_comap_ι_preimage): w' is the lift of V ⟶ Z along the open immersion of the
untouched open Z ∖ w(U) into Z through the last stage (isIso_stageMap_restrict).
The two pieces of a closed open O of the smooth X at a point o of O: U = C ∩ O for the
irreducible component C of X through o, and V = O ∖ C. They are disjoint closed opens of X
covering O, U is integral (a nonempty open of the integral component open
irreducibleComponentOpen C, the component itself since the components of the regular X are
pairwise disjoint), and V meets one component of X fewer than O does.
The induction over the components #
The round of order d, by components: for every closed open O of X and every scheme Z
containing O as an open subscheme with closed range along w, with an ideal sheaf J_Z and a
reduced boundary E_Z restricting on O to J and E₀ and with J_Z of order at most d
everywhere, a round of order d on Z over the range of w, by induction on the number of
irreducible components of X meeting O. If O is empty the empty succession does. Otherwise a
component C meets O; U := C ∩ O is a closed irreducible open of X, on which the round is
run and extended to Z (exists_orderReductionRound_extend), with centres over
R₁ = w(U); the complement V := O ∖ C meets one component fewer and embeds into the last
stage of that round over the untouched open W = Z ∖ R₁, where the stage map is an isomorphism
(isIso_stageMap_restrict) and the last weak transform and boundary are the inverse images of
J_Z and E_Z (weakTransformSeq_comap_ι_preimage, boundarySeq_comap_ι_preimage), so the
induction hypothesis gives a round on that last stage over the embedded V; the two rounds
concatenate (IsOrderRound.concat).
Main Theorem II for every smooth scheme #
One round of order reduction of order d on a smooth algebraic scheme X over k, every
irreducible component treated in turn (exists_orderReductionRound_extend_aux with O = X):
the clauses of IsOrderRound over all of X.
The order of an ideal sheaf with nonzero stalks is bounded on a smooth algebraic scheme over
k: on each of the finitely many irreducible components, smooth of one relative dimension, the
maximal order is finite (maxOrd_ne_top), and the bound is the largest of these.
Main Theorem II(N) for every smooth scheme #
Main Theorem II(N) on every smooth algebraic scheme whose ideal has order at most d
everywhere, by induction on d, iterating Main Theorem II (the induction of
exists_isHironakaIIN_of_maxOrd_le, run at the level of the main theorem; Hironaka instead deduces
II(N) from his fundamental theorem II₂^N): if the order is at most 0 the ideal is the unit ideal
and the empty succession does; otherwise either the order is at most d already, or one round of
order d + 1 (exists_orderReductionRound_smooth) has every centre of order exactly d + 1, the
maximal order at its stage, so it satisfies clauses (1)–(3) with d_i = d + 1, and its last stage,
again smooth of finite type over k, carries the last weak transform, of order at most d, and the
last boundary, reduced with only normal crossings, to which the induction hypothesis applies; the
two are concatenated (isHironakaIIN_concat).
Hironaka's Main Theorem II [Hir64, Main Theorem II, pp. 142–143]: order reduction. Let X
be a smooth algebraic k-scheme (AlgScheme k), k of characteristic zero, J an ideal sheaf on
X with nonzero stalks whose greatest order ν(J_x) over the points x of X is d, and E₀ a
reduced closed subscheme of X with only normal crossings. Then there is a finite succession of
monoidal transformations f_i : X_{i+1} → X_i with centres D_i ⊆ X_i such that
- (i) each
D_iis non-singular and irreducible (BlowUpSequence.HasRegularIrreducibleCenters); - (ii) the weak transform
J_iofJonX_ihas order at leastdat every point ofD_i; - (iii) with
E_{i+1} = red(f_i⁻¹(E_i) ∪ f_i⁻¹(D_i)), eachE_ihas only normal crossings withD_i; - (iv)
E_rhas only normal crossings andJ_rhas order less thandat every point ofX_r.
Clause (iii) and the first half of (iv) are BlowUpSequence.HasSncBoundaries; the second half of
(iv) is the last conjunct. The weak transform J_{i+1} is the pull-back of J_i along f_i
divided by the largest power of the ideal of the exceptional divisor that divides it; "has only
normal crossings (with)" is Hironaka's Definition 2 (IsSncBoundary, IsSncBoundaryWith), which
on a scheme is simple normal crossings of the reduced E_i: the condition DivisorFamily.IsSnc
(DivisorFamily.HasSncWith) of the functorial theorems, read on the family of irreducible
components of E_i.
For d = 0 (J = 𝒪_X), which the printed statement does not exclude, clause (iv) forces X_r to
be empty; blowing up the irreducible components of X one after another achieves it
(Hironaka.Sequence.exists_blowUpSequence_isEmpty_last_of_smooth). Hironaka's monoidal
transformation, defined by a universal property [Hir64, pp. 129, 166], is empty over a centre that
is a whole component, and clause (i) asks no density.
Relation to the source.
- Translation.
S.weakTransformSeq J iis Hironaka's $J_i$,S.boundarySeq E₀ ihis $E_i$, andJ.ord xhis $\nu(J_x)$;IsGreatest (Set.range J.ord) dsays that $d$ is the greatest of the orders $\nu(J_x)$. - Translation.
[Smooth (X.left ↘ Spec (.of k))]is Hironaka's "non-singular": for a scheme of finite type over the perfect fieldkthe two agree (smoothness gives the regularity of every local ring, and a non-singular such scheme is smooth). As in the print, the irreducible components ofXmay have different dimensions. - Interpretation. Hironaka's "coherent sheaf of non-zero ideals" is read as an ideal sheaf
(
X.left.IdealSheafData, quasi-coherent, hence coherent on the NoetherianX) with nonzero stalks (hJ). - Restatement. The regularity of the local rings of
Xand the invertibility of the ideal sheaf ofE₀("of everywhere codimension one"), which Hironaka also assumes, are not separate hypotheses: they follow from the hypotheses kept (regularity from smoothness over the perfect fieldk; invertibility from reducedness and normal crossings on a regular scheme, seeIsSncBoundaryWith). Of his "reduced subscheme of everywhere codimension one" only the reducedness,[IsReduced E₀.subscheme], is assumed. - Out of scope. Hironaka's remark that the theorem remains true over any local ring of his class ℬ [Hir64, p. 151; ℬ defined on p. 161], which he uses for local rings of analytic spaces (Main Theorem II′, p. 152). The base here is a field of characteristic zero, as in the print ("a field B of characteristc [sic] zero").
Source statement: [Hir64, Main Theorem II, pp. 142–143]
Hironaka's Main Theorem II(N) [Hir64, Main Theorem II(N), p. 176]: principalization by
iterated order reduction. Let X be a smooth algebraic k-scheme (AlgScheme k), k of
characteristic zero, J an ideal sheaf on X with nonzero stalks, and E a reduced closed
subscheme of X with only normal crossings. Then there is a finite succession of monoidal
transformations f_i : X_{i+1} → X_i with centres B_i ⊆ X_i such that
- (1) each
B_iis non-singular and irreducible (BlowUpSequence.HasRegularIrreducibleCenters); - (2) for each
ithere is a positive integerd_ithat is the greatest order of the weak transformJ_iofJonX_iand its order at every point ofB_i; - (3) with
E_{i+1} = red(f_i⁻¹(E_i ∪ B_i)), eachE_ihas only normal crossings withB_i; - (4)
E_rhas only normal crossings andJ_r = 𝒪_{X_r}.
Clause (3) and the first half of (4) are BlowUpSequence.HasSncBoundaries; the second half of (4)
is the last conjunct. II(N) writes red(f_i⁻¹(E_i ∪ B_i)) where II writes
red(f_i⁻¹(E_i) ∪ f_i⁻¹(D_i)), the same reduced subscheme: both are the reduced structure on
f_i⁻¹(|E_i| ∪ |B_i|). For J = 𝒪_X the empty succession satisfies every clause.
Relation to the source.
- Translation. The notation is that of Main Theorem II
(
exists_blowUpSequence_ord_weakTransformSeq_lt):S.weakTransformSeq J iis $J_i$ andS.boundarySeq E iis $E_i$.S.weakTransformSeq J (Fin.last S.length) = ⊤is $J_r = \mathcal{O}_{X_r}$, the top ideal sheaf⊤being the unit ideal. - Translation. As in Main Theorem II,
[Smooth (X.left ↘ Spec (.of k))]is Hironaka's "non-singular" (the two agree for a scheme of finite type over the perfect fieldk). - Interpretation. As in Main Theorem II, Hironaka's "coherent sheaf of non-zero ideals" is read
as an ideal sheaf with nonzero stalks (
hJ). - Gap. Hironaka's "algebraic scheme" [Hir64, Ch. I, p. 162] is a scheme of finite type over
$\operatorname{Spec} S$ for some local ring $S$ of his class ℬ (Noetherian, residue field of
characteristic zero, his condition (ii) on completions, p. 161), a class containing every field of
characteristic zero and the local rings of analytic spaces. Here
Xis separated and of finite type over a fieldkof characteristic zero. - Restatement. As in Main Theorem II, the regularity of
Xand the invertibility of the ideal sheaf ofE, which Hironaka also assumes, are not separate hypotheses: they follow from the hypotheses kept (regularity from smoothness over the perfect fieldk; invertibility from reducedness and normal crossings on a regular scheme). - Restatement. Hironaka states the theorem for $X$ of dimension $N$, the index of the
fundamental theorem II₂^N from which he deduces it [Hir64, p. 176]; $N$ does not appear in the
conclusion. The statement here is II(N) for all $N$ at once. As in the print,
Xmay have several irreducible components (Hironaka reduces the proof to irreducible $X$).
Source statement: [Hir64, Main Theorem II(N), p. 176]