# Dedekind domains #

This file defines an equivalent notion of a Dedekind domain (or Dedekind ring), namely a Noetherian integral domain where the localization at all nonzero prime ideals is a DVR (TODO: and shows that implies the main definition).

## 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.

## 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ölich, Algebraic Number Theory][cassels1967algebraic]
• [J. Neukirch, Algebraic Number Theory][Neukirch1992]

## Tags #

dedekind domain, dedekind ring

structure IsDedekindDomainDvr (A : Type u_2) [] [] :

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. TODO: prove the equivalence.

• isNoetherianRing :
• is_dvr_at_nonzero_prime : ∀ (P : ), P ∀ (x : ),
Instances For
theorem Ring.DimensionLEOne.localization {R : Type u_4} (Rₘ : Type u_5) [] [] [CommRing Rₘ] [Algebra R Rₘ] {M : } [] (hM : ) [h : ] :

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_2) [] [] [] {M : } (hM : ) (Aₘ : Type u_4) [CommRing Aₘ] [IsDomain Aₘ] [Algebra A Aₘ] [] :

The localization of a Dedekind domain is a Dedekind domain.

theorem IsLocalization.AtPrime.isDedekindDomain (A : Type u_2) [] [] [] (P : ) [] (Aₘ : Type u_4) [CommRing Aₘ] [IsDomain Aₘ] [Algebra A Aₘ] [] :

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

theorem IsLocalization.AtPrime.not_isField (A : Type u_2) [] [] {P : } (hP : P ) [pP : ] (Aₘ : Type u_4) [CommRing Aₘ] [Algebra A Aₘ] [] :
theorem IsLocalization.AtPrime.discreteValuationRing_of_dedekind_domain (A : Type u_2) [] [] [] {P : } (hP : P ) [pP : ] (Aₘ : Type u_4) [CommRing Aₘ] [IsDomain Aₘ] [Algebra A Aₘ] [] :

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

theorem IsDedekindDomain.isDedekindDomainDvr (A : Type u_2) [] [] [] :

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.