# Dedekind rings and domains #

This file defines the notion of a Dedekind ring (domain), as a Noetherian integrally closed commutative ring (domain) of Krull dimension at most one.

## Main definitions #

`IsDedekindRing`

defines a Dedekind ring as a commutative ring that is Noetherian, integrally closed in its field of fractions and has Krull dimension at most one.`isDedekindRing_iff`

shows that this does not depend on the choice of field of fractions.`IsDedekindDomain`

defines a Dedekind domain as a Dedekind ring that is a 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.

`IsDedekindRing`

and `IsDedekindDomain`

form a cycle in the typeclass hierarchy:
`IsDedekindRing R + IsDomain R`

imply `IsDedekindDomain R`

, which implies `IsDedekindRing R`

.
This should be safe since the start and end point is the literal same expression,
which the tabled typeclass synthesis algorithm can deal with.

Often, definitions assume that Dedekind rings 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

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

A Dedekind ring is a commutative ring that is Noetherian, integrally closed, and has Krull dimension at most one.

This is exactly `IsDedekindDomain`

minus the `IsDomain`

hypothesis.

The integral closure condition is independent of the choice of field of fractions:
use `isDedekindRing_iff`

to prove `IsDedekindRing`

for a given `fraction_map`

.

## Instances

An integral domain is a Dedekind domain if and only if it 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.

A Dedekind domain is an integral domain that is Noetherian, integrally closed, and has Krull dimension at most one.

This is definition 3.2 of [Neukirch1992].

This is exactly `IsDedekindRing`

plus the `IsDomain`

hypothesis.

The integral closure condition is independent of the choice of field of fractions:
use `isDedekindDomain_iff`

to prove `IsDedekindDomain`

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.

## Instances

Make a Dedekind domain from a Dedekind ring given that it is a domain.

`IsDedekindRing`

and `IsDedekindDomain`

form a cycle in the typeclass hierarchy:
`IsDedekindRing R + IsDomain R`

imply `IsDedekindDomain R`

, which implies `IsDedekindRing R`

.
This should be safe since the start and end point is the literal same expression,
which the tabled typeclass synthesis algorithm can deal with.

## Equations

- ⋯ = ⋯

An integral domain is a Dedekind domain iff and only if it 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.

## Equations

- ⋯ = ⋯