Dedekind domains

This file defines an equivalent notion of a Dedekind domain (or Dedekind ring), namely a Noetherian integral domain where the localization at every nonzero prime ideal is a DVR.

Main definitions

• IsDedekindDomainDvr alternatively defines a Dedekind domain as an integral domain that is Noetherian, and the localization at every nonzero prime ideal is a DVR.

Main results

• IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain shows that IsDedekindDomain implies the localization at each nonzero prime ideal is a DVR.
• IsDedekindDomain.isDedekindDomainDvr is one direction of the equivalence of definitions of a Dedekind domain

Implementation notes

The definitions that involve a field of fractions choose a canonical field of fractions, but are independent of that choice. The ..._iff lemmas express this independence.

Often, definitions assume that Dedekind domains are not fields. We found it more practical to add a (h : ¬ IsField A) assumption whenever this is explicitly needed.

References

• [D. Marcus, Number Fields][marcus1977number]
• [J.W.S. Cassels, A. Fröhlich, Algebraic Number Theory][cassels1967algebraic]
• [J. Neukirch, Algebraic Number Theory][Neukirch1992]

Tags

dedekind domain, dedekind ring

class IsDedekindDomainDvr (A : Type u_1) [CommRing A] [IsDomain A] extends IsNoetherian A A : Prop

A Dedekind domain is an integral domain that is Noetherian, and the localization at every nonzero prime is a discrete valuation ring.

This is equivalent to IsDedekindDomain.

• noetherian (s : Submodule A A) : s.FG
• is_dvr_at_nonzero_prime (P : Ideal A) : P ≠ ⊥ → ∀ (x : P.IsPrime), IsDiscreteValuationRing (Localization.AtPrime P)

theorem Ring.DimensionLEOne.localization {R : Type u_2} (Rₘ : Type u_3) [CommRing R] [IsDomain R] [CommRing Rₘ] [Algebra R Rₘ] {M : Submonoid R} [IsLocalization M Rₘ] (hM : M ≤ nonZeroDivisors R) [h : DimensionLEOne R] : DimensionLEOne Rₘ

Localizing a domain of Krull dimension ≤ 1 gives another ring of Krull dimension ≤ 1.

Note that the same proof can/should be generalized to preserving any Krull dimension, once we have a suitable definition.

theorem IsLocalization.isDedekindDomain (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] {M : Submonoid A} (hM : M ≤ nonZeroDivisors A) (Aₘ : Type u_2) [CommRing Aₘ] [IsDomain Aₘ] [Algebra A Aₘ] [IsLocalization M Aₘ] : IsDedekindDomain Aₘ

The localization of a Dedekind domain is a Dedekind domain.

theorem IsLocalization.AtPrime.isDedekindDomain (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] (P : Ideal A) [P.IsPrime] (Aₘ : Type u_2) [CommRing Aₘ] [IsDomain Aₘ] [Algebra A Aₘ] [IsLocalization.AtPrime Aₘ P] : IsDedekindDomain Aₘ

The localization of a Dedekind domain at every nonzero prime ideal is a Dedekind domain.

instance Localization.AtPrime.isDedekindDomain (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] (P : Ideal A) [P.IsPrime] : IsDedekindDomain (Localization.AtPrime P)

theorem IsLocalization.AtPrime.not_isField (A : Type u_1) [CommRing A] [IsDomain A] {P : Ideal A} (hP : P ≠ ⊥) [pP : P.IsPrime] (Aₘ : Type u_2) [CommRing Aₘ] [Algebra A Aₘ] [IsLocalization.AtPrime Aₘ P] : ¬IsField Aₘ

theorem IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] {P : Ideal A} (hP : P ≠ ⊥) [pP : P.IsPrime] (Aₘ : Type u_2) [CommRing Aₘ] [IsDomain Aₘ] [Algebra A Aₘ] [IsLocalization.AtPrime Aₘ P] : IsDiscreteValuationRing Aₘ

In a Dedekind domain, the localization at every nonzero prime ideal is a DVR.

instance IsDedekindDomain.isDedekindDomainDvr (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] : IsDedekindDomainDvr A

Dedekind domains, in the sense of Noetherian integrally closed domains of Krull dimension ≤ 1, are also Dedekind domains in the sense of Noetherian domains where the localization at every nonzero prime ideal is a DVR.

instance IsDedekindDomainDvr.ring_dimensionLEOne (A : Type u_1) [CommRing A] [IsDomain A] [h : IsDedekindDomainDvr A] : Ring.DimensionLEOne A

instance IsDedekindDomainDvr.isIntegrallyClosed (A : Type u_1) [CommRing A] [IsDomain A] [h : IsDedekindDomainDvr A] : IsIntegrallyClosed A

instance IsDedekindDomainDvr.isDedekindDomain (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomainDvr A] : IsDedekindDomain A

If an integral domain is Noetherian, and the localization at every nonzero prime is a discrete valuation ring, then it is a Dedekind domain.