N-1 and Japanese domains

A domain R with fraction field K is N-1 if its integral closure in K is a finite R-module, and Japanese (or N-2) if its integral closure in every finite extension L of K is a finite R-module, inseparable extensions included (Stacks, Definition 10.161.1 (032F)). These finiteness conditions are the input of finite normalization: they are what makes the normalization of an integral scheme in a finite extension of its function field a finite morphism, and Nagata rings, the Noetherian rings all of whose prime quotients are Japanese, are defined from them.

For a Noetherian integrally closed domain, finiteness of the integral closure in a separable extension is classical (Mathlib's IsIntegralClosure.finite, by the trace form). Inseparable extensions are where Japanese rings differ from N-1 rings; when the fraction field is perfect, as in characteristic zero, there are none, and the two notions agree for Noetherian domains. In general a finite extension sits inside a normal one, which is separable over a purely inseparable extension of the fraction field, so for Noetherian domains only the purely inseparable extensions need to be tested.

Main definitions and results

• TauCeti.Ring.IsN1 R: the domain R is N-1.
• TauCeti.Ring.IsJapanese R: the domain R is Japanese (N-2).
• TauCeti.Ring.IsJapanese.finite_integralClosure: the defining property of a Japanese ring for an arbitrary model K of its fraction field and a finitely generated, possibly transcendental, field extension L of K in any universe.
• TauCeti.Ring.IsN1.of_isIntegrallyClosed: an integrally closed ring is N-1.
• TauCeti.Ring.IsJapanese.of_field: a field is Japanese.
• TauCeti.Ring.IsJapanese.of_isIntegrallyClosed: a Noetherian integrally closed domain with perfect fraction field (for instance of characteristic zero, such as ℤ or the ring of integers of a number field) is Japanese.
• TauCeti.Ring.IsJapanese.of_finite: a domain that is a finite extension of a Japanese domain is Japanese (Stacks, Lemma 10.161.5 (032I), finite case); in particular being Japanese is invariant under ring isomorphisms (RingEquiv.isJapanese).
• TauCeti.Ring.isN1_of_isLocalization, TauCeti.Ring.isJapanese_of_isLocalization: a localization of an N-1, respectively Japanese, domain is N-1, respectively Japanese (Stacks, Lemma 10.161.3 (032G)).
• TauCeti.Ring.IsN1.exists_isIntegrallyClosed_localization_away: an N-1 domain becomes integrally closed after inverting a single nonzero element, so the normal locus of its spectrum contains a nonempty open.
• TauCeti.Ring.isN1_iff_exists_isIntegrallyClosed_localization_away_and_isN1_localization_atPrime: the N-1 local criterion, a Noetherian domain is N-1 if and only if it becomes integrally closed after inverting a single nonzero element and its localizations at maximal ideals are N-1 (Stacks, Lemma 10.161.15 (0333)). The substantive direction is TauCeti.Ring.IsN1.of_isIntegrallyClosed_localization_away_of_isN1_localization_atPrime.
• TauCeti.Ring.IsN1.of_span_eq_top, TauCeti.Ring.IsJapanese.of_span_eq_top: being N-1, respectively Japanese, is local on Spec R: a domain is N-1, respectively Japanese, as soon as its localizations R_{f_i} are, for elements f_i generating the unit ideal (Stacks, Lemma 10.161.6 (032J)).
• TauCeti.Ring.finite_integralClosure_of_isSeparable: for a Noetherian domain whose integral closure in a finite extension M of the fraction field is finite, the integral closure in every finite separable extension of M is finite (Stacks, Lemma 10.161.8 (032L), applied to the normalization); for M the fraction field this covers every Noetherian N-1 domain.
• TauCeti.Ring.finite_integralClosure_of_etale: the integral closure of a Noetherian N-1 domain in a finite étale algebra over its fraction field, a finite product of finite separable extensions, is finite.
• TauCeti.Ring.isJapanese_iff_isN1: a Noetherian domain with perfect fraction field is Japanese if and only if it is N-1 (Stacks, Lemma 10.161.11 (032M), in characteristic zero).
• TauCeti.Ring.isJapanese_iff_isPurelyInseparable: a Noetherian domain is Japanese if and only if its integral closure in every finite purely inseparable extension of the fraction field is finite (Stacks, Lemma 10.161.12 (032N)); TauCeti.Ring.IsJapanese.of_isPurelyInseparable is the criterion for an arbitrary model of the fraction field.

Implementation notes

As in Stacks, the definition of IsJapanese R quantifies over the finite extensions L of FractionRing R lying in the universe of R. Every finite extension of a fraction field of R is isomorphic to one of these, so IsJapanese.finite_integralClosure gives the property for every fraction field and every universe.

References

• Stacks Project, Section 10.161 (0BI1)
• The proof of TauCeti.Ring.finite_integralClosure_of_etale through the field factors follows T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit 9a20b3f351446d64e6015d704198bc71c7002008 (Apache-2.0), lean/Pcf/Stacks/Purity/FiniteNormalModel.lean, where the base is integrally closed (finiteEtaleAlgebra_integralClosure_finite).

class TauCeti.Ring.IsN1 (R : Type u) [CommRing R] : Prop

A commutative ring R is N-1 if its integral closure in its total ring of fractions FractionRing R is a finite R-module. Stacks, Definition 10.161.1 (032F), where R is a domain and FractionRing R its fraction field. See IsN1.finite_integralClosure for an arbitrary model of the fraction field.

• finite_integralClosure_fractionRing : Module.Finite R ↥(integralClosure R (FractionRing R))

class TauCeti.Ring.IsJapanese (R : Type u) [CommRing R] [IsDomain R] : Prop

A domain R is Japanese (or N-2) if for every finite extension L of its fraction field, the integral closure of R in L is a finite R-module; inseparable extensions are included. Stacks, Definition 10.161.1 (032F). See IsJapanese.finite_integralClosure for an arbitrary model of the fraction field and an extension in an arbitrary universe.

• finite_integralClosure_fractionRing (L : Type u) [Field L] [Algebra R L] [Algebra (FractionRing R) L] [IsScalarTower R (FractionRing R) L] [FiniteDimensional (FractionRing R) L] : Module.Finite R ↥(integralClosure R L)

instance TauCeti.Ring.IsN1.finite_integralClosure {R : Type u} [CommRing R] [IsN1 R] (K : Type v) [CommRing K] [Algebra R K] [IsFractionRing R K] : Module.Finite R ↥(integralClosure R K)

The integral closure of an N-1 ring in any model of its total ring of fractions is finite.

theorem TauCeti.Ring.IsN1.of_finite_integralClosure {R : Type u} [CommRing R] (K : Type v) [CommRing K] [Algebra R K] [IsFractionRing R K] [Module.Finite R ↥(integralClosure R K)] : IsN1 R

A ring whose integral closure in some model of its total ring of fractions is finite is N-1.

instance TauCeti.Ring.IsN1.of_isIntegrallyClosed {R : Type u} [CommRing R] [IsIntegrallyClosed R] : IsN1 R

An integrally closed ring is N-1: its integral closure in its total ring of fractions is R itself.

theorem TauCeti.Ring.IsJapanese.finite_integralClosure {R : Type u} [CommRing R] [IsDomain R] [IsJapanese R] (K : Type v) (L : Type w) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra.EssFiniteType K L] : Module.Finite R ↥(integralClosure R L)

The defining property of a Japanese domain R, for an arbitrary model K of the fraction field and a finitely generated field extension L of K, transcendental or not, in an arbitrary universe: the integral closure of R in L is a finite R-module.

theorem TauCeti.Ring.IsJapanese.of_finite_integralClosure {R : Type u} [CommRing R] [IsDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (h : ∀ (L : Type u) [inst : Field L] [inst_1 : Algebra K L] [inst_2 : Algebra R L] [IsScalarTower R K L] [FiniteDimensional K L], Module.Finite R ↥(integralClosure R L)) : IsJapanese R

A domain R is Japanese as soon as its integral closure in every finite extension of some model K of its fraction field, in the universe of R, is a finite R-module.

instance TauCeti.Ring.IsJapanese.isN1 {R : Type u} [CommRing R] [IsDomain R] [IsJapanese R] : IsN1 R

A Japanese domain is N-1.

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

A field is Japanese: its integral closure in a finite extension is the whole extension, which is finite-dimensional.

instance TauCeti.Ring.IsJapanese.of_isIntegrallyClosed {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R] [PerfectField (FractionRing R)] : IsJapanese R

A Noetherian integrally closed domain whose fraction field is perfect is Japanese. This covers every Noetherian integrally closed domain of characteristic zero, for instance ℤ, and Dedekind domains of characteristic zero: over a perfect field every finite extension is separable, and the integral closure in a finite separable extension is finite by the trace form.

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

A domain S that is a finite extension of a Japanese domain R is Japanese, with no Noetherian hypothesis. Stacks, Lemma 10.161.5 (032I), for finite extensions.

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

Being Japanese is invariant under ring isomorphisms.

theorem TauCeti.Ring.finite_integralClosure_of_isSeparable {R : Type u} [CommRing R] [IsNoetherianRing R] (K : Type u_1) (M : Type u_2) (E : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] [Field M] [Algebra K M] [Algebra R M] [IsScalarTower R K M] [FiniteDimensional K M] [Module.Finite R ↥(integralClosure R M)] [Field E] [Algebra M E] [Algebra R E] [IsScalarTower R M E] [FiniteDimensional M E] [Algebra.IsSeparable M E] : Module.Finite R ↥(integralClosure R E)

Finiteness of the integral closure in a separable extension. Let R be a Noetherian domain with fraction field K, let M be a finite extension of K in which the integral closure of R is a finite R-module, and let E be a finite separable extension of M. Then the integral closure of R in E is a finite R-module. For M = K this says that the integral closure of a Noetherian N-1 domain in a finite separable extension of its fraction field is finite. Stacks, Lemma 10.161.8 (032L) for normal R, applied to the integral closure of R in M.

theorem TauCeti.Ring.finite_integralClosure_of_etale {R : Type u} [CommRing R] [IsNoetherianRing R] [IsN1 R] (K : Type u_1) (L : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [CommRing L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra.Etale K L] : Module.Finite R ↥(integralClosure R L)

Finiteness of the integral closure in a finite étale algebra. Let R be a Noetherian N-1 domain with fraction field K, for instance an integrally closed Noetherian domain. Then the integral closure of R in a finite étale K-algebra L, that is, in a finite product of finite separable extensions of K, is a finite R-module.

theorem TauCeti.Ring.isJapanese_iff_isN1 {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R] [PerfectField (FractionRing R)] : IsJapanese R ↔ IsN1 R

A Noetherian domain whose fraction field is perfect, for instance of characteristic zero, is Japanese if and only if it is N-1. Stacks, Lemma 10.161.11 (032M), stated there in characteristic zero.

theorem TauCeti.Ring.IsJapanese.of_isPurelyInseparable {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (h : ∀ (M : Type u) [inst : Field M] [inst_1 : Algebra K M] [inst_2 : Algebra R M] [IsScalarTower R K M] [FiniteDimensional K M] [IsPurelyInseparable K M], Module.Finite R ↥(integralClosure R M)) : IsJapanese R

Testing the Japanese property on purely inseparable extensions. A Noetherian domain R with fraction field K is Japanese as soon as its integral closure in every finite purely inseparable extension of K is a finite R-module. Stacks, Lemma 10.161.12 (032N), where K has characteristic p > 0; no hypothesis on the characteristic is needed.

theorem TauCeti.Ring.isJapanese_iff_isPurelyInseparable {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R] : IsJapanese R ↔ ∀ (L : Type u) [inst : Field L] [inst_1 : Algebra R L] [inst_2 : Algebra (FractionRing R) L] [IsScalarTower R (FractionRing R) L] [FiniteDimensional (FractionRing R) L] [IsPurelyInseparable (FractionRing R) L], Module.Finite R ↥(integralClosure R L)

A Noetherian domain is Japanese if and only if its integral closure in every finite purely inseparable extension of its fraction field is a finite module. Stacks, Lemma 10.161.12 (032N), with no hypothesis on the characteristic. When the fraction field is perfect its only finite purely inseparable extension is itself, and the condition reduces to N-1, as in isJapanese_iff_isN1.

theorem TauCeti.Ring.isN1_of_isLocalization {R : Type u} [CommRing R] [IsDomain R] [IsN1 R] (M : Submonoid R) (S : Type u_1) [CommRing S] [Algebra R S] [IsLocalization M S] : IsN1 S

A localization of an N-1 domain is N-1. Stacks, Lemma 10.161.3 (032G).

theorem TauCeti.Ring.isJapanese_of_isLocalization {R : Type u} [CommRing R] [IsDomain R] [IsJapanese R] (M : Submonoid R) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra R S] [IsLocalization M S] : IsJapanese S

A localization of a Japanese domain is Japanese. Stacks, Lemma 10.161.3 (032G).

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

Being N-1 is local on Spec R. If the elements of t generate the unit ideal of a domain R and the localization R_f is N-1 for every nonzero f ∈ t, then R is N-1. Stacks, Lemma 10.161.6 (032J).

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

Being Japanese is local on Spec R. If the elements of t generate the unit ideal of a domain R and the localization R_f is Japanese for every f ∈ t, then R is Japanese. Stacks, Lemma 10.161.6 (032J). The localization at f = 0 is the zero ring, which is not a domain, and the hypothesis asks nothing of it.

theorem TauCeti.Ring.IsN1.exists_isIntegrallyClosed_localization_away {R : Type u} [CommRing R] [IsDomain R] [IsN1 R] : ∃ (f : R), f ≠ 0 ∧ IsIntegrallyClosed (Localization.Away f)

An N-1 domain is generically integrally closed. If R is an N-1 domain, there is a nonzero f : R such that R_f is integrally closed: a common denominator f of the finite R-module R' of elements of the fraction field integral over R satisfies f • R' ⊆ R, so R_f = R'_f is integrally closed.

instance TauCeti.Ring.IsN1.localization_atPrime {R : Type u} [CommRing R] [IsDomain R] [IsN1 R] (p : Ideal R) [p.IsPrime] : IsN1 (Localization.AtPrime p)

The localization of an N-1 domain at a prime is N-1.

instance TauCeti.Ring.IsJapanese.localization_atPrime {R : Type u} [CommRing R] [IsDomain R] [IsJapanese R] (p : Ideal R) [p.IsPrime] : IsJapanese (Localization.AtPrime p)

The localization of a Japanese domain at a prime is Japanese.

The N-1 local criterion

Let R be a Noetherian domain with fraction field K and let f : R be nonzero with R_f integrally closed. Every element x of K integral over R then lies in R_f, so f ^ n • x ∈ R for some n: the integral closure is the increasing union of the finite R-modules integralPow f n of integral x with f ^ n • x ∈ R. Multiplication by f embeds each quotient integralPow f (n + 2) / integralPow f (n + 1) into the previous one, so the annihilators integralPowColon f n of these quotients form an ascending chain of ideals, which stabilizes. If R_𝔪 is N-1, finitely many generators of its integral closure, after clearing denominators outside 𝔪, lie in some integralPow f n, so integralPowColon f n is not contained in 𝔪. When this holds at every maximal ideal the stable value of the chain is R, the chain integralPow f n is eventually constant, and the integral closure is finite.

theorem TauCeti.Ring.IsN1.of_isIntegrallyClosed_localization_away_of_isN1_localization_atPrime {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R] {f : R} (hf : f ≠ 0) (hfn : IsIntegrallyClosed (Localization.Away f)) (H : ∀ (m : Ideal R) [inst : m.IsMaximal], IsN1 (Localization.AtPrime m)) : IsN1 R

The N-1 local criterion. A Noetherian domain R is N-1 as soon as R_f is integrally closed for some nonzero f : R and the localization R_𝔪 is N-1 at every maximal ideal 𝔪. Stacks, Lemma 10.161.15 (0333); the equivalence is isN1_iff_exists_isIntegrallyClosed_localization_away_and_isN1_localization_atPrime.

theorem TauCeti.Ring.isN1_iff_exists_isIntegrallyClosed_localization_away_and_isN1_localization_atPrime {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R] : IsN1 R ↔ (∃ (f : R), f ≠ 0 ∧ IsIntegrallyClosed (Localization.Away f)) ∧ ∀ (m : Ideal R) [inst : m.IsMaximal], IsN1 (Localization.AtPrime m)

The N-1 local criterion. A Noetherian domain R is N-1 if and only if R_f is integrally closed for some nonzero f : R and the localization R_𝔪 is N-1 at every maximal ideal 𝔪. Stacks, Lemma 10.161.15 (0333).