Nagata rings

A commutative ring R is Nagata if it is Noetherian and R ⧸ p is a Japanese domain for every prime ideal p of R (Stacks, Definition 10.162.1 (032R)). Nagata rings are the rings over which normalization is well behaved: the normalization of an integral scheme whose affine opens have Nagata section rings, in a finite extension of its function field, is finite (Stacks, Lemma 29.54.14 (0AVK)). Quasi-excellent rings, for instance complete Noetherian local rings and algebras of finite type over a field or over ℤ, are Nagata (Stacks, Lemma 15.53.5 (07QV)); this file develops the definition and its elementary permanence properties and examples.

Main definitions and results

• TauCeti.Ring.IsNagata R: the ring R is Nagata.
• TauCeti.Ring.IsNagata.of_finite: a finite algebra over a Nagata ring is Nagata (Stacks, Lemma 10.162.5 (032T)). In particular quotients of Nagata rings are Nagata (TauCeti.Ring.IsNagata.quotient), and being Nagata is invariant under ring isomorphisms.
• TauCeti.Ring.IsNagata.of_isLocalization: a localization of a Nagata ring is Nagata (Stacks, Lemma 10.162.6 (032U)).
• TauCeti.Ring.isNagata_iff_of_span_eq_top: being Nagata is local on Spec R: for elements f_i generating the unit ideal, R is Nagata if and only if every R_{f_i} is (Stacks, Lemma 10.162.7 (032V)). This is what makes the Nagata property of a scheme, asked of the section rings of its affine opens, checkable on an affine open cover.
• TauCeti.Ring.IsNagata.isJapanese: a Nagata domain is Japanese.
• TauCeti.Ring.IsNagata.finite_integralClosure: for a Nagata ring R and a reduced R-algebra S essentially of finite type, the integral closure of R in S is a finite R-module (Stacks, Lemma 10.162.2 (03GH)). The ring S embeds in the product of the fraction fields of its quotients by its finitely many minimal primes q, each a finitely generated field extension of the fraction field of the Japanese domain R ⧸ (q ∩ R).
• TauCeti.Ring.IsNagata.of_krullDimLE_zero: a Noetherian ring of Krull dimension zero, such as a field or an Artinian ring, is Nagata.
• TauCeti.Ring.isNagata_iff_isJapanese: a Noetherian domain of Krull dimension at most one is Nagata if and only if it is Japanese (Stacks, Example 10.162.17 (09E1) for discrete valuation rings). Hence ℤ, and every Dedekind domain whose fraction field is perfect, is Nagata.

Implementation notes

The rules producing IsNagata from IsNoetherianRing and dimension hypotheses are theorems rather than instances: as IsNagata extends IsNoetherianRing, such instances would make every search for IsNoetherianRing or IsJapanese cycle through IsNagata. Fields are the exception, with their own instance.

References

• Stacks Project, Section 10.162 (032E)

class TauCeti.Ring.IsNagata (R : Type u) [CommRing R] extends IsNoetherian R R : Prop

A commutative ring R is Nagata if it is Noetherian and the quotient R ⧸ p by every prime ideal p is a Japanese domain. Stacks, Definition 10.162.1 (032R).

• noetherian (s : Submodule R R) : s.FG
• isJapanese_quotient (p : Ideal R) [p.IsPrime] : IsJapanese (R ⧸ p)

theorem TauCeti.Ring.IsNagata.of_finite (R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S] [Module.Finite R S] [IsNagata R] : IsNagata S

A finite algebra over a Nagata ring is Nagata. Stacks, Lemma 10.162.5 (032T).

instance TauCeti.Ring.IsNagata.quotient {R : Type u} [CommRing R] [IsNagata R] (I : Ideal R) : IsNagata (R ⧸ I)

A quotient of a Nagata ring is Nagata.

theorem RingEquiv.isNagata {R : Type u} [CommRing R] {S : Type v} [CommRing S] [TauCeti.Ring.IsNagata R] (e : R ≃+* S) : TauCeti.Ring.IsNagata S

Being Nagata is invariant under ring isomorphisms.

@[instance 100]

instance TauCeti.Ring.IsNagata.isJapanese {R : Type u} [CommRing R] [IsDomain R] [IsNagata R] : IsJapanese R

A Nagata domain is Japanese.

theorem TauCeti.Ring.IsNagata.finite_integralClosure {R : Type u} [CommRing R] [IsNagata R] (S : Type v) [CommRing S] [IsReduced S] [Algebra R S] [Algebra.EssFiniteType R S] : Module.Finite R ↥(integralClosure R S)

Finiteness of integral closures over a Nagata ring. For a Nagata ring R and a reduced R-algebra S essentially of finite type, the integral closure of R in S is a finite R-module. Stacks, Lemma 10.162.2 (03GH).

theorem TauCeti.Ring.IsNagata.of_krullDimLE_zero {R : Type u} [CommRing R] [IsNoetherianRing R] [Ring.KrullDimLE 0 R] : IsNagata R

A Noetherian ring of Krull dimension zero, for instance an Artinian ring or the zero ring, is Nagata.

instance TauCeti.Ring.IsNagata.of_field (k : Type u) [Field k] : IsNagata k

A field is Nagata.

theorem TauCeti.Ring.IsNagata.of_isJapanese {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R] [Ring.KrullDimLE 1 R] [IsJapanese R] : IsNagata R

A Noetherian Japanese domain of Krull dimension at most one is Nagata.

theorem TauCeti.Ring.IsNagata.of_isLocalization {R : Type u} [CommRing R] [IsNagata R] (M : Submonoid R) (S : Type v) [CommRing S] [Algebra R S] [IsLocalization M S] : IsNagata S

A localization of a Nagata ring is Nagata. Stacks, Lemma 10.162.6 (032U).

instance TauCeti.Ring.IsNagata.localization {R : Type u} [CommRing R] [IsNagata R] (M : Submonoid R) : IsNagata (Localization M)

A localization of a Nagata ring is Nagata.

theorem TauCeti.Ring.IsNagata.of_span_eq_top {R : Type u} [CommRing R] {t : Set R} (ht : Ideal.span t = ⊤) (H : ∀ f ∈ t, IsNagata (Localization.Away f)) : IsNagata R

Being Nagata is local on Spec R. If the elements of t generate the unit ideal of R and the localization R_f is Nagata for every f ∈ t, then R is Nagata. Stacks, Lemma 10.162.7 (032V).

theorem TauCeti.Ring.isNagata_iff_of_span_eq_top {R : Type u} [CommRing R] {t : Set R} (ht : Ideal.span t = ⊤) : IsNagata R ↔ ∀ f ∈ t, IsNagata (Localization.Away f)

Being Nagata is local on Spec R. If the elements of t generate the unit ideal of R, then R is Nagata if and only if the localization R_f is Nagata for every f ∈ t. Stacks, Lemmas 10.162.6 (032U) and 10.162.7 (032V).

theorem TauCeti.Ring.isNagata_iff_isJapanese {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R] [Ring.KrullDimLE 1 R] : IsNagata R ↔ IsJapanese R

A Noetherian domain of Krull dimension at most one, for instance a Dedekind domain or a discrete valuation ring, is Nagata if and only if it is Japanese. Stacks, Example 10.162.17 (09E1), for discrete valuation rings.