Integral closures of one-dimensional Noetherian domains

Let A be a Noetherian domain of dimension at most one with fraction field K, and let L be a finite extension of K. Any integral closure of A in L is a Dedekind domain. Neither integral closedness of A nor separability of L / K is required. In particular, this applies to the normalization of a singular affine curve and to inseparable function-field extensions.

Main results

• TauCeti.IsIntegralClosure.isDedekindDomain: the result for any ring C known to be an integral closure of A in L.
• TauCeti.integralClosure.isDedekindDomain: the result for Mathlib's integralClosure A L, with a fraction field chosen by the caller.
• TauCeti.integralClosure.isDedekindDomain_fractionRing: the instance with K := FractionRing A.

The abstract form applies, for example, to a subring of a function field known to be an integral closure. The ring C need not be assumed to be a domain: its map into the field L is injective.

Krull–Akizuki gives Noetherianity without separability, but does not assert that the integral closure is a finite A-module. That stronger conclusion requires additional hypotheses on the base ring or extension. For example, Mathlib proves module finiteness for separable extensions when A is integrally closed, and TauCeti.IsIntegralClosure.finite_adjoin_of_transcendental proves it over a polynomial subalgebra of a function field without separability.

References

The proof follows Mathlib's IsIntegralClosure.isDedekindDomain (Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean), replacing its separable Noetherianity argument with Krull–Akizuki, TauCeti.IsIntegralClosure.isNoetherianRing.

theorem TauCeti.IsIntegralClosure.isDedekindDomain (A : Type u_1) [CommRing A] [IsDomain A] [IsNoetherianRing A] [Ring.DimensionLEOne A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [Module.Finite K L] (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C L] [IsScalarTower A C L] [IsIntegralClosure C A L] : IsDedekindDomain C

An integral closure of a Noetherian domain of dimension at most one in a finite extension of its fraction field is a Dedekind domain. Neither integral closedness of the base ring nor separability of the extension is required. The integral closure need not be assumed to be a domain.

This does not assert finiteness as a module over the base ring.

theorem TauCeti.integralClosure.isDedekindDomain (A : Type u_1) [CommRing A] [IsDomain A] [IsNoetherianRing A] [Ring.DimensionLEOne A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [Module.Finite K L] : IsDedekindDomain ↥(integralClosure A L)

The integral closure of a Noetherian domain of dimension at most one in a finite extension of its fraction field is a Dedekind domain, with no separability hypothesis.

This cannot be an instance since K cannot be inferred; see integralClosure.isDedekindDomain_fractionRing for the instance with K := FractionRing A.

instance TauCeti.integralClosure.isDedekindDomain_fractionRing {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] [Ring.DimensionLEOne A] {L : Type u_2} [Field L] [Algebra A L] [Algebra (FractionRing A) L] [IsScalarTower A (FractionRing A) L] [Module.Finite (FractionRing A) L] : IsDedekindDomain ↥(integralClosure A L)

For a Noetherian domain A of dimension at most one and a finite extension L of FractionRing A, the integral closure of A in L is a Dedekind domain. No separability is required. See integralClosure.isDedekindDomain to choose the fraction field.