Smooth at a prime implies regular

The last assertion of [TSPA, Tag 00TT], "in this case the local ring S_𝔮 is regular", for a finite type algebra S over any field k. The argument is the Jacobian one, assembled from [TSPA, Tags 00T6, 00RX, 00RU, 00NQ]; the numbered steps below are followed by the Lean proof.

The presentation. By Mathlib's Algebra.IsSmoothAt.exists_notMem_isStandardSmooth, smoothness at 𝔮 gives a g ∉ 𝔮 with S_g standard smooth over k ([TSPA, Tags 00TA, 00T7]; finite type over a field is finite presentation); since S_𝔮 ≅ (S_g)_{𝔮 S_g} and regularity is invariant under ring isomorphism, we may assume S itself standard smooth: S ≅ A/(f_1, …, f_c) with A = k[x_1, …, x_N] and the Jacobian minor Δ = det(∂f_j/∂x_{m(i)}) a unit of S (Mathlib's SubmersivePresentation, whose map : σ → ι picks the c distinguished variables). For such S, Ω[S⁄k] is free of rank N - c ([TSPA, Tag 00T7, (2)]; rank_kaehlerDifferential), so κ(𝔮) ⊗[S] Ω[S⁄k] has dimension N - c at every prime.

The Jacobian argument. (1) Let Q ⊆ A be the preimage of 𝔮 and P = A_Q, a regular local ring (Hironaka/Algebra/RegularSmooth/Polynomial.lean). (2) The localized surjection φ : P → S_𝔮 has kernel (f_1, …, f_c)P, so S_𝔮 ≅ P/(f_1, …, f_c). (3) In the basis 1 ⊗ d x_i of κ ⊗[P] Ω[P⁄k] the vector 1 ⊗ d f_j has coordinates ∂f_j/∂x_i mod Q, and the c × c minor on the distinguished variables is Δ mod Q ≠ 0 (a unit of S does not lie in 𝔮), so the 1 ⊗ d f_j are linearly independent over κ. (4) The conormal map 𝔪_P/𝔪_P² → κ ⊗ Ω[P⁄k] sends the class of f_j to 1 ⊗ d f_j, so the classes of the f_j are linearly independent in 𝔪_P/𝔪_P² (no injectivity of the conormal map is used, only that it is a well-defined linear map). (5) By [TSPA, Tag 00NQ] (Hironaka/Algebra/RegularSmooth/QuotientRegular.lean), P/(f_1, …, f_c) is a regular local ring, and so is S_𝔮.

theorem Algebra.IsSmoothAt.exists_notMem_isStandardSmooth_of_finiteType {k : Type u} [Field k] {S : Type u} [CommRing S] [Algebra k S] [FiniteType k S] (𝔮 : Ideal S) [𝔮.IsPrime] [IsSmoothAt k 𝔮] : ∃ g ∉ 𝔮, IsStandardSmooth k (Localization.Away g)

If the finite type k-algebra S is smooth at 𝔮 over k, there is g ∉ 𝔮 with S_g standard smooth over k (the first sentence of the proof of (1) ⇒ (3) in [TSPA, Tag 00TT]; [TSPA, Tag 00TA]). Mathlib's statement for finitely presented algebras, with finite type over a field giving finite presentation.

theorem Algebra.IsStandardSmoothOfRelativeDimension.finrank_residueField_tensor_kaehlerDifferential {k : Type u} [Field k] {S : Type u} [CommRing S] [Algebra k S] (d : ℕ) [IsStandardSmoothOfRelativeDimension d k S] (𝔮 : Ideal S) [𝔮.IsPrime] : Module.finrank 𝔮.ResidueField (TensorProduct S 𝔮.ResidueField Ω[S⁄k]) = d

For S standard smooth of relative dimension d over k, Ω[S⁄k] is free of rank d, so κ(𝔮) ⊗[S] Ω[S⁄k] has dimension d at every prime 𝔮 ([TSPA, Tag 00T7, (2)]; [TSPA, Tag 02G1]).

theorem Algebra.IsStandardSmooth.isRegularLocalRing_localization_atPrime {k : Type u} [Field k] {S : Type u} [CommRing S] [Algebra k S] [IsStandardSmooth k S] (𝔮 : Ideal S) [𝔮.IsPrime] : IsRegularLocalRing (Localization.AtPrime 𝔮)

If S is standard smooth over the field k, then S_𝔮 is a regular local ring at every prime 𝔮: the Jacobian argument, steps (1)–(5) of the module docstring.

theorem Algebra.IsSmoothAt.isRegularLocalRing {k : Type u} [Field k] {S : Type u} [CommRing S] [Algebra k S] [FiniteType k S] (𝔮 : Ideal S) [𝔮.IsPrime] [IsSmoothAt k 𝔮] : IsRegularLocalRing (Localization.AtPrime 𝔮)

If the finite type k-algebra S is smooth at 𝔮 over k, then S_𝔮 is a regular local ring, for any field k (the last sentence of [TSPA, Tag 00TT], assembled from Sta, Tags 00T6, 00RX, 00RU, 00NQ). Standard smoothness of some S_g with g ∉ 𝔮, then the Jacobian argument on S_g, whose localization at 𝔮 S_g is S_𝔮.