Dedekind domains and invertible ideals #
In this file, we show a ring is a Dedekind domain iff all fractional ideals are invertible,
and prove instances such as the unique factorization of ideals.
Further results on the structure of ideals in a Dedekind domain are found in
Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
.
Main definitions #
IsDedekindDomainInv
alternatively defines a Dedekind domain as an integral domain where every nonzero fractional ideal is invertible.isDedekindDomainInv_iff
shows that this does note depend on the choice of field of fractions.
Main results: #
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
- J.W.S. Cassels, A. Fröhlich, Algebraic Number Theory
- J. Neukirch, Algebraic Number Theory
Tags #
dedekind domain, dedekind ring
A Dedekind domain is an integral domain such that every fractional ideal has an inverse.
This is equivalent to IsDedekindDomain
.
In particular we provide a fractional_ideal.comm_group_with_zero
instance,
assuming IsDedekindDomain A
, which implies IsDedekindDomainInv
. For integral ideals,
IsDedekindDomain
(_inv
) implies only Ideal.cancelCommMonoidWithZero
.
Equations
- IsDedekindDomainInv A = ∀ (I : FractionalIdeal (nonZeroDivisors A) (FractionRing A)), I ≠ ⊥ → I * I⁻¹ = 1
Instances For
Showing one side of the equivalence between the definitions
IsDedekindDomainInv
and IsDedekindDomain
of Dedekind domains.
Specialization of exists_primeSpectrum_prod_le_and_ne_bot_of_domain
to Dedekind domains:
Let I : Ideal A
be a nonzero ideal, where A
is a Dedekind domain that is not a field.
Then exists_primeSpectrum_prod_le_and_ne_bot_of_domain
states we can find a product of prime
ideals that is contained within I
. This lemma extends that result by making the product minimal:
let M
be a maximal ideal that contains I
, then the product including M
is contained within I
and the product excluding M
is not contained within I
.
Nonzero integral ideals in a Dedekind domain are invertible.
We will use this to show that nonzero fractional ideals are invertible, and finally conclude that fractional ideals in a Dedekind domain form a group with zero.
Nonzero fractional ideals in a Dedekind domain are units.
This is also available as _root_.mul_inv_cancel
, using the
Semifield
instance defined below.
This is also available as _root_.div_eq_mul_inv
, using the
Semifield
instance defined below.
IsDedekindDomain
and IsDedekindDomainInv
are equivalent ways
to express that an integral domain is a Dedekind domain.
Equations
- One or more equations did not get rendered due to their size.
Fractional ideals have cancellative multiplication in a Dedekind domain.
Although this instance is a direct consequence of the instance
FractionalIdeal.semifield
, we define this instance to provide
a computable alternative.
Equations
- One or more equations did not get rendered due to their size.
Equations
For ideals in a Dedekind domain, to divide is to contain.