Regular equals smooth over a perfect field

The scheme form of [TSPA, Tag 00TV] with [TSPA, Tag 00TT] (see also [TSPA, Tag 038X]): for X locally of finite type over a perfect field k, the smooth locus of X → Spec k is exactly the set of regular points, and X → Spec k is smooth iff X is regular. Smooth implies regular is Scheme.isRegularAt_of_mem_smoothLocus (SchemeForms.lean); regular implies smooth reduces, through an affine open neighbourhood U of the point and the affine forms of Regular.lean and SmoothAt.lean (x ∈ f.smoothLocus iff Γ(X, U) is smooth at the prime of x; X regular at x iff that localization is a regular local ring), to the affine statement Algebra.IsSmoothAt.of_isRegularLocalRing_of_perfectField. The global statement is the pointwise one with Mathlib's Scheme.Hom.smoothLocus_eq_top_iff (finite type over the Noetherian Spec k is finite presentation); see also SingularLocus.lean.

theorem AlgebraicGeometry.Scheme.mem_smoothLocus_iff_isRegularAt {k : Type u} [Field k] {X : Scheme} [PerfectField k] (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] (x : ↥X) : x ∈ Hom.smoothLocus f ↔ X.IsRegularAt x

For X locally of finite type over a perfect field k, a point lies in the smooth locus of X → Spec k iff it is a regular point ([TSPA, Tag 00TV] with [TSPA, Tag 00TT]; see also [TSPA, Tag 038X]).

theorem AlgebraicGeometry.Scheme.smooth_iff_isRegular {k : Type u} [Field k] {X : Scheme} [PerfectField k] (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] : Smooth f ↔ IsRegular X

Over a perfect field k, X → Spec k locally of finite type is smooth iff X is regular.