# mathlibdocumentation

ring_theory.dedekind_domain

# Dedekind domains

This file defines the notion of a Dedekind domain (or Dedekind ring), giving three equivalent definitions (TODO: and shows that they are equivalent).

## Main definitions

• is_dedekind_domain defines a Dedekind domain as a commutative ring that is not a field, Noetherian, integrally closed in its field of fractions and has Krull dimension exactly one. is_dedekind_domain_iff shows that this does not depend on the choice of field of fractions.
• is_dedekind_domain_dvr alternatively defines a Dedekind domain as an integral domain that is not a field, Noetherian, and the localization at every nonzero prime ideal is a discrete valuation ring.
• is_dedekind_domain_inv alternatively defines a Dedekind domain as an integral domain that is not a field, and every nonzero fractional ideal is invertible.
• is_dedekind_domain_inv_iff shows that this does note depend on the choice of field of fractions.

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

## References

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

## Tags

dedekind domain, dedekind ring

def ring.dimension_le_one (R : Type u_1) [comm_ring R] :
Prop

A ring R has Krull dimension at most one if all nonzero prime ideals are maximal.

Equations
theorem ring.dimension_le_one.integral_closure (R : Type u_1) (A : Type u_2) [comm_ring R] [nontrivial R] [ A] :

@[class]
structure is_dedekind_domain (A : Type u_2)  :
Prop
• not_is_field :
• is_noetherian_ring :
• dimension_le_one :
• is_integrally_closed :

A Dedekind domain is an integral domain that is Noetherian, integrally closed, and has Krull dimension exactly one (not_is_field and dimension_le_one).

The integral closure condition is independent of the choice of field of fractions: use is_dedekind_domain_iff to prove is_dedekind_domain for a given fraction_map.

This is the default implementation, but there are equivalent definitions, is_dedekind_domain_dvr and is_dedekind_domain_inv. TODO: Prove that these are actually equivalent definitions.

theorem is_dedekind_domain_iff (A : Type u_2) (K : Type u_3) [field K] (f : K) :

An integral domain is a Dedekind domain iff and only if it is not a field, is Noetherian, has dimension ≤ 1, and is integrally closed in a given fraction field. In particular, this definition does not depend on the choice of this fraction field.

structure is_dedekind_domain_dvr (A : Type u_2)  :
Prop
• not_is_field :
• is_noetherian_ring :
• is_dvr_at_nonzero_prime : ∀ (P : ideal A), P ∀ (a : P.is_prime),

A Dedekind domain is an integral domain that is not a field, 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.

structure is_dedekind_domain_inv (A : Type u_2)  :
Prop
• not_is_field :
• mul_inv_cancel : ∀ (I : , I I * I⁻¹ = 1

A Dedekind domain is an integral domain that is not a field such that every fractional ideal has an inverse.

This is equivalent to is_dedekind_domain. TODO: prove the equivalence.

theorem is_dedekind_domain_inv_iff (A : Type u_2) (K : Type u_3) [field K] (f : K) :
∀ (I : , I I * I⁻¹ = 1