Regular points of a scheme: basic facts

Hironaka's simple points (X.IsRegularAt x: the stalk 𝒪_{X,x} is a regular local ring), the non-singular schemes (IsRegular X) and the singular locus X.singularLocus [Hir64, Introduction, p. 112; Ch. I, p. 163], in which the main theorems are stated: their unfolding lemmas, and the characterization of IsRegular X as the emptiness of the singular locus. Over a field these notions are compared with Mathlib's smooth locus in Hironaka/Algebra/RegularSmooth/RegularSmoothEquiv.lean: smooth at x implies 𝒪_{X,x} regular [TSPA, Tag 00TT], and the converse holds over a perfect field [TSPA, Tag 00TV].

The affine-local form (the reduction "the question is local" of [TSPA, Tag 038X]): on an affine open U ∋ x, with 𝔮 = hU.primeIdealOf ⟨x, hx⟩ the prime of Γ(X, U) corresponding to x, the stalk 𝒪_{X,x} is the localization Γ(X, U)_𝔮 (IsAffineOpen.isLocalization_stalk), so X is regular at x iff Γ(X, U)_𝔮 is a regular local ring. Regularity of a local ring is invariant under ring isomorphism (IsRegularLocalRing.of_ringEquiv), which is all the proof uses.

theorem AlgebraicGeometry.Scheme.isRegularAt_iff {X : Scheme} {x : ↥X} : X.IsRegularAt x ↔ IsRegularLocalRing ↑(X.presheaf.stalk x)

theorem AlgebraicGeometry.Scheme.mem_singularLocus_iff {X : Scheme} {x : ↥X} : x ∈ X.singularLocus ↔ ¬X.IsRegularAt x

theorem AlgebraicGeometry.Scheme.isRegularAt_iff_isRegularLocalRing_localization {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {x : ↥X} (hx : x ∈ U) : X.IsRegularAt x ↔ IsRegularLocalRing (Localization.AtPrime (hU.primeIdealOf ⟨x, hx⟩).asIdeal)

The affine-local form of regularity at a point: on an affine open U ∋ x with 𝔮 = hU.primeIdealOf ⟨x, hx⟩ the prime of x, X is regular at x iff the localization Γ(X, U)_𝔮 is a regular local ring, because 𝒪_{X,x} ≅ Γ(X, U)_𝔮 (IsAffineOpen.isLocalization_stalk) and regularity is invariant under ring isomorphism.

theorem AlgebraicGeometry.isRegular_iff {X : Scheme} : IsRegular X ↔ ∀ (x : ↥X), X.IsRegularAt x

theorem AlgebraicGeometry.isRegular_iff_singularLocus_eq_empty {X : Scheme} : IsRegular X ↔ X.singularLocus = ∅