Localization of Regular Local Ring is Regular

In this file, we establish the full version of Auslander-Buchsbaum-Serre criterion and its corollary that localization of regular local ring is regular.

theorem Auslander_Buchsbaum_Serre (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] : IsRegularLocalRing R ↔ globalDimension R < ⊤

theorem isRegularLocalRing_localization (R : Type u) [CommRing R] [IsRegularLocalRing R] (p : Ideal R) [p.IsPrime] : IsRegularLocalRing (Localization.AtPrime p)

theorem IsRegularLocalRing.of_isLocalization (R : Type u) [CommRing R] [IsRegularLocalRing R] (p : Ideal R) [p.IsPrime] (S : Type u_1) [CommRing S] [Algebra R S] [IsLocalization.AtPrime S p] : IsRegularLocalRing S

theorem isRegularRing_of_globalDimension_lt_top (R : Type u) [CommRing R] [IsNoetherianRing R] [Small.{v, u} R] (h : globalDimension R < ⊤) : IsRegularRing R

theorem isRegularRing_of_isRegularLocalRing (R : Type u) [CommRing R] [IsRegularLocalRing R] : IsRegularRing R

theorem isRegularRing_of_localization_maximal_isRegularLocalRing (R : Type u) [CommRing R] [IsNoetherianRing R] (h : ∀ (m : Ideal R) (x : m.IsMaximal), IsRegularLocalRing (Localization.AtPrime m)) : IsRegularRing R