The relative singular locus

Let X be flat and locally of finite presentation over a commutative ring R, with every nonempty fibre pure of dimension one. The sheaf of relative differentials Ω_{X/R} is quasi-coherent, and its sections over every affine open are finitely generated, so it has Fitting ideal sheaves. The relative singular locus Sing(X/R) is the closed subscheme of X cut out by the first Fitting ideal sheaf Fitt₁(Ω_{X/R}).

Over an affine open U its ideal is the first Fitting ideal of the module of Kähler differentials Ω[Γ(X, U)⁄R], and a point x lies in Sing(X/R) exactly when the fibre Ω_{X/R} ⊗ κ(x) has dimension at least two, that is, when Ω_{X/R} needs at least two generators near x. For a family of curves this is the closed subscheme in terms of which the Stacks Project defines families of nodal curves.

Main definitions

• AlgebraicGeometry.Scheme.singularLocus R X: the ideal sheaf Fitt₁(Ω_{X/R}) of the relative singular locus; its closed subscheme is (X.singularLocus R).subscheme.

Main results

• AlgebraicGeometry.Scheme.singularLocus_ideal: over an affine open U, the ideal of the singular locus is the first Fitting ideal of Ω[Γ(X, U)⁄R].
• AlgebraicGeometry.Scheme.mem_support_singularLocus_iff: a point x of an affine open U lies in the singular locus exactly when 1 < dim_{κ(x)} κ(x) ⊗ Ω[Γ(X, U)⁄R].
• AlgebraicGeometry.Scheme.singularLocus_ideal_top_Spec: on Spec A, the ideal of global sections is the image of the first Fitting ideal of Ω[A⁄R].
• AlgebraicGeometry.Scheme.singularLocus_eq_top: a smooth relative curve, smooth of relative dimension one over Spec R, has empty singular locus: there Ω_{X/R} is locally free of rank one, so its first Fitting ideal sheaf is the unit ideal sheaf.
• AlgebraicGeometry.Scheme.singularLocus_eq_comap_of_isPullback: the formation of the singular locus commutes with base change along Spec R' → Spec R: if X' is the base change of X, then Sing(X'/R') is the inverse image of Sing(X/R).
• AlgebraicGeometry.Scheme.isPullback_singularLocus_subschemeι: the same for the closed subschemes, Sing(X'/R') = Sing(X/R) ×_X X'.

Restriction to open subschemes, and more generally to étale neighbourhoods, is AlgebraicGeometry.Scheme.singularLocus_eq_comap_of_etale. Together with base change, it lets the affine-base singular loci agree on affine overlaps and identifies the singular subscheme after extending the ground ring. It is therefore the local input for gluing the relative singular locus over a general base and for transporting that locus under base change.

References

• Stacks Project, Tag 0C3C: Fitting ideals of a finite type quasi-coherent module.
• Stacks Project, Tag 0C58: families of nodal curves, where the singular locus of a family of curves is cut out by the first Fitting ideal of its sheaf of relative differentials.

noncomputable def AlgebraicGeometry.Scheme.singularLocus (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] [_hflat : Flat (X ↘ Spec ↧R)] [_hfinite : LocallyOfFinitePresentation (X ↘ Spec ↧R)] [_hpure : TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧R)] : X.IdealSheafData

The relative singular locus of a flat, locally finitely presented scheme X of pure relative dimension one over Spec R, as an ideal sheaf: the first Fitting ideal sheaf Fitt₁(Ω_{X/R}) of the sheaf of relative differentials. Its support is the set of points at which the fibre of Ω_{X/R} has dimension at least two (AlgebraicGeometry.Scheme.mem_support_singularLocus_iff).

theorem AlgebraicGeometry.Scheme.singularLocus_def (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] [Flat (X ↘ Spec ↧R)] [LocallyOfFinitePresentation (X ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧R)] : singularLocus R X = (relativeDifferentials R X).fittingIdeal ⋯ 1

The singular locus is the first Fitting ideal sheaf of the relative differentials.

theorem AlgebraicGeometry.Scheme.singularLocus_ideal (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] [Flat (X ↘ Spec ↧R)] [LocallyOfFinitePresentation (X ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧R)] (U : ↑X.affineOpens) : (singularLocus R X).ideal U = TauCeti.fittingIdeal ↑(X.presheaf.obj (Opposite.op ↑U)) Ω[↑(X.presheaf.obj (Opposite.op ↑U))⁄R] 1

Over an affine open U, the ideal of the singular locus is the first Fitting ideal of the module of Kähler differentials Ω[Γ(X, U)⁄R].

theorem AlgebraicGeometry.Scheme.mem_support_singularLocus_iff (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] [Flat (X ↘ Spec ↧R)] [LocallyOfFinitePresentation (X ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧R)] {x : ↥X} {U : ↑X.affineOpens} (hx : x ∈ ↑U) : x ∈ (singularLocus R X).support ↔ 1 < Module.finrank (↑(X.residueField x)) (TensorProduct ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(X.residueField x) Ω[↑(X.presheaf.obj (Opposite.op ↑U))⁄R])

The support of the singular locus. A point x of an affine open U lies in the singular locus exactly when the fibre κ(x) ⊗ Ω[Γ(X, U)⁄R] of the relative differentials at x has dimension greater than one.

theorem AlgebraicGeometry.Scheme.singularLocus_ideal_top_Spec (R : Type u) [CommRing R] (A : CommRingCat) [Algebra R ↑A] [Algebra.FiniteType R ↑A] [Flat (Spec A ↘ Spec ↧R)] [LocallyOfFinitePresentation (Spec A ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (Spec A ↘ Spec ↧R)] : (singularLocus R (Spec A)).ideal ⟨⊤, ⋯⟩ = Ideal.map (CommRingCat.Hom.hom (ΓSpecIso A).inv) (TauCeti.fittingIdeal ↑A Ω[↑A⁄R] 1)

On an affine scheme Spec A of finite type over R, the ideal of global sections of the singular locus is the image of the first Fitting ideal of Ω[A⁄R] under A ≅ Γ(Spec A, ⊤).

@[simp]

theorem AlgebraicGeometry.Scheme.singularLocus_eq_top (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] [SmoothOfRelativeDimension 1 (X ↘ Spec ↧R)] : singularLocus R X = ⊤

A smooth relative curve has empty singular locus. If X is smooth of relative dimension one over Spec R, then the first Fitting ideal sheaf of Ω_{X/R} is the unit ideal sheaf, since Ω_{X/R} is locally free of rank one.

theorem AlgebraicGeometry.Scheme.singularLocus_eq_comap_of_isPullback {R R' : Type u} [CommRing R] [CommRing R'] [Algebra R R'] {X X' : Scheme} [X.Over (Spec ↧R)] [X'.Over (Spec ↧R')] {g : X' ⟶ X} [Flat (X ↘ Spec ↧R)] [LocallyOfFinitePresentation (X ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧R)] [Flat (X' ↘ Spec ↧R')] [LocallyOfFinitePresentation (X' ↘ Spec ↧R')] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X' ↘ Spec ↧R')] (H : CategoryTheory.IsPullback g (X' ↘ Spec ↧R') (X ↘ Spec ↧R) (Spec.map (CommRingCat.ofHom (algebraMap R R')))) : singularLocus R' X' = (singularLocus R X).comap g

The singular locus commutes with base change. If X' is the base change of X along Spec R' → Spec R, with projection g : X' ⟶ X, then the singular locus of X' over R' is the inverse image under g of the singular locus of X over R. For the closed subschemes, see AlgebraicGeometry.Scheme.isPullback_singularLocus_subschemeι.

theorem AlgebraicGeometry.Scheme.isPullback_singularLocus_subschemeι {R R' : Type u} [CommRing R] [CommRing R'] [Algebra R R'] {X X' : Scheme} [X.Over (Spec ↧R)] [X'.Over (Spec ↧R')] {g : X' ⟶ X} [Flat (X ↘ Spec ↧R)] [LocallyOfFinitePresentation (X ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧R)] [Flat (X' ↘ Spec ↧R')] [LocallyOfFinitePresentation (X' ↘ Spec ↧R')] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X' ↘ Spec ↧R')] (H : CategoryTheory.IsPullback g (X' ↘ Spec ↧R') (X ↘ Spec ↧R) (Spec.map (CommRingCat.ofHom (algebraMap R R')))) : CategoryTheory.IsPullback (singularLocus R' X').subschemeι ((singularLocus R' X').subschemeMap (singularLocus R X) g ⋯) g (singularLocus R X).subschemeι

The singular subscheme commutes with base change. If X' is the base change of X along Spec R' → Spec R, with projection g : X' ⟶ X, then Sing(X'/R') is the base change Sing(X/R) ×_X X' of the closed subscheme Sing(X/R), and hence the base change of Sing(X/R) along Spec R' → Spec R.