The embedded desingularization functor #
[Wlo05, Theorem 1.0.2] asks for an assignment Y ↦ S of a succession of blow-ups to EVERY
reduced closed subscheme Y of a smooth equidimensional k-scheme X of finite type — the
functor type EmbeddedDesingularizationAssignment k has the single field seq, defined on every
smooth X of finite type and every ideal sheaf Y. The embedded desingularization sequence BED
(Hironaka.Resolution.Algebraic.Wlo05.Embedded) runs on a Triple k: X equidimensional and the
ideal NONZERO ON EVERY IRREDUCIBLE COMPONENT of X (Kollár's standing convention, Kol07, Notation
64). The theorem's hypotheses have the former (∃ n, SmoothOfRelativeDimension n (X ↘ Spec k)) and
not the latter: a reduced Y may contain irreducible components of X (Włodarczyk's X is a
variety, where this means Y = X).
The totalisation. EDFunctor k assigns BED ⟨X, hX, coreIdeal Y, …, ∅, …⟩ when X is
equidimensional (classically decided) and the empty succession otherwise, where the core of
Y is the reduced ideal sheaf of V(Y) ∩ X₁, X₁ = componentsOutside Y the (finite, closed)
union of the irreducible components of X NOT contained in V(Y):
coreIdeal Yis reduced by construction (isReduced_subscheme_vanishingIdeal) and nonzero everywhere on any Noetherian space (isNonzeroEverywhere_coreIdeal; the scheme is one bynoetherianSpace_of_field): offV(Y) ∩ X₁its stalk is the unit ideal; at a point of a componentC ⊄ V(Y)a zero stalk would propagate to the generic point ofC(stalkIdeal_eq_bot_of_specializes), putting it — henceC— insideV(Y);- when
Yis reduced and nonzero everywhere,coreIdeal Y = Y(coreIdeal_eq_of_isNonzeroEverywhere): no component lies inV(Y)(at a generic point of a component the maximal ideal of the smooth stalk is zero,maximalIdeal_stalk_eq_bot_of_isGenericPoint), soX₁ = XandV(Y)'s reduced ideal isY(vanishingIdeal_support_of_isReduced). Hence on the inputs of the sources(EDFunctor k).seq X Y = BED ⟨X, hX, Y, hY, DivisorFamily.empty X, _⟩on the nose (EDFunctor_seq_of_isNonzeroEverywhere); off them the run isBEDof the core onXitself — no pushforward, no second scheme — and the clauses aboutYfollow from the clauses about the core on the clopen coverX = X₀ ⊔ X₁(Hironaka.Resolution.Algebraic.Wlo05.EmbeddedFunctorSplit,Hironaka.Resolution.Algebraic.Wlo05.EmbeddedFunctorClauses).
The functor is the witness of the theorem
AlgebraicGeometry.exists_functorial_embeddedDesingularization
(Hironaka.Resolution.Algebraic.Wlo05.EmbeddedFunctorClauses).
For the empty succession on disconnected inputs compare [Kol07, Warning 38].
The core of an ideal sheaf: the reduced ideal of V(Y) on the components outside V(Y) #
The union of the irreducible components of X NOT contained in V(Y) — finitely many closed
sets (X a Noetherian space), so closed. Named after Mathlib's irreducibleComponents; the
complement is the union of the components inside V(Y).
Equations
Instances For
The core of Y — the reduced ideal sheaf of V(Y) ∩ X₁, X₁ the components of X
outside V(Y); the ideal on which BED is run.
Equations
Instances For
The core is nonzero on every irreducible component ([Kol07, Notation 64 (2)]): off V(Y) ∩ X₁
its stalk is the unit ideal; at x ∈ X₁, on a component C ⊄ V(Y) through x with generic point
η ⤳ x, a zero stalk at x would be a zero stalk at η (stalkIdeal_eq_bot_of_specializes), so
η ∈ V(Y) and C = closure {η} ⊆ V(Y).
On a smooth X, an ideal sheaf nonzero everywhere is contained in no irreducible component's
ideal: at the generic point η of a component the smooth stalk is a field
(maximalIdeal_stalk_eq_bot_of_isGenericPoint), so Y_η ≤ 𝔪_η = ⊥ contradicts Y_η ≠ ⊥. Hence
every component is outside V(Y).
On the inputs of the sources — Y reduced and nonzero everywhere on the smooth X — the core
is Y itself: X₁ = X and V(Y)'s reduced ideal is Y.
The functor #
BED depends on the triple's ideal only through its value: changing the proof-irrelevant fields
and rewriting the ideal along an equation gives the same succession.
A scheme quasi-compact and locally of finite type over a field is Noetherian
(Scheme.Hom.isNoetherian_of_field), hence a Noetherian space (Mathlib's
IsNoetherian.noetherianSpace).
The embedded desingularization functor — the witness of
AlgebraicGeometry.exists_functorial_embeddedDesingularization ([Wlo05, Theorem 1.0.2]): on an
equidimensional X (classically decided) the embedded desingularization sequence BED on the
triple (X, coreIdeal Y, ∅), the empty succession otherwise (the theorem asserts nothing there).
On the inputs of the sources the core is Y (EDFunctor_seq_of_isNonzeroEverywhere).
Equations
- One or more equations did not get rendered due to their size.
Instances For
On an equidimensional X the functor is BED on the core.
Off the equidimensional schemes the functor assigns the empty succession.
The inputs of the sources: for Y reduced and nonzero everywhere on the equidimensional X,
the functor is BED ⟨X, hX, Y, hY, ∅, _⟩ on the nose.