The clopen split of a smooth scheme along the components inside a closed subscheme #
The split X = X₀ ⊔ X₁ behind the embedded desingularization functor EDFunctor
(Hironaka.Resolution.Algebraic.Wlo05.EmbeddedFunctor): X₁ = componentsOutside Y is the union of
the irreducible components of X not contained in V(Y), X₀ its complement, and the core
coreIdeal Y = vanishingIdeal (V(Y) ∩ X₁) is the ideal the sequence BED runs on.
- On a smooth
Xtwo irreducible components through a point coincide (eq_of_mem_irreducibleComponents_of_smooth): their generic pointsη₁, η₂ ⤳ xhave closure ideals whose stalks atxare minimal primes over⊥in the regular — hence domain — stalk, so both are⊥andη₁ = η₂(eq_of_stalkIdeal_vanishingIdeal_closure_eq). Hence every component is open (isOpen_of_mem_irreducibleComponents_of_smooth) and bothX₁andX₀are open (isOpen_componentsOutside,isOpen_compl_componentsOutside). - Over
X₀ ⊆ V(Y)the reducedYis zero (stalkIdeal_eq_bot_of_notMem_componentsOutside: on an affine open insideX₀the reduced ideal ofV(Y)is that of the whole space, the nilradical of the reduced stalk); overX₁the core agrees withY(stalkIdeal_coreIdeal_of_mem_componentsOutside). - The theorem's image hypothesis on a smooth
htransfers fromYto its core (hmeets_coreIdeal): a point ofV(Y) ∩ X₁maximal for specialization there is maximal inV(Y),X₁being open. - No centre of the run lies over
X₀(notMem_center_support_of_stageMap_notMem_componentsOutside): the run is of order≥ 1for the core (isOrderGeSeq_BED), whose cosupportV(Y) ∩ X₁missesX₀(centersMiss_of_isOrderGeSeq). - The smooth locus of a closed subscheme is read on the restrictions along an open immersion
(
subschemeRestrict,mem_image_smoothLocus_iff_of_isOpenImmersion): overX₁the smooth points ofYand of its core coincide (mem_image_smoothLocus_coreIdeal_iff), and a closed subscheme smooth on each of two complementary clopens is smooth (smooth_subschemeι_comp_of_isClopen). - The exchange with smooth morphisms (
componentsOutside_comap— for flath—,coreIdeal_comap) and the transfer of the clauses: on the run the last strict transforms ofYand of its core agree overX₁while that ofYis zero overX₀, so the core's clauses (c1), (c2), (e) and the clause (b) about the smooth points ofYtransfer toY(smooth_strictTransformSeq_last_of_coreIdeal,hasSncWith_strictTransformSeq_last_of_coreIdeal,comap_composite_eq_strictTransform_mul_of_coreIdeal,stageMap_notMem_image_smoothLocus_of_coreIdeal).
The clauses are those of [Wlo05, Theorem 1.0.2]; the equidimensionality convention is
[Kol07, Notation 64]. These are the tools of
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedFunctorClauses.
On a smooth scheme two irreducible components through a point coincide: at the point the stalk
is a domain, the closure ideals of the two generic points have stalks that are minimal primes over
⊥, hence both ⊥, and equal stalks force equal generic points
(eq_of_stalkIdeal_vanishingIdeal_closure_eq). Compare
eq_of_mem_irreducibleComponents_of_isRegular
(Hironaka.Resolution.Algebraic.Kol07.Thm36.Identification), the same fact for a regular closed
subscheme.
On a smooth Noetherian scheme every irreducible component is open (its complement is the finite union of the other components, which it does not meet).
X₁ = componentsOutside Y is open on a smooth Noetherian scheme (a union of components).
On a smooth scheme a point lies in X₁ iff ITS component is not inside V(Y).
The clopen split: X₀, the complement of componentsOutside Y, is open — it is the union
of the components inside V(Y), each open.
the components inside V(Y) lie in V(Y) — every point lies on its component.
over X₀ the reduced Y is the zero ideal — X₀ is an open subset of V(Y) in the
reduced X, so on an affine open inside X₀ the reduced ideal of V(Y) is that of the whole
space, whose stalk is the nilradical of the reduced stalk.
Over X₁ the core agrees with Y stalkwise: on an affine open inside the open X₁,
V(Y) ∩ X₁ is V(Y), and Y is the reduced ideal of V(Y).
The transfer of the image hypothesis from Y to its core (the smoothness of X is needed): a
point of V(core Y) = V(Y) ∩ X₁ maximal for specialization there is maximal in V(Y) — a
generization in V(Y) of a point of the open X₁ lies in X₁ — so the theorem's hypothesis on
h's image implies the core's.
No centre over X₀: the run of the functor misses X₀ — it is a run of order ≥ 1 for the
core (isOrderGeSeq_BED), whose cosupport V(Y) ∩ X₁ is inside X₁
(centersMiss_of_isOrderGeSeq); off the equidimensional schemes the run is empty.
Pointwise: a point of a centre of the run of the functor does not lie over X₀.
The run over the two clopens #
X₀, the union of the components inside V(Y), as an open of X.
Equations
- Hironaka.Resolution.insideOpens k X Y = { carrier := (↑(Hironaka.Resolution.componentsOutside Y))ᶜ, is_open' := ⋯ }
Instances For
X₁, the union of the components outside V(Y), as an open of X.
Equations
- Hironaka.Resolution.outsideOpens k X Y = { carrier := ↑(Hironaka.Resolution.componentsOutside Y), is_open' := ⋯ }
Instances For
Pulled back to X₀, the run of the functor has only empty centres (no centre lies over
X₀).
Over X₀ the reduced Y pulls back to the zero ideal sheaf.
Over X₁ the core and Y pull back to the same ideal sheaf.
A point of a stage of the run lying over X₀ is in the image of the stage of the pull-back.
A point of a stage of the run lying over X₁ is in the image of the stage of the pull-back.
The strict transform of Y over X₀ is the zero ideal at the points over X₀ — pulled back
to X₀ the run has empty centres, so the strict transform is the pull-back of Y|_{X₀} = 0.
No exceptional member over X₀: no member of the total transform of the empty family
passes through a point over X₀ — pulled back to X₀ every centre is empty, so every member of
the pulled-back total transform is the unit ideal.
Locality over X₁: over X₁ the strict transforms of Y and of its core agree — both
are the pull-backs along X₁ ↪ X of the same ideal sheaf (strictTransformSeq_pullback).
The remaining glue: a point on no member; the exchange along a flat morphism #
Clause (c2) at a point with no member through it: a regular system of parameters is an
snc system for E at a point lying on no member of E — the index type of the members through the
point is empty.
An irreducible set lies in an irreducible component.
The generic point of a component not inside a closed set lies outside it.
The exchange with a flat morphism, components: for a flat h : X' → X a component of X'
lies in V(h^*Y) iff the component of X through its image does — h is generalizing
(Flat.generalizingMap): the generic point of a component of X through h x' lifts to a
generization of x', whose closure lies in a component of X' not inside h⁻¹ V(Y); conversely
the image of a component of X' is an irreducible set inside a component of X.
The exchange with a smooth morphism, cores: core (h^* Y) = h^* (core Y) for smooth h — the
component exchange, support_comap, and comap_vanishingIdeal_of_smooth.
The second leg V(ι^* Z) → V(Z) of Mathlib's pull-back square of Z.subschemeι along ι
(comapIso); an open immersion when ι is.
Equations
Instances For
The restriction square commutes: V(ι^* Z) → V(Z) → X is V(ι^* Z) → W → X.
The image of the restriction is the part of V(Z) over W (the square is a pull-back).
The smooth locus of two equal morphisms is the same.
Smooth-locus locality along an open immersion: a point of V(Z) over W is smooth over T iff
its preimage in V(Z) ∩ W is smooth for the restricted composite (preimage_smoothLocus_eq).
Smooth points of V(Z) over W, read on V(Z) ∩ W: a point ι w lies in the image of the
smooth locus of V(Z) → T iff it is the image of a point of V(Z) ∩ W smooth for the restricted
composite.
Clause (c1): a closed subscheme smooth over k on each of two complementary clopens
is smooth over k — smoothness is Zariski-local on the source (IsZariskiLocalAtSource, found
under the transparency setting Mathlib's smoothLocus_eq_top_iff uses), and the two restrictions
subschemeRestrict Z U.ι, subschemeRestrict Z U'.ι form an open cover of V(Z)
(range_subschemeRestrict).
Over X₁ the smooth points of Y and of its core coincide: x = ι w for the open immersion
ι : X₁ ↪ X, both images are read on the restrictions to X₁
(mem_image_smoothLocus_iff_of_isOpenImmersion), and the two restricted ideals agree
(stalkIdeal_coreIdeal_of_mem_componentsOutside, stalkwise).
A closed subscheme with zero ideal is the whole scheme: smooth over T when the scheme is.
Clause (c2): Z has snc with E when at every point its stalk is that of a Z' having snc
with E, or is zero at a point on no member of E (there a regular system of parameters of the
regular stalk of the smooth scheme, with no coordinate used, is an snc system).
Over any scheme mapping into a stage over X₀ the strict transform of Y pulls back to zero
(stalkwise).
Over any scheme mapping into a stage over X₁ the strict transforms of the core and of Y pull
back to the same ideal sheaf (stalkwise).
Over X₁ the supports of the strict transforms of the core and of Y agree.
Clause (e): the fine factorisation of the core's total pull-back gives that of Y with the same
snc divisor, stalkwise — over X₁ the ideals agree, over X₀ both sides are zero.
Clause (c1): the last strict transform of Y is smooth over k when that of the core is — over
the clopen part of the last stage over X₁ they agree, over the part over X₀ the strict transform
of Y is zero and the stage is smooth (smooth_subschemeι_comp_of_isClopen).
Clause (c2): the last strict transform of Y has snc with the exceptional family when that of
the core does (hasSncWith_of_forall_stalkIdeal: over X₁ the stalks agree, over X₀ the stalk is
zero at a point on no exceptional member).
Clause (b): the Reg-window clause for Y from that of the core — a point of a centre lies over
X₁, where the strict transforms and the smooth points of Y and its core agree.