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
- J.W.S. Cassels, A. Frölich, Algebraic Number Theory
- J. Neukirch, Algebraic Number Theory
Tags #
dedekind domain, dedekind ring
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
.
- noetherian : ∀ (s : Submodule A A), s.FG
- maximalOfPrime : ∀ {p : Ideal A}, p ≠ ⊥ → p.IsPrime → p.IsMaximal
- isIntegral_iff : ∀ {x : FractionRing A}, IsIntegral A x ↔ ∃ (y : A), (algebraMap A (FractionRing A)) y = x
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 [Neu99].
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,
IsDedekindDomainDvr
and IsDedekindDomainInv
.
- exists_pair_ne : ∃ (x : A) (y : A), x ≠ y
- noetherian : ∀ (s : Submodule A A), s.FG
- maximalOfPrime : ∀ {p : Ideal A}, p ≠ ⊥ → p.IsPrime → p.IsMaximal
- isIntegral_iff : ∀ {x : FractionRing A}, IsIntegral A x ↔ ∃ (y : A), (algebraMap A (FractionRing A)) y = x
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.
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.