Independence of the singular locus from an unramified base

Let X → Spec S → Spec R be a compatible pair of structure morphisms, with S/R formally unramified. When both structure morphisms define relative curves, their singular ideal sheaves on X agree: Ω[A⁄R] ≃ Ω[A⁄S] on every affine open of X, so their first Fitting ideals agree.

Together with restriction on the source, this comparison identifies singular loci computed on overlapping affine base charts. The equality is scheme-theoretic and does not discard nilpotents in the singular subscheme.

References

• The Stacks Project, Tag 00RS: the transitivity sequence for differentials.
• The Stacks Project, Tag 0C3C: Fitting ideal sheaves.

theorem AlgebraicGeometry.Scheme.singularLocus_eq_of_formallyUnramified_base {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] {X : Scheme} [X.Over (Spec ↧R)] [X.Over (Spec ↧S)] [Algebra.FormallyUnramified R S] [Flat (X ↘ Spec ↧R)] [LocallyOfFinitePresentation (X ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧R)] [Flat (X ↘ Spec ↧S)] [LocallyOfFinitePresentation (X ↘ Spec ↧S)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧S)] (h : CategoryTheory.CategoryStruct.comp (X ↘ Spec ↧S) (Spec.map (CommRingCat.ofHom (algebraMap R S))) = X ↘ Spec ↧R) : singularLocus R X = singularLocus S X

The relative singular ideal is unchanged on enlarging the affine base through a formally unramified algebra, provided the structure morphisms are compatible.

theorem AlgebraicGeometry.Scheme.singularLocus_eq_comap_of_isOpenImmersion_of_formallyUnramified_base {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FormallyUnramified R S] {X Y : Scheme} [X.Over (Spec ↧S)] [Y.Over (Spec ↧R)] [Flat (Y ↘ Spec ↧R)] [LocallyOfFinitePresentation (Y ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (Y ↘ Spec ↧R)] [Flat (X ↘ Spec ↧S)] [LocallyOfFinitePresentation (X ↘ Spec ↧S)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧S)] (i : X ⟶ Y) [IsOpenImmersion i] (h : CategoryTheory.CategoryStruct.comp (X ↘ Spec ↧S) (Spec.map (CommRingCat.ofHom (algebraMap R S))) = CategoryTheory.CategoryStruct.comp i (Y ↘ Spec ↧R)) : singularLocus S X = (singularLocus R Y).comap i

Singular loci computed on different affine bases agree after restriction along an open immersion of sources, when the base-ring map is formally unramified and the structure morphisms commute.

theorem AlgebraicGeometry.Scheme.isPullback_singularLocus_subschemeι_of_isOpenImmersion_of_formallyUnramified_base {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FormallyUnramified R S] {X Y : Scheme} [X.Over (Spec ↧S)] [Y.Over (Spec ↧R)] [Flat (Y ↘ Spec ↧R)] [LocallyOfFinitePresentation (Y ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (Y ↘ Spec ↧R)] [Flat (X ↘ Spec ↧S)] [LocallyOfFinitePresentation (X ↘ Spec ↧S)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧S)] (i : X ⟶ Y) [IsOpenImmersion i] (h : CategoryTheory.CategoryStruct.comp (X ↘ Spec ↧S) (Spec.map (CommRingCat.ofHom (algebraMap R S))) = CategoryTheory.CategoryStruct.comp i (Y ↘ Spec ↧R)) : CategoryTheory.IsPullback (singularLocus S X).subschemeι ((singularLocus S X).subschemeMap (singularLocus R Y) i ⋯) i (singularLocus R Y).subschemeι

Restriction of sources and a formally unramified change of affine base give a pullback square of singular subschemes.