Descent of regularity along flat local homomorphisms

A ring faithfully flat in a regular local ring is regular local. Neither locality nor Noetherianity of the source is necessary: both descend by faithful flatness. The projective dimension of the source residue field is then bounded by the dimension of the target, so Serre's criterion proves regularity.

In particular, regularity descends along any flat local homomorphism (TauCeti.IsRegularLocalRing.of_flat_of_isLocalHom). The closed fibre need not be a field or be regular. This is the local input for descent of regularity of schemes along faithfully flat covers.

Globally, a ring faithfully flat in a regular ring is a regular ring (TauCeti.IsRegularRing.of_faithfullyFlat), by passing to localizations at primes and a prime of the target above each.

References

• H. Matsumura, Commutative Ring Theory, Theorem 23.7 (i).
• TauCeti.IsRegularRing.projectiveDimension_le_ringKrullDim_of_faithfullyFlat and TauCeti.isRegularLocalRing_iff_projectiveDimension_ne_top supply the homological criteria.

theorem TauCeti.IsRegularLocalRing.of_faithfullyFlat {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [IsRegularLocalRing S] [Module.FaithfullyFlat R S] : IsRegularLocalRing R

A ring faithfully flat in a regular local ring is regular local. Locality and Noetherianity of the source follow from faithful flatness, rather than being hypotheses.

theorem TauCeti.IsRegularLocalRing.of_flat_of_isLocalHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsRegularLocalRing S] [Module.Flat R S] [IsLocalHom (algebraMap R S)] : IsRegularLocalRing R

Regularity descends along a flat local homomorphism, without a hypothesis on the closed fibre or a Noetherianity assumption on the source.

theorem TauCeti.IsRegularRing.of_faithfullyFlat {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [IsRegularRing S] [Module.FaithfullyFlat R S] : IsRegularRing R

Regularity descends along faithfully flat extensions by regular rings. If a regular ring S is faithfully flat over a ring R, then R is a regular ring (in particular Noetherian).