def singularLocus {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFinitePresentation f] : Set ↥X

The singular locus of a morphism f : X → Spec K is the complement of the smooth locus, i.e., the set of points where f fails to be smooth.

theorem singularLocus_isClosed {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFinitePresentation f] : IsClosed (singularLocus f)

The singular locus is closed: smoothness is an open condition.

theorem singularLocus_ne_univ {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [PerfectField K] [AlgebraicGeometry.IsReduced X] [Nonempty ↥X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFinitePresentation f] : singularLocus f ≠ Set.univ

Singular locus is not everything for a reduced scheme over a perfect field: a non-empty reduced scheme of finite presentation has a non-empty smooth locus, so its singular locus is a proper subset. This is generic smoothness in the perfect-field case.

def singularLocusAlg (K : Type u_2) [Field K] (A : Type u_3) [CommRing A] [Algebra K A] : Set (PrimeSpectrum A)

Algebraic version of singularLocus: for a K-algebra A, the singular locus is the complement of the smooth locus inside Spec A.

theorem singularLocusAlg_isClosed {K : Type u} [Field K] {A : Type u_1} [CommRing A] [Algebra K A] [Algebra.FinitePresentation K A] : IsClosed (singularLocusAlg K A)

The algebraic singular locus is closed when A is finitely presented over K.