Tools for the core lemma of the smooth case #
The core lemma of bed_eq_nil_of_smooth — the first centre of BMO_1(X, I_Y, 1, ∅) for a smooth
Y contains a generic point of Y (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilCore) — is
proved by the descent along closed embeddings of Kollár's Claim 71.2 ([Kol07, 71], proved in Kol07,
108) along a local cover carrying a smooth hypersurface of maximal contact (Step 3 of the proof of
[Kol07, Theorem 103]). This module holds its general tools:
- the order of the ideal of a smooth closed subscheme is at most
1at every point where it is nonzero (stalkIdeal_eq_bot_of_two_le_ord_of_smooth: a regular quotient of a regular local ring is cut out by part of a regular system of parameters, [TSPA, Tag 00NR];maxOrd_le_one_of_smooth), andmax-ord I ≥ 1forI ≠ 𝒪_X; - generic points of a support are carried by a surjective coproduct of open immersions
(
mem_genericPoints_of_openImmersionCoprods: an open embedding reflects specialization); - the subscheme of
I.comap gis smooth overkfor a smoothg(smooth_comap_subschemeι_comp: Mathlib'scomapIsoand the base change), andV(J) ≅ V(j_* J)for a closed immersionj(smooth_subschemeι_comp_of_map); - when no component of a smooth hypersurface
H ⊇ V(I)lies inV(I)—Z_{-1}(I, 1, H) = 𝒪_Xin the notation of the proof of [Kol07, Lemma 102] — the restrictionI|_His nonzero on every component ofH(isNonzeroEverywhere_comap_subschemeι_of_Zminus1_eq_top).
The order of the ideal of a smooth closed subscheme #
If V(Z) is smooth over k and Z has order ≥ 2 at x, then Z_x = 0: Z_x is generated
by an initial segment of a regular system of parameters (the quotient is regular,
[TSPA, Tag 00NR]), none of which lies in 𝔪_x².
The ideal of a smooth closed subscheme, nonzero on every component, has maximal order
≤ 1.
A point of the support of an ideal sheaf other than the unit ideal.
An ideal sheaf other than the unit ideal has maximal order ≥ 1.
The ideal of a nonempty smooth closed subscheme, nonzero on every component, has maximal order
exactly 1.
Generic points along a cover and along a closed immersion #
A surjective coproduct of open immersions g carries a generic point of supp (g^* I) to a
generic point of supp I — g restricted to the summand through the point is an open embedding,
whose range is closed under generization and which reflects specialization.
The image of a point of the support under a closed immersion lies in the support of the pushed-forward ideal.
Smoothness of the subscheme along a pullback and along a pushforward #
The subscheme of g^* I for a smooth g : Y ⟶ X is smooth over k when V(I) is — it is the
base change of V(I) along g (Mathlib's comapIso).
For a closed immersion j : Y ⟶ X and J on Y, the subscheme V(J) is smooth over k when
V(j_* J) is — V(J) ⟶ V(j_* J) is an isomorphism (j_* J is the kernel of V(J) ⟶ Y ⟶ X,
Mathlib's Hom.toImage).
Nonvanishing of the restriction to a hypersurface without absorbed components #
If no irreducible component of the hypersurface H lies in V(I) — Z_{-1}(I, 1, H) = 𝒪_X
in the notation of the proof of [Kol07, Lemma 102] — then I|_H is nonzero on every irreducible
component of V(H): at a generic point η of a component of V(H), (I|_H)_η = 0 would put
I_{ι η} inside H_{ι η}, hence ι η ∈ supp I with ord_{ι η} I ≥ 1, so ι η would be a
selected generic point of Z_{-1}.