Smooth algebras over regular rings are regular

Let R be a regular ring and S a finitely presented R-algebra which is smooth at a prime q. Then the local ring S_q is regular. In particular an R-algebra smooth over a regular ring, for instance over a field, is a regular ring.

Near q, some localization S_g is standard smooth over R, so Ω[S_g⁄R] has a basis d a₁, …, d aₙ of differentials of elements of S_g. Sending Xᵢ ↦ aᵢ then makes S_g étale over the polynomial ring P = R[X₁, …, Xₙ], by the Jacobi–Zariski criterion TauCeti.formallyEtale_of_bijective_mapBaseChange. The polynomial ring over a regular ring is regular (Mathlib's MvPolynomial.isRegularRing_of_isRegularRing), and the localization of an étale algebra at a prime is flat and unramified over the corresponding localization of P, so regularity ascends by TauCeti.IsRegularLocalRing.of_flat_of_formallyUnramified.

Main declarations

• TauCeti.isRegularLocalRing_localization_of_isSmoothAt: the localization of a finitely presented algebra over a regular ring at a prime where it is smooth is a regular local ring;
• TauCeti.IsRegularRing.of_smooth: a smooth algebra over a regular ring is a regular ring.

References

• H. Matsumura, Commutative Ring Theory, Theorem 23.7, for the ascent of regularity along the flat local homomorphism P_p → S_q.

theorem TauCeti.isRegularLocalRing_localization_of_isSmoothAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsRegularRing R] [Algebra.FinitePresentation R S] (q : Ideal S) [q.IsPrime] [Algebra.IsSmoothAt R q] : IsRegularLocalRing (Localization.AtPrime q)

Let R be a regular ring and S a finitely presented R-algebra which is smooth at the prime q. Then the local ring S_q is regular.

theorem TauCeti.IsRegularRing.of_smooth {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsRegularRing R] [Algebra.Smooth R S] : IsRegularRing S

A smooth algebra over a regular ring is a regular ring.