Dedekind domains #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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

is_localization.at_prime.discrete_valuation_ring_of_dedekind_domain shows that is_dedekind_domain implies the localization at each nonzero prime ideal is a DVR.
is_dedekind_domain.is_dedekind_domain_dvr 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 : ¬ is_field A) assumption whenever this is explicitly needed.

References #

Tags #

dedekind domain, dedekind ring

source

structure is_dedekind_domain_dvr (A : Type u_2) [comm_ring A] [is_domain A] :

Prop

is_noetherian_ring : is_noetherian_ring A
is_dvr_at_nonzero_prime : ∀ (P : ideal A), P ≠ ⊥ → ∀ (ᾰ : P.is_prime), discrete_valuation_ring (localization.at_prime P)

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

source

theorem ring.dimension_le_one.localization {R : Type u_1} (Rₘ : Type u_2) [comm_ring R] [is_domain R] [comm_ring Rₘ] [algebra R Rₘ] {M : submonoid R} [is_localization M Rₘ] (hM : M ≤ non_zero_divisors R) (h : ring.dimension_le_one R) :

ring.dimension_le_one 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.

source

theorem is_localization.is_dedekind_domain (A : Type u_2) [comm_ring A] [is_domain A] [is_dedekind_domain A] {M : submonoid A} (hM : M ≤ non_zero_divisors A) (Aₘ : Type u_1) [comm_ring Aₘ] [is_domain Aₘ] [algebra A Aₘ] [is_localization M Aₘ] :

is_dedekind_domain Aₘ

The localization of a Dedekind domain is a Dedekind domain.

source

theorem is_localization.at_prime.is_dedekind_domain (A : Type u_2) [comm_ring A] [is_domain A] [is_dedekind_domain A] (P : ideal A) [P.is_prime] (Aₘ : Type u_1) [comm_ring Aₘ] [is_domain Aₘ] [algebra A Aₘ] [is_localization.at_prime Aₘ P] :

is_dedekind_domain Aₘ

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

source

theorem is_localization.at_prime.not_is_field (A : Type u_2) [comm_ring A] [is_domain A] {P : ideal A} (hP : P ≠ ⊥) [pP : P.is_prime] (Aₘ : Type u_1) [comm_ring Aₘ] [algebra A Aₘ] [is_localization.at_prime Aₘ P] :

¬is_field Aₘ

source

theorem is_localization.at_prime.discrete_valuation_ring_of_dedekind_domain (A : Type u_2) [comm_ring A] [is_domain A] [is_dedekind_domain A] {P : ideal A} (hP : P ≠ ⊥) [pP : P.is_prime] (Aₘ : Type u_1) [comm_ring Aₘ] [is_domain Aₘ] [algebra A Aₘ] [is_localization.at_prime Aₘ P] :

discrete_valuation_ring Aₘ

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

source

theorem is_dedekind_domain.is_dedekind_domain_dvr (A : Type u_2) [comm_ring A] [is_domain A] [is_dedekind_domain A] :

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