The singular locus and its ideal sheaf

Consequences of the comparison of regular and smooth points for X locally of finite type over a perfect field k: the singular locus Sing X is the complement of the smooth locus of X → Spec k (Hironaka/Algebra/RegularSmooth/RegularSmoothEquiv.lean), hence closed (Mathlib's Scheme.Hom.isOpen_smoothLocus; [TSPA, Tag 00TT]); the regular locus is dense when X is reduced and contains the generic point when X is integral (Mathlib's dense_smoothLocus_of_perfectField, genericPoint_mem_smoothLocus_of_perfectField); and the ideal sheaf 𝒥 of Sing X with its reduced structure is the vanishing ideal sheaf of Sing X (Scheme.singIdeal). The main theorems (Challenge/Algebraic.lean) state Main Theorem I with Sing X.

Sing X need not be closed for an arbitrary scheme, and Mathlib's IdealSheafData.vanishingIdeal takes a closed set; since the vanishing ideal of a set is that of its closure, singIdeal X is defined for every scheme as the vanishing ideal sheaf of closure (Sing X), and under the hypotheses above its support is exactly Sing X (coe_support_singIdeal_eq_singularLocus). It is a radical ideal sheaf (the reduced induced structure), and it is the unit ideal iff X is regular.

noncomputable def AlgebraicGeometry.Scheme.singIdeal (X : Scheme) : X.IdealSheafData

The ideal sheaf 𝒥 of the singular locus with its reduced structure: the vanishing ideal sheaf of closure (Sing X), whose support is Sing X itself when the latter is closed. It is a factor of the single centre D with |D| = Sing X in Hironaka/Resolution/Algebraic/Hir64/SingleCenter.lean.

Equations

• X.singIdeal = AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal { carrier := closure X.singularLocus, isClosed' := ⋯ }

theorem AlgebraicGeometry.Scheme.singularLocus_eq_compl_smoothLocus {k : Type u} [Field k] {X : Scheme} [PerfectField k] (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] : X.singularLocus = (↑(Hom.smoothLocus f))ᶜ

For X locally of finite type over a perfect field k, Sing X is the complement of the smooth locus of X → Spec k ([TSPA, Tag 00TT] with [TSPA, Tag 00TV]).

theorem AlgebraicGeometry.Scheme.isClosed_singularLocus {k : Type u} [Field k] {X : Scheme} [PerfectField k] (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] : IsClosed X.singularLocus

Sing X is closed when X is locally of finite type over a perfect field.

theorem AlgebraicGeometry.Scheme.dense_setOf_isRegularAt {k : Type u} [Field k] {X : Scheme} [PerfectField k] [IsReduced X] (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] : Dense {x : ↥X | X.IsRegularAt x}

For X reduced and locally of finite type over a perfect field, the regular locus is dense (Mathlib's Scheme.Hom.dense_smoothLocus_of_perfectField).

theorem AlgebraicGeometry.Scheme.isRegularAt_genericPoint {k : Type u} [Field k] {X : Scheme} [PerfectField k] [IsIntegral X] (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] : X.IsRegularAt (genericPoint ↥X)

For X integral and locally of finite type over a perfect field, the generic point is a regular point (Mathlib's Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField).

theorem AlgebraicGeometry.Scheme.singIdeal_eq_vanishingIdeal_closure_singularLocus (X : Scheme) : X.singIdeal = IdealSheafData.vanishingIdeal { carrier := closure X.singularLocus, isClosed' := ⋯ }

The defining equation of singIdeal X.

theorem AlgebraicGeometry.Scheme.coe_support_singIdeal (X : Scheme) : ↑X.singIdeal.support = closure X.singularLocus

The support of singIdeal X is the closure of Sing X.

theorem AlgebraicGeometry.Scheme.coe_support_singIdeal_eq_singularLocus {k : Type u} [Field k] {X : Scheme} [PerfectField k] (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] : ↑X.singIdeal.support = X.singularLocus

For X locally of finite type over a perfect field, the support of singIdeal X is Sing X itself: V(𝒥) = Sing X.

theorem AlgebraicGeometry.Scheme.radical_singIdeal (X : Scheme) : X.singIdeal.radical = X.singIdeal

singIdeal X is a radical ideal sheaf (the reduced structure on the singular locus): the vanishing ideal sheaf of the support of any ideal sheaf is its radical (Mathlib's vanishingIdeal_support), and the support of singIdeal X is the closed set it vanishes on.

theorem AlgebraicGeometry.Scheme.singIdeal_eq_top_iff_isRegular (X : Scheme) : X.singIdeal = ⊤ ↔ IsRegular X

singIdeal X is the unit ideal sheaf iff X is regular (the singular locus is empty).