Regularity ascends along flat unramified local homomorphisms

Let R → S be a flat homomorphism of Noetherian local rings under which the maximal ideal of R generates the maximal ideal of S. If R is regular, so is S: the images of dim R generators of 𝔪_R generate 𝔪_S, and flatness gives going down, hence dim R ≤ dim S. This is the special case, with a field as closed fibre, of the ascent of regularity along flat local homomorphisms with regular closed fibre.

Formally unramified local homomorphisms essentially of finite type satisfy the hypothesis on the maximal ideals, so regularity ascends along local homomorphisms of this kind which are flat, such as the localizations of étale algebras at primes. This is the local input for showing that an algebra smooth over a regular ring is regular.

Main declarations

• TauCeti.IsRegularLocalRing.of_flat_of_map_maximalIdeal_eq: regularity ascends along a flat homomorphism of Noetherian local rings with 𝔪_R S = 𝔪_S;
• TauCeti.IsRegularLocalRing.of_flat_of_formallyUnramified: the same for a flat, formally unramified local homomorphism essentially of finite type.

References

• H. Matsumura, Commutative Ring Theory, Theorem 23.7.

theorem TauCeti.IsRegularLocalRing.of_flat_of_map_maximalIdeal_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsRegularLocalRing R] [IsLocalRing S] [IsNoetherianRing S] [Module.Flat R S] (h : Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) = IsLocalRing.maximalIdeal S) : IsRegularLocalRing S

Regularity ascends along a flat homomorphism of Noetherian local rings under which the maximal ideal of the source generates the maximal ideal of the target.

theorem TauCeti.IsRegularLocalRing.of_flat_of_formallyUnramified {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsRegularLocalRing R] [IsLocalRing S] [IsNoetherianRing S] [IsLocalHom (algebraMap R S)] [Module.Flat R S] [Algebra.EssFiniteType R S] [Algebra.FormallyUnramified R S] : IsRegularLocalRing S

Regularity ascends along a flat, formally unramified local homomorphism essentially of finite type between Noetherian local rings.