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

- `isDedekindDomain_iff_isDedekindDomainInv`
- `Ideal.uniqueFactorizationMonoid`

## 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][marcus1977number]
- [J.W.S. Cassels, A. Fröhlich, Algebraic Number Theory][cassels1967algebraic]
- [J. Neukirch, Algebraic Number Theory][Neukirch1992]

## Tags #

dedekind domain, dedekind ring

source
def IsDedekindDomainInv (A : Type u_2) [CommRing A] [IsDomain A] :
Prop

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 `CommGroupWithZero` instance, assuming `IsDedekindDomain A`, which implies `IsDedekindDomainInv`. For integral domain, `IsDedekindDomain`(`Inv`) implies only `Ideal.cancelCommMonoidWithZero`.

Equations

- IsDedekindDomainInv A = ∀ (I : FractionalIdeal (nonZeroDivisors A) (FractionRing A)), I ≠ ⊥ → I * I⁻¹ = 1

Instances For

source
theorem isDedekindDomainInv_iff {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] :
IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal (nonZeroDivisors A) K), I ≠ ⊥ → I * I⁻¹ = 1
source
theorem FractionalIdeal.adjoinIntegral_eq_one_of_isUnit {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (x : K) (hx : IsIntegral A x) (hI : IsUnit (adjoinIntegral (nonZeroDivisors A) x hx)) :
adjoinIntegral (nonZeroDivisors A) x hx = 1
source
@[reducible, inline]
noncomputable abbrev IsDedekindDomainInv.commGroupWithZero {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (h : IsDedekindDomainInv A) :
CommGroupWithZero (FractionalIdeal (nonZeroDivisors A) K)

`IsDedekindDomainInv A` implies that fractional ideals over it form a commutative group with zero.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[deprecated mul_inv_cancel₀ (since := "2025-09-09")]
theorem IsDedekindDomainInv.mul_inv_eq_one {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (h : IsDedekindDomainInv A) {I : FractionalIdeal (nonZeroDivisors A) K} (hI : I ≠ 0) :
I * I⁻¹ = 1
source
@[deprecated inv_mul_cancel₀ (since := "2025-09-09")]
theorem IsDedekindDomainInv.inv_mul_eq_one {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (h : IsDedekindDomainInv A) {I : FractionalIdeal (nonZeroDivisors A) K} (hI : I ≠ 0) :
I⁻¹ * I = 1
source
theorem IsDedekindDomainInv.isNoetherianRing {A : Type u_2} [CommRing A] [IsDomain A] (h : IsDedekindDomainInv A) :
IsNoetherianRing A
source
theorem IsDedekindDomainInv.integrallyClosed {A : Type u_2} [CommRing A] [IsDomain A] (h : IsDedekindDomainInv A) :
IsIntegrallyClosed A
source
theorem IsDedekindDomainInv.dimensionLEOne {A : Type u_2} [CommRing A] [IsDomain A] (h : IsDedekindDomainInv A) :
Ring.DimensionLEOne A
source
theorem IsDedekindDomainInv.isDedekindDomain {A : Type u_2} [CommRing A] [IsDomain A] (h : IsDedekindDomainInv A) :
IsDedekindDomain A

Showing one side of the equivalence between the definitions `IsDedekindDomainInv` and `IsDedekindDomain` of Dedekind domains.

source
theorem one_mem_inv_coe_ideal {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDomain A] {I : Ideal A} (hI : I ≠ ⊥) :
1 ∈ (↑I)⁻¹
source
theorem exists_multiset_prod_cons_le_and_prod_not_le {A : Type u_2} [CommRing A] [IsDedekindDomain A] (hNF : ¬IsField A) {I M : Ideal A} (hI0 : I ≠ ⊥) (hIM : I ≤ M) [hM : M.IsMaximal] :
∃ (Z : Multiset (PrimeSpectrum A)), (M ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I

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

source
theorem FractionalIdeal.not_inv_le_one_of_ne_bot {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {I : Ideal A} (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) :
¬(↑I)⁻¹ ≤ 1
source
theorem FractionalIdeal.mul_inv_cancel_of_le_one {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {I : Ideal A} (hI0 : I ≠ ⊥) (hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1) :
↑I * (↑I)⁻¹ = 1
source
theorem FractionalIdeal.coe_ideal_mul_inv {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (I : Ideal A) (hI0 : I ≠ ⊥) :
↑I * (↑I)⁻¹ = 1

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.

source
noncomputable instance FractionalIdeal.semifield {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] :
Semifield (FractionalIdeal (nonZeroDivisors A) K)
Equations

- One or more equations did not get rendered due to their size.

source
instance FractionalIdeal.cancelCommMonoidWithZero {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] :
CancelCommMonoidWithZero (FractionalIdeal (nonZeroDivisors A) K)

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.

source
instance FractionalIdeal.instPosMulStrictMonoNonZeroDivisors {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] :
PosMulStrictMono (FractionalIdeal (nonZeroDivisors A) K)
source
instance FractionalIdeal.instMulPosStrictMonoNonZeroDivisors {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] :
MulPosStrictMono (FractionalIdeal (nonZeroDivisors A) K)
source
instance FractionalIdeal.instPosMulReflectLENonZeroDivisors {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] :
PosMulReflectLE (FractionalIdeal (nonZeroDivisors A) K)
source
instance FractionalIdeal.instMulPosReflectLENonZeroDivisors {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] :
MulPosReflectLE (FractionalIdeal (nonZeroDivisors A) K)
source
@[deprecated mul_inv_cancel₀ (since := "2025-09-14")]
theorem FractionalIdeal.mul_inv_cancel {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {I : FractionalIdeal (nonZeroDivisors A) K} (hne : I ≠ 0) :
I * I⁻¹ = 1
source
@[deprecated mul_le_mul_iff_left₀ (since := "2025-09-14")]
theorem FractionalIdeal.mul_right_le_iff {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {J : FractionalIdeal (nonZeroDivisors A) K} (hJ : J ≠ 0) {I I' : FractionalIdeal (nonZeroDivisors A) K} :
I * J ≤ I' * J ↔ I ≤ I'
source
@[deprecated mul_le_mul_iff_left₀ (since := "2025-09-14")]
theorem FractionalIdeal.mul_left_le_iff {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {J : FractionalIdeal (nonZeroDivisors A) K} (hJ : J ≠ 0) {I I' : FractionalIdeal (nonZeroDivisors A) K} :
J * I ≤ J * I' ↔ I ≤ I'
source
theorem FractionalIdeal.mul_left_strictMono {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {I : FractionalIdeal (nonZeroDivisors A) K} (hI : I ≠ 0) :
StrictMono fun (x : FractionalIdeal (nonZeroDivisors A) K) => x * I
source
theorem FractionalIdeal.mul_right_strictMono {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {I : FractionalIdeal (nonZeroDivisors A) K} (hI : I ≠ 0) :
StrictMono fun (x : FractionalIdeal (nonZeroDivisors A) K) => I * x
source
instance FractionalIdeal.instPosMulReflectLEIdealOfIsDedekindDomain {A : Type u_2} [CommRing A] [IsDedekindDomain A] :
PosMulReflectLE (Ideal A)
source
@[deprecated div_eq_mul_inv (since := "2025-09-14")]
theorem FractionalIdeal.div_eq_mul_inv {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (I J : FractionalIdeal (nonZeroDivisors A) K) :
I / J = I * J⁻¹
source
theorem isDedekindDomain_iff_isDedekindDomainInv {A : Type u_2} [CommRing A] [IsDomain A] :
IsDedekindDomain A ↔ IsDedekindDomainInv A

`IsDedekindDomain` and `IsDedekindDomainInv` are equivalent ways to express that an integral domain is a Dedekind domain.

source
noncomputable instance Ideal.cancelCommMonoidWithZero {A : Type u_2} [CommRing A] [IsDedekindDomain A] :
CancelCommMonoidWithZero (Ideal A)
Equations

- Ideal.cancelCommMonoidWithZero = Function.Injective.cancelCommMonoidWithZero ⇑(FractionalIdeal.coeIdealHom (nonZeroDivisors A) (FractionRing A)) ⋯ ⋯ ⋯ ⋯ ⋯

source
instance Ideal.isDomain {A : Type u_2} [CommRing A] [IsDedekindDomain A] :
IsDomain (Ideal A)
source
instance instPosMulStrictMonoIdeal {A : Type u_2} [CommRing A] [IsDedekindDomain A] :
PosMulStrictMono (Ideal A)
source
instance instMulPosStrictMonoIdeal {A : Type u_2} [CommRing A] [IsDedekindDomain A] :
MulPosStrictMono (Ideal A)
source
theorem Ideal.dvd_iff_le {A : Type u_2} [CommRing A] [IsDedekindDomain A] {I J : Ideal A} :
I ∣ J ↔ J ≤ I

For ideals in a Dedekind domain, to divide is to contain.

source
theorem Ideal.liesOver_iff_dvd_map {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [IsDedekindDomain A] [Algebra R A] {p : Ideal R} {P : Ideal A} (hP : P ≠ ⊤) [p.IsMaximal] :
P.LiesOver p ↔ P ∣ map (algebraMap R A) p
source
theorem Ideal.dvdNotUnit_iff_lt {A : Type u_2} [CommRing A] [IsDedekindDomain A] {I J : Ideal A} :
DvdNotUnit I J ↔ J < I
source
instance instWfDvdMonoidIdeal {A : Type u_2} [CommRing A] [IsDedekindDomain A] :
WfDvdMonoid (Ideal A)
source
instance Ideal.uniqueFactorizationMonoid {A : Type u_2} [CommRing A] [IsDedekindDomain A] :
UniqueFactorizationMonoid (Ideal A)
source
noncomputable instance Ideal.normalizationMonoid {A : Type u_2} [CommRing A] [IsDedekindDomain A] :
NormalizationMonoid (Ideal A)
Equations

- Ideal.normalizationMonoid = NormalizationMonoid.ofUniqueUnits