Overrings of a Dedekind domain in its fraction field

An overring of A here is a subalgebra of the fraction field K of A, that is, a ring between A and K. Every such ring is integrally closed: its localizations at maximal ideals are localizations of A too, and those are valuation rings of K, or K itself over the zero prime.

Nothing about integral closures of A in larger fields is needed for this, which is why it lives apart from RingTheory/IntegralClosure/.

The extension to an overring B of a height one prime 𝔭 of A is read off the valuation of 𝔭. If some element of B has a pole at 𝔭, the extension is the unit ideal: that pole puts an element of A outside 𝔭 into 𝔭B. If instead the valuation of 𝔭 is the valuation of a height one prime 𝔓 of B, then 𝔓 is the only prime of B containing 𝔭B, and 𝔭B = 𝔓, with no ramification, the two rings having the same fraction field.

Main results

• Subalgebra.isIntegrallyClosed_overring: every subalgebra of the fraction field of a Dedekind domain is integrally closed.
• IsDedekindDomain.HeightOneSpectrum.map_asIdeal_eq_top_of_one_lt_valuation: a prime extends to the unit ideal of an overring containing an element with a pole at it.
• IsDedekindDomain.HeightOneSpectrum.map_asIdeal_eq_asIdeal_of_valuation_eq: a prime extends to the prime of an overring carrying the same valuation.

Provenance

Adapted from D. K. Angdinata's NormalizationFinite.lean, Apache-2.0, supplied by the author on 2026-09-07, declaration Subalgebra.isIntegrallyClosed_overring.

theorem Subalgebra.isIntegrallyClosed_overring {A : Type u_1} {K : Type u_2} [CommRing A] [IsDedekindDomain A] [Field K] [Algebra A K] [IsFractionRing A K] (C : Subalgebra A K) : IsIntegrallyClosed ↥C

Every overring of a Dedekind domain in its fraction field is integrally closed.

theorem IsDedekindDomain.HeightOneSpectrum.map_asIdeal_eq_top_of_one_lt_valuation {A : Type u_1} {K : Type u_2} {B : Type u_3} [CommRing A] [IsDedekindDomain A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing B] [Algebra A B] [Algebra B K] [IsScalarTower A B K] [FaithfulSMul B K] (v : HeightOneSpectrum A) {b : B} (hb : 1 < (valuation K v) ((algebraMap B K) b)) : Ideal.map (algebraMap A B) v.asIdeal = ⊤

A prime extends to the unit ideal of an overring containing an element with a pole at it. If b ∈ B has v 𝔭 b > 1, then 𝔭B is the unit ideal.

theorem IsDedekindDomain.HeightOneSpectrum.map_asIdeal_eq_asIdeal_of_valuation_eq {A : Type u_1} {K : Type u_2} {B : Type u_3} [CommRing A] [IsDedekindDomain A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing B] [Algebra A B] [Algebra B K] [IsScalarTower A B K] [IsDedekindDomain B] [IsFractionRing B K] (v : HeightOneSpectrum A) (𝔓 : HeightOneSpectrum B) (h : valuation K 𝔓 = valuation K v) : Ideal.map (algebraMap A B) v.asIdeal = 𝔓.asIdeal

A prime extends to the prime of an overring carrying the same valuation, unramified: if the valuation of the height one prime 𝔓 of the Dedekind overring B is that of 𝔭, then 𝔭B = 𝔓.