Hironaka's Corollaries 1 and 3 for every smooth scheme #
Hironaka's Corollary 1 [Hir64, Corollary 1, pp. 143–144], the simultaneous trivialization of a
finite system of ideal sheaves, and Corollary 3 [Hir64, Corollary 3, p. 146], the simplification
of an algebraic boundary, are proved in the library for a scheme smooth of a single relative
dimension over the field (hironaka_corollary1, hironaka_corollary3). This module derives them
for every scheme smooth and of finite type over the field, by the componentwise assembly of
Hironaka/Resolution/Algebraic/Hir64/ComponentwiseMainTheorems.lean: the irreducible components
of a smooth Noetherian scheme are disjoint closed opens, each smooth of one relative dimension; the
corollary is applied to a component, its succession is extended by the unit ideal across the
complement (exists_extend_of_isOpenImmersion), the untouched remainder embeds into the last stage
(exists_untouched_embedding), and the successions concatenate. The clauses of both corollaries
are pointwise, on the centres and on the points of the last stage, which is what the assembly
reads: IsTrivializingRound and IsBoundaryRound record them relative to the set over which the
centres lie, with concat lemmas in the manner of IsOrderRound.concat.
The corollaries themselves are stated and proved at the end of the file:
AlgebraicGeometry.exists_blowUpSequence_forall_exists_stalkIdeal_weakTransformSeq_eq_top: Corollary 1 for every smoothX, in the clauses ofhironaka_corollary1.AlgebraicGeometry.exists_blowUpSequence_isInvertible_isSncBoundary_radical_comap: Corollary 3 for every smoothX, in the clauses ofhironaka_corollary3. Its final clauses are read on the stalks: the radical of the inverse image is invertible when every stalk is generated by a nonzerodivisor (isInvertible_of_forall_stalkIdeal_eq_span), and Definition 2 holds when it holds at every point (isSncBoundary_iff_forall_isSncBoundaryAt); both transport along open immersions through the stalk isomorphisms (exists_stalkIdeal_comap_eq_span_iff,IsSncBoundaryAt.comap), and the radical of an inverse image along an open immersion is the inverse image of the radical (radical_comap_of_isOpenImmersion).
Stalks generated by a nonzerodivisor, along an open immersion #
The stalk of I at u y is generated by a nonzerodivisor iff the stalk of I.comap u at y
is, for an open immersion u: the stalk map is a ring isomorphism carrying the one ideal to the
other (stalkIdeal_comap) and nonzerodivisors to nonzerodivisors
(MulEquivClass.map_nonZeroDivisors).
The support of the inverse image of W along an open immersion is nowhere dense when the
support of W is: the preimage of a nowhere dense set under an open continuous map is nowhere
dense.
Corollary 1: the clauses of a trivializing succession, relative to a set #
The clauses of Hironaka's Corollary 1 for the system J on Z, read on the centres and, for
the final clause, on the points of the last stage lying over the set R ⊆ Z over which the
centres lie: the centres are regular and irreducible, every weak transform has constant positive
order along them (clause (1)), and at every point of the last stage over R some weak transform
has order 0, that is, is the unit ideal there (clause (2)).
- center (i : Fin S.length) : AlgebraicGeometry.IsRegular (S.center i).subscheme ∧ IrreducibleSpace ↥(S.center i).subscheme
Instances For
The empty succession is a trivializing round over the empty set.
Two trivializing rounds concatenate, as in IsOrderRound.concat: a round S₁ over R₁
followed by a round S₂ on its last stage for the last weak transforms, 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₁. At a point of the last stage not over R₂ the last weak transforms of
S₂ have the orders of those of S₁ at the image (ord_weakTransformSeq_of_stageMap_notMem).
Corollary 1 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, for a system J_Z on Z restricting to J on O: hironaka_corollary1 on U
(smooth of one relative dimension, since irreducible), extended across the complement
(exists_extend_of_isOpenImmersion), with the clauses transported along the stage lifts
(weakTransformSeq_pullback_of_centersInRange).
The induction of exists_orderReductionRound_extend_aux for Corollary 1: over the closed
opens O of X, on the number of irreducible components of X meeting O, the succession
produced on any scheme Z containing O as an open and closed subscheme along w, for a system
J_Z on Z restricting to J on O.
Corollary 3: the clauses of a boundary simplification, relative to a set #
The clauses of Hironaka's Corollary 3 for the ideal sheaf W on Z, read on the centres 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 lie over W (clause (ii)) and over R; at the points of
the last stage over R the scheme is regular (clause (i)) and the radical of the inverse image of
W has its stalk generated by a nonzerodivisor and has only normal crossings (clause (iii)).
- center (i : Fin S.length) : AlgebraicGeometry.IsRegular (S.center i).subscheme
- isRegularAt_last (z : ↥S.last) : S.composite z ∈ R → S.last.IsRegularAt z
- stalkIdeal_last (z : ↥S.last) : S.composite z ∈ R → ∃ a ∈ nonZeroDivisors ↑(S.last.presheaf.stalk z), (W.comap S.composite).radical.stalkIdeal z = Ideal.span {a}
Instances For
The empty succession is a boundary round over the empty set.
Two boundary rounds concatenate, as in IsOrderRound.concat: a round S₁ on Z for W over
R₁ followed by a round S₂ on its last stage for the inverse image W.comap S₁.composite, over
R₂, is a round for W 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 inverse image of W along the
concatenation is the inverse image along S₂ of the inverse image along S₁; at a point of the
last stage not over R₂, the composite of S₂ is an open immersion near the point
(isOpenImmersion_ι_preimage_comp_stageMap), so the radical of the inverse image is the inverse
image of the radical (radical_comap_of_isOpenImmersion) and the final clauses of S₁ at the
image transport.
Corollary 3 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, for an ideal sheaf W_Z on Z restricting to W on O: hironaka_corollary3
on U (smooth of one relative dimension, since irreducible; the support of W restricted to U
is nowhere dense), extended across the complement (exists_extend_of_isOpenImmersion), with the
clauses transported along the stage lifts: the inverse image of W_Z along the composite
restricts along the last stage lift to the inverse image of W along the composite on U
(pullbackStageHom_stageMap).
The induction of exists_orderReductionRound_extend_aux for Corollary 3: over the closed
opens O of X, on the number of irreducible components of X meeting O, the succession
produced on any scheme Z containing O as an open and closed subscheme along w, for an ideal
sheaf W_Z on Z restricting to W on O.
Hironaka's Corollary 1 [Hir64, Corollary 1, pp. 143–144], the trivialization of a system of
coherent sheaves of ideals. Let X be a smooth algebraic k-scheme (AlgScheme k), k of
characteristic zero, and J_1, …, J_e (e ≥ 1) ideal sheaves on X with nonzero stalks. Then
there is a finite succession of monoidal transformations f_i : X_{i+1} → X_i with non-singular
irreducible centres D_i ⊆ X_i (BlowUpSequence.HasRegularIrreducibleCenters) such that
- (1) every weak transform
J_j(i)of everyJ_jhas a constant positive order alongD_i(BlowUpSequence.HasConstantPositiveOrderAlongCenters); - (2) at every point of the end result
X_rat least one of the weak transformsJ_j(r)is the unit ideal.
Relation to the source.
- Translation. The weak transforms are those of Main Theorem II
(
exists_blowUpSequence_ord_weakTransformSeq_lt):S.weakTransformSeq (J j) iis Hironaka's $J_j(i)$. "$\nu(J_j(i)_y)$ is a positive constant for the points $y$ of $D(i)$" isordequal to a natural numbercwith0 < cat every point of the support of the centre ($\nu$ is integer-valued on non-zero ideals), and his $J_j(r)_x = \mathcal{O}_{X(r),x}$ is(S.weakTransformSeq (J j) (Fin.last S.length)).stalkIdeal x = ⊤, read on the stalk. His $e \ge 1$ is0 < e. - 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). - Interpretation. Hironaka's "coherent sheaves of non-zero ideals" are read as ideal sheaves
with nonzero stalks (
hJ), as in Main Theorem II. - Restatement. The regularity of the local rings of
Xis not a separate hypothesis: it follows from smoothness over the perfect fieldk.
Source statement: [Hir64, Corollary 1, pp. 143–144]
Hironaka's Corollary 3 [Hir64, Corollary 3, p. 146], the simplification of an algebraic
boundary. Let X be a smooth algebraic k-scheme (AlgScheme k), k of characteristic zero, and
W a nowhere dense closed subscheme of X, given by its ideal sheaf. Then there is a finite
succession of monoidal transformations f_i : X_{i+1} → X_i with non-singular centres D_i ⊆ X_i
such that
- (i) the end result
X_ris non-singular; - (ii) every centre lies over
W:D_i ⊆ f̄_i⁻¹(W), wheref̄_i = f_0 ∘ ⋯ ∘ f_{i-1} : X_i → X; - (iii) the associated reduced scheme
red(f̄_r⁻¹(W))off̄_r⁻¹(W)is defined by an invertible sheaf of ideals onX_rand has only normal crossings.
Hironaka asks nothing of W beyond nowhere density; W may be empty (the unit ideal sheaf, of
nowhere dense support), for which the empty succession satisfies every clause.
Relation to the source.
- Translation. $\bar f_i$ is
S.stageMap i.castSuccand $\bar f_r$ isS.composite. The associated reduced scheme $\mathrm{red}(\bar f_r^{-1}(W))$ is the radical(W.comap S.composite).radicalof the inverse image ideal sheaf; "invertible" isIsInvertible(generated on an affine neighbourhood of every point by a nonzerodivisor, an effective Cartier divisor; on the locally NoetherianX_rthis is the stalkwise condition that every stalk is generated by a nonzerodivisor of the local ring,isInvertible_iff_forall_stalkIdeal_eq_span), and "has only normal crossings" is Hironaka's Definition 2 (IsSncBoundary). - Translation. Clause (ii) is read on points: every point of a centre maps into the support of
W; since $D_i$ is non-singular, hence reduced, this is the inclusion $D_i \subseteq \bar f_i^{-1}(W)$ of subschemes. - Interpretation. Hironaka's "nowhere dense" for the closed subscheme $W$ of $X$ is read
topologically, of its support (
IsNowhereDense (W.support : Set X.left)). - Translation.
[Smooth (X.left ↘ Spec (.of k))]is Hironaka's "non-singular" forX: 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). - Restatement. The regularity of the local rings of
Xis not a separate hypothesis: it follows from smoothness over the perfect fieldk.
Source statement: [Hir64, Corollary 3, p. 146]