The regular locus of a commutative ring

The regular locus of a commutative ring R is the set of primes p of R whose localization R_p is a regular local ring (Stacks, Section 15.48, opening paragraph). It is defined for every commutative ring, with no Noetherian hypothesis, and it need not be open: openness for all finite type algebras is the J-2 condition of Stacks, Definition 15.48.1 (07P7).

Main definitions and results

• TauCeti.Excellence.regularLocus R: the primes p of R with R_p a regular local ring.
• TauCeti.Excellence.mem_regularLocus_iff_of_isLocalization: membership can be tested on any localization of R at the prime, not only on Localization.AtPrime.
• TauCeti.Excellence.regularLocus_eq_univ: a regular ring is regular at every prime, and TauCeti.Excellence.regularLocus_eq_univ_iff: conversely, a Noetherian ring regular at every prime is a regular ring.
• TauCeti.Excellence.algebraMap_eq_zero_of_mem_regularLocus_of_isNilpotent: a nilpotent element of R vanishes in every localization at a prime of the regular locus.
• TauCeti.Excellence.regularLocus_ringEquiv: a ring isomorphism R ≃+* S identifies the regular loci through the induced homeomorphism of prime spectra.
• TauCeti.Excellence.regularLocus_eq_empty_of_subsingleton: the zero ring has empty regular locus, as its spectrum is empty.
• TauCeti.Excellence.regularLocus_trivSqZeroExt_eq_empty: the dual numbers k[ε]/(ε²) over a commutative ring k have empty regular locus, since a regular local ring is a domain.

References

• Stacks Project, Section 15.48.
• Ported from T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit a39c3781b9850b9f3d5cbc9920322a3b8e365ef2 (Apache-2.0), lean/Pcf/Bounding/FiniteTypeRegularLocus.lean: regularLocus and regularLocus_eq_univ are its Pcf.primeRegularLocus and Pcf.primeRegularLocus_eq_univ, and regularLocus_ringEquiv follows the comap-preimage form of its Pcf.preimage_primeRegularLocus_of_isLocalization together with its Pcf.isRegularLocalRing_iff_of_ringEquiv. New here, with no source in that project: mem_regularLocus_iff_of_isLocalization, regularLocus_eq_univ_iff, algebraMap_eq_zero_of_mem_regularLocus_of_isNilpotent, the empty-locus results and the examples.

def TauCeti.Excellence.regularLocus (R : Type u_1) [CommRing R] : Set (PrimeSpectrum R)

The regular locus of R: the primes p such that R_p is a regular local ring. It need not be open. Stacks, Section 15.48.

@[simp]

theorem TauCeti.Excellence.mem_regularLocus {R : Type u_1} [CommRing R] {p : PrimeSpectrum R} : p ∈ regularLocus R ↔ IsRegularLocalRing (Localization.AtPrime p.asIdeal)

theorem TauCeti.Excellence.mem_regularLocus_iff_of_isLocalization {R : Type u_1} [CommRing R] {p : PrimeSpectrum R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization.AtPrime S p.asIdeal] : p ∈ regularLocus R ↔ IsRegularLocalRing S

A prime p lies in the regular locus exactly when some, equivalently every, localization S of R at p is a regular local ring.

theorem TauCeti.Excellence.regularLocus_eq_univ (R : Type u_1) [CommRing R] [IsRegularRing R] : regularLocus R = Set.univ

Every prime of a regular ring lies in its regular locus.

theorem TauCeti.Excellence.regularLocus_eq_univ_iff (R : Type u_1) [CommRing R] [IsNoetherianRing R] : regularLocus R = Set.univ ↔ IsRegularRing R

A Noetherian ring is a regular ring exactly when its regular locus is everything.

theorem TauCeti.Excellence.regularLocus_ringEquiv {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (e : R ≃+* S) : PrimeSpectrum.comap ↑e ⁻¹' regularLocus R = regularLocus S

A ring isomorphism e : R ≃+* S identifies the regular loci: a prime p of S is in the regular locus of S exactly when its contraction to R is in the regular locus of R.

theorem TauCeti.Excellence.algebraMap_eq_zero_of_mem_regularLocus_of_isNilpotent {R : Type u_1} [CommRing R] {p : PrimeSpectrum R} (hp : p ∈ regularLocus R) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization.AtPrime S p.asIdeal] {a : R} (ha : IsNilpotent a) : (algebraMap R S) a = 0

A nilpotent element of R vanishes in every localization S of R at a prime of the regular locus, since a regular local ring is a domain.

theorem TauCeti.Excellence.regularLocus_eq_empty_of_subsingleton (R : Type u_1) [CommRing R] [Subsingleton R] : regularLocus R = ∅

The zero ring has empty regular locus, as it has no primes.

theorem TauCeti.Excellence.regularLocus_trivSqZeroExt_eq_empty (k : Type u_2) [CommRing k] : regularLocus (TrivSqZeroExt k k) = ∅

The dual numbers k[ε]/(ε²) over a commutative ring k have empty regular locus: in every localization at a prime, ε is a nonzero element with ε² = 0, whereas nilpotents vanish in the localizations at primes of the regular locus.