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 not 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

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

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

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

@[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.

@[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

@[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

theorem IsDedekindDomainInv.isNoetherianRing {A : Type u_2} [CommRing A] [IsDomain A] (h : IsDedekindDomainInv A) : IsNoetherianRing A

theorem IsDedekindDomainInv.integrallyClosed {A : Type u_2} [CommRing A] [IsDomain A] (h : IsDedekindDomainInv A) : IsIntegrallyClosed A

theorem IsDedekindDomainInv.dimensionLEOne {A : Type u_2} [CommRing A] [IsDomain A] (h : IsDedekindDomainInv A) : Ring.DimensionLEOne A

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.

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)⁻¹

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.

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

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

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.

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)

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)

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)

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)

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)

@[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

@[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'

@[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'

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

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

instance FractionalIdeal.instPosMulReflectLEIdealOfIsDedekindDomain {A : Type u_2} [CommRing A] [IsDedekindDomain A] : PosMulReflectLE (Ideal A)

@[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⁻¹

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.

instance Ideal.isCancelMulZero {A : Type u_2} [CommRing A] [IsDedekindDomain A] : IsCancelMulZero (Ideal A)

instance Ideal.isDomain {A : Type u_2} [CommRing A] [IsDedekindDomain A] : IsDomain (Ideal A)

instance instPosMulStrictMonoIdeal {A : Type u_2} [CommRing A] [IsDedekindDomain A] : PosMulStrictMono (Ideal A)

instance instMulPosStrictMonoIdeal {A : Type u_2} [CommRing A] [IsDedekindDomain A] : MulPosStrictMono (Ideal A)

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.

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

theorem Ideal.dvdNotUnit_iff_lt {A : Type u_2} [CommRing A] [IsDedekindDomain A] {I J : Ideal A} : DvdNotUnit I J ↔ J < I

instance instWfDvdMonoidIdeal {A : Type u_2} [CommRing A] [IsDedekindDomain A] : WfDvdMonoid (Ideal A)

instance Ideal.uniqueFactorizationMonoid {A : Type u_2} [CommRing A] [IsDedekindDomain A] : UniqueFactorizationMonoid (Ideal A)

noncomputable instance Ideal.normalizationMonoid {A : Type u_2} [CommRing A] : NormalizationMonoid (Ideal A)