def Scheme.IsSmoothAtPoint (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian X] (x : ↥X) : Prop

A locally Noetherian scheme X is smooth at a point x if the local ring O_{X,x} is a regular local ring.

def Scheme.IsSingularAtPoint (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian X] (x : ↥X) : Prop

X is singular at x if it is not smooth at x.

def Scheme.IsSmooth (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian X] : Prop

X is smooth if it is smooth at every point.

theorem Scheme.isSmoothAtPoint_iff_isRegularLocalRing {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (x : ↥X) : IsSmoothAtPoint X x ↔ IsRegularLocalRing ↑(X.presheaf.stalk x)

Smoothness at x is by definition regularity of the local ring O_{X,x}.

theorem Scheme.isSmoothAtPoint_iff_spanFinrank {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (x : ↥X) [IsLocalRing ↑(X.presheaf.stalk x)] [IsNoetherianRing ↑(X.presheaf.stalk x)] : IsSmoothAtPoint X x ↔ ↑(Submodule.spanFinrank (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x))) = ringKrullDim ↑(X.presheaf.stalk x)

Smoothness criterion via the minimal number of generators of the maximal ideal: X is smooth at x iff spanFinrank(𝔪_x) = dim O_{X,x}.

theorem Scheme.isSmoothAtPoint_iff_finrank_cotangentSpace {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (x : ↥X) [IsLocalRing ↑(X.presheaf.stalk x)] [IsNoetherianRing ↑(X.presheaf.stalk x)] : IsSmoothAtPoint X x ↔ ↑(Module.finrank (IsLocalRing.ResidueField ↑(X.presheaf.stalk x)) (IsLocalRing.CotangentSpace ↑(X.presheaf.stalk x))) = ringKrullDim ↑(X.presheaf.stalk x)

Smoothness via the cotangent space: X is smooth at x iff dim_κ(𝔪_x/𝔪_x²) = dim O_{X,x}. This is the classical "Zariski tangent space of expected dimension" criterion.