Documentation

Mathlib.RingTheory.DedekindDomain.Ideal.Basic

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 #

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 #

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
Instances For
    theorem isDedekindDomainInv_iff {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] :
    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
    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.isUnit {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) :

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

    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] [h : 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] [h : 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.

    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

    Nonzero fractional ideals in a Dedekind domain are units.

    This is also available as _root_.mul_inv_cancel, using the Semifield instance defined below.

    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'
    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.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⁻¹

    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.

    noncomputable instance FractionalIdeal.semifield {A : Type u_2} (K : Type u_3) [CommRing A] [Field K] [IsDedekindDomain A] [Algebra A K] [IsFractionRing A K] :
    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.
    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.dvdNotUnit_iff_lt {A : Type u_2} [CommRing A] [IsDedekindDomain A] {I J : Ideal A} :
    DvdNotUnit I J J < I