Smooth pull-back of a reduced closed subscheme is reduced #
Włodarczyk's embedded desingularization "commutes with smooth morphisms" (Wlo05, Theorem 1.0.2,
(d); [Wlo05, §4.1]). The embedded resolution of Hironaka/Resolution/ divides by the REDUCED
ideal I_Γ = vanishingIdeal Γ of the absorbed strict transforms; transporting it along a smooth
h : X' → X needs (vanishingIdeal Γ).comap h = vanishingIdeal (h⁻¹ Γ), i.e. that the pull-back
of a reduced closed subscheme along a smooth morphism is reduced. In characteristic zero this is
[TSPA, Tag 033B] read through Mathlib's GeometricallyReduced: a smooth morphism is geometrically
reduced (its fibres over fields are smooth over a field, hence regular, hence reduced:
isRegularLocalRing_stalk and IsLocalRing.isDomain_of_isRegularLocalRing), and a flat
geometrically reduced morphism from a reduced scheme with finitely many irreducible components
has a reduced source (Mathlib's
GeometricallyReduced.isReduced_of_flat_of_finite_irreducibleComponents).
geometricallyReduced_of_smooth: smooth morphisms are geometrically reduced.isReduced_subscheme_of_radical_eq_self: a radical ideal sheaf cuts out a reduced subscheme (the converse ofAlgebraicGeometry.radical_eq_self_of_isReduced_subscheme).isReduced_comap_subscheme_of_smooth: the smooth pull-back of a reduced closed subscheme of a Noetherian scheme is reduced.comap_vanishingIdeal_of_smooth:(vanishingIdeal S).comap h = vanishingIdeal (h⁻¹ S).
Used for the functoriality of the embedded resolution under smooth morphisms
(Hironaka/Resolution/Algebraic/Wlo05/EmbeddedPullbackTools.lean, EmbeddedFunctorSplit.lean) and
for normal crossings (Hironaka/Resolution/Algebraic/Snc/SncLocal.lean).
A smooth morphism is geometrically reduced: every fibre product with the spectrum of a field
is smooth over that field, so its local rings are regular (isRegularLocalRing_stalk), hence
domains, hence reduced.
A radical ideal sheaf cuts out a reduced closed subscheme: the stalks of the subscheme are the
quotients of the ambient stalks by the (radical) stalk ideals
(AlgebraicGeometry.stalkEquivQuotient_of_isClosedImmersion,
Hironaka.Sequence.stalkIdeal_radical).
The pull-back of a reduced closed subscheme of a Noetherian scheme along a smooth morphism is
reduced: the fibre product h⁻¹(V(I)) = V(I) ×_X X' is the source of the flat, geometrically
reduced base change of h, over the reduced V(I) with finitely many irreducible components
(Mathlib's GeometricallyReduced.isReduced_of_flat_of_finite_irreducibleComponents); the subscheme
of I.comap h is that fibre product (comapIso).
The pull-back along a smooth morphism of the reduced ideal of a closed set is the reduced ideal of the preimage (the compatibility with smooth morphisms behind [Wlo05, §4.1]).