Documentation

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Dedekind domains and ideals #

In this file, we prove some results on the unique factorization monoid structure of the ideals. The unique factorization of ideals and invertibility of fractional ideals can be found in Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean.

Main definitions #

Implementation notes #

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

theorem FractionalIdeal.exists_notMem_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 ) :
x(↑I)⁻¹, x1
@[deprecated FractionalIdeal.exists_notMem_one_of_ne_bot (since := "2025-05-23")]
theorem FractionalIdeal.exists_not_mem_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 ) :
x(↑I)⁻¹, x1

Alias of FractionalIdeal.exists_notMem_one_of_ne_bot.

@[simp]
theorem Ideal.dvd_span_singleton {A : Type u_2} [CommRing A] [IsDedekindDomain A] {I : Ideal A} {x : A} :
I span {x} x I
theorem Ideal.isPrime_of_prime {A : Type u_2} [CommRing A] [IsDedekindDomain A] {P : Ideal A} (h : Prime P) :
theorem Ideal.prime_of_isPrime {A : Type u_2} [CommRing A] [IsDedekindDomain A] {P : Ideal A} (hP : P ) (h : P.IsPrime) :
theorem Ideal.prime_iff_isPrime {A : Type u_2} [CommRing A] [IsDedekindDomain A] {P : Ideal A} (hP : P ) :

In a Dedekind domain, the (nonzero) prime elements of the monoid with zero Ideal A are exactly the prime ideals.

In a Dedekind domain, the prime ideals are the zero ideal together with the prime elements of the monoid with zero Ideal A.

@[simp]
theorem Ideal.pow_right_strictAnti {A : Type u_2} [CommRing A] [IsDedekindDomain A] (I : Ideal A) (hI0 : I ) (hI1 : I ) :
StrictAnti fun (x : ) => I ^ x
theorem Ideal.pow_lt_self {A : Type u_2} [CommRing A] [IsDedekindDomain A] (I : Ideal A) (hI0 : I ) (hI1 : I ) (e : ) (he : 2 e) :
I ^ e < I
theorem Ideal.exists_mem_pow_notMem_pow_succ {A : Type u_2} [CommRing A] [IsDedekindDomain A] (I : Ideal A) (hI0 : I ) (hI1 : I ) (e : ) :
xI ^ e, xI ^ (e + 1)
@[deprecated Ideal.exists_mem_pow_notMem_pow_succ (since := "2025-05-23")]
theorem Ideal.exists_mem_pow_not_mem_pow_succ {A : Type u_2} [CommRing A] [IsDedekindDomain A] (I : Ideal A) (hI0 : I ) (hI1 : I ) (e : ) :
xI ^ e, xI ^ (e + 1)

Alias of Ideal.exists_mem_pow_notMem_pow_succ.

theorem Ideal.eq_prime_pow_of_succ_lt_of_le {A : Type u_2} [CommRing A] [IsDedekindDomain A] {P I : Ideal A} [P_prime : P.IsPrime] (hP : P ) {i : } (hlt : P ^ (i + 1) < I) (hle : I P ^ i) :
I = P ^ i
theorem Ideal.pow_succ_lt_pow {A : Type u_2} [CommRing A] [IsDedekindDomain A] {P : Ideal A} [P_prime : P.IsPrime] (hP : P ) (i : ) :
P ^ (i + 1) < P ^ i
theorem FractionalIdeal.le_inv_comm {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDedekindDomain A] [Algebra A K] [IsFractionRing A K] {I J : FractionalIdeal (nonZeroDivisors A) K} (hI : I 0) (hJ : J 0) :
theorem FractionalIdeal.inv_le_comm {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDedekindDomain A] [Algebra A K] [IsFractionRing A K] {I J : FractionalIdeal (nonZeroDivisors A) K} (hI : I 0) (hJ : J 0) :
theorem Ideal.exist_integer_multiples_notMem {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDedekindDomain A] [Algebra A K] [IsFractionRing A K] {J : Ideal A} (hJ : J ) {ι : Type u_4} (s : Finset ι) (f : ιK) {j : ι} (hjs : j s) (hjf : f j 0) :
∃ (a : K), (∀ is, IsLocalization.IsInteger A (a * f i)) is, a * f iJ

Strengthening of IsLocalization.exist_integer_multiples: Let J ≠ ⊤ be an ideal in a Dedekind domain A, and f ≠ 0 a finite collection of elements of K = Frac(A), then we can multiply the elements of f by some a : K to find a collection of elements of A that is not completely contained in J.

@[deprecated Ideal.exist_integer_multiples_notMem (since := "2025-05-23")]
theorem Ideal.exist_integer_multiples_not_mem {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDedekindDomain A] [Algebra A K] [IsFractionRing A K] {J : Ideal A} (hJ : J ) {ι : Type u_4} (s : Finset ι) (f : ιK) {j : ι} (hjs : j s) (hjf : f j 0) :
∃ (a : K), (∀ is, IsLocalization.IsInteger A (a * f i)) is, a * f iJ

Alias of Ideal.exist_integer_multiples_notMem.


Strengthening of IsLocalization.exist_integer_multiples: Let J ≠ ⊤ be an ideal in a Dedekind domain A, and f ≠ 0 a finite collection of elements of K = Frac(A), then we can multiply the elements of f by some a : K to find a collection of elements of A that is not completely contained in J.

theorem Ideal.mul_iInf {A : Type u_2} [CommRing A] [IsDedekindDomain A] (I : Ideal A) {ι : Type u_4} [Nonempty ι] (J : ιIdeal A) :
I * ⨅ (i : ι), J i = ⨅ (i : ι), I * J i
theorem Ideal.iInf_mul {A : Type u_2} [CommRing A] [IsDedekindDomain A] (I : Ideal A) {ι : Type u_4} [Nonempty ι] (J : ιIdeal A) :
(⨅ (i : ι), J i) * I = ⨅ (i : ι), J i * I
theorem Ideal.mul_inf {A : Type u_2} [CommRing A] [IsDedekindDomain A] (I J K : Ideal A) :
I * (JK) = I * JI * K
theorem Ideal.inf_mul {A : Type u_2} [CommRing A] [IsDedekindDomain A] (I J K : Ideal A) :
(IJ) * K = I * KJ * K
theorem FractionalIdeal.mul_inf {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDedekindDomain A] [Algebra A K] [IsFractionRing A K] (I J K✝ : FractionalIdeal (nonZeroDivisors A) K) :
I * (JK✝) = I * JI * K✝
theorem FractionalIdeal.inf_mul {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDedekindDomain A] [Algebra A K] [IsFractionRing A K] (I J K✝ : FractionalIdeal (nonZeroDivisors A) K) :
(IJ) * K✝ = I * K✝J * K✝

GCD and LCM of ideals in a Dedekind domain #

We show that the gcd of two ideals in a Dedekind domain is just their supremum, and the lcm is their infimum, and use this to instantiate NormalizedGCDMonoid (Ideal A).

@[simp]
theorem Ideal.sup_mul_inf {A : Type u_2} [CommRing A] [IsDedekindDomain A] (I J : Ideal A) :
(IJ) * (IJ) = I * J

Ideals in a Dedekind domain have gcd and lcm operators that (trivially) are compatible with the normalization operator.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Ideal.gcd_eq_sup {A : Type u_2} [CommRing A] [IsDedekindDomain A] (I J : Ideal A) :
gcd I J = IJ
@[simp]
theorem Ideal.lcm_eq_inf {A : Type u_2} [CommRing A] [IsDedekindDomain A] (I J : Ideal A) :
lcm I J = IJ
theorem Ideal.isCoprime_iff_gcd {A : Type u_2} [CommRing A] [IsDedekindDomain A] {I J : Ideal A} :
IsCoprime I J gcd I J = 1
theorem FractionalIdeal.sup_mul_inf {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDedekindDomain A] [Algebra A K] [IsFractionRing A K] (I J : FractionalIdeal (nonZeroDivisors A) K) :
(IJ) * (IJ) = I * J
theorem irreducible_pow_sup {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I J : Ideal T} [DecidableEq (Ideal T)] (hI : I ) (hJ : Irreducible J) (n : ) :
theorem irreducible_pow_sup_of_le {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I J : Ideal T} (hJ : Irreducible J) (n : ) (hn : n emultiplicity J I) :
J ^ nI = J ^ n
theorem irreducible_pow_sup_of_ge {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I J : Ideal T} (hI : I ) (hJ : Irreducible J) (n : ) (hn : emultiplicity J I n) :
J ^ nI = J ^ multiplicity J I
theorem Ideal.eq_prime_pow_mul_coprime {T : Type u_4} [CommRing T] [IsDedekindDomain T] [DecidableEq (Ideal T)] {I : Ideal T} (hI : I ) (P : Ideal T) [hpm : P.IsMaximal] :

Height one spectrum of a Dedekind domain #

If R is a Dedekind domain of Krull dimension 1, the maximal ideals of R are exactly its nonzero prime ideals. We define HeightOneSpectrum and provide lemmas to recover the facts that prime ideals of height one are prime and irreducible.

The height one prime spectrum of a Dedekind domain R is the type of nonzero prime ideals of R. Note that this equals the maximal spectrum if R has Krull dimension 1.

Instances For
    theorem IsDedekindDomain.HeightOneSpectrum.ext {R : Type u_1} {inst✝ : CommRing R} {x y : HeightOneSpectrum R} (asIdeal : x.asIdeal = y.asIdeal) :
    x = y

    An equivalence between the height one and maximal spectra for rings of Krull dimension 1.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      An ideal of R is not the whole ring if and only if it is contained in an element of HeightOneSpectrum R

      A Dedekind domain is equal to the intersection of its localizations at all its height one non-zero prime ideals viewed as subalgebras of its field of fractions.

      def idealFactorsFunOfQuotHom {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [IsDedekindDomain A] {I : Ideal R} {J : Ideal A} {f : R I →+* A J} (hf : Function.Surjective f) :
      { p : Ideal R // p I } →o { p : Ideal A // p J }

      The map from ideals of R dividing I to the ideals of A dividing J induced by a homomorphism f : R/I →+* A/J

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem idealFactorsFunOfQuotHom_coe_coe {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [IsDedekindDomain A] {I : Ideal R} {J : Ideal A} {f : R I →+* A J} (hf : Function.Surjective f) (X : { p : Ideal R // p I }) :
        theorem idealFactorsFunOfQuotHom_comp {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [IsDedekindDomain A] {I : Ideal R} {J : Ideal A} {B : Type u_4} [CommRing B] [IsDedekindDomain B] {L : Ideal B} {f : R I →+* A J} {g : A J →+* B L} (hf : Function.Surjective f) (hg : Function.Surjective g) :
        def idealFactorsEquivOfQuotEquiv {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [IsDedekindDomain A] {I : Ideal R} {J : Ideal A} [IsDedekindDomain R] (f : R I ≃+* A J) :
        {p : Ideal R | p I} ≃o {p : Ideal A | p J}

        The bijection between ideals of R dividing I and the ideals of A dividing J induced by an isomorphism f : R/I ≅ A/J.

        Equations
        Instances For
          theorem idealFactorsEquivOfQuotEquiv_is_dvd_iso {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [IsDedekindDomain A] {I : Ideal R} {J : Ideal A} [IsDedekindDomain R] (f : R I ≃+* A J) {L M : Ideal R} (hL : L I) (hM : M I) :

          The bijection between the sets of normalized factors of I and J induced by a ring isomorphism f : R/I ≅ A/J.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem Ring.DimensionLeOne.prime_le_prime_iff_eq {R : Type u_1} [CommRing R] [DimensionLEOne R] {P Q : Ideal R} [hP : P.IsPrime] [hQ : Q.IsPrime] (hP0 : P ) :
            P Q P = Q
            theorem Ideal.IsPrime.mul_mem_pow {R : Type u_1} [CommRing R] [IsDedekindDomain R] (I : Ideal R) [hI : I.IsPrime] {a b : R} {n : } (h : a * b I ^ n) :
            a I b I ^ n
            theorem Ideal.IsPrime.mem_pow_mul {R : Type u_1} [CommRing R] [IsDedekindDomain R] (I : Ideal R) [hI : I.IsPrime] {a b : R} {n : } (h : a * b I ^ n) :
            a I ^ n b I
            theorem Ideal.count_normalizedFactors_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] {p x : Ideal R} [hp : p.IsPrime] {n : } (hle : x p ^ n) [DecidableEq (Ideal R)] (hlt : ¬x p ^ (n + 1)) :

            The number of times an ideal I occurs as normalized factor of another ideal J is stable when regarding these ideals as associated elements of the monoid of ideals.

            theorem Ideal.count_associates_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] [DecidableEq (Associates (Ideal R))] [(p : Associates (Ideal R)) → Decidable (Irreducible p)] {a a₀ x : R} {n : } (hx : Prime x) (ha : ¬x a) (heq : a₀ = x ^ n * a) :

            Variant of UniqueFactorizationMonoid.count_normalizedFactors_eq for associated Ideals.

            theorem Ideal.count_associates_eq' {R : Type u_1} [CommRing R] [IsDedekindDomain R] [DecidableEq (Associates (Ideal R))] [(p : Associates (Ideal R)) → Decidable (Irreducible p)] {a x : R} (hx : Prime x) {n : } (hle : x ^ n a) (hlt : ¬x ^ (n + 1) a) :

            Variant of UniqueFactorizationMonoid.count_normalizedFactors_eq for associated Ideals.

            theorem Ideal.le_mul_of_no_prime_factors {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I J K : Ideal R} (coprime : ∀ (P : Ideal R), J PK P¬P.IsPrime) (hJ : I J) (hK : I K) :
            I J * K
            theorem IsDedekindDomain.inf_prime_pow_eq_prod {R : Type u_1} [CommRing R] [IsDedekindDomain R] {ι : Type u_4} (s : Finset ι) (f : ιIdeal R) (e : ι) (prime : is, Prime (f i)) (coprime : is, js, i jf i f j) :
            (s.inf fun (i : ι) => f i ^ e i) = is, f i ^ e i

            The intersection of distinct prime powers in a Dedekind domain is the product of these prime powers.

            noncomputable def IsDedekindDomain.quotientEquivPiOfProdEq {R : Type u_1} [CommRing R] [IsDedekindDomain R] {ι : Type u_4} [Fintype ι] (I : Ideal R) (P : ιIdeal R) (e : ι) (prime : ∀ (i : ι), Prime (P i)) (coprime : Pairwise fun (i j : ι) => P i P j) (prod_eq : i : ι, P i ^ e i = I) :
            R I ≃+* ((i : ι) → R P i ^ e i)

            Chinese remainder theorem for a Dedekind domain: if the ideal I factors as ∏ i, P i ^ e i, then R ⧸ I factors as Π i, R ⧸ (P i ^ e i).

            Equations
            Instances For

              Chinese remainder theorem for a Dedekind domain: R ⧸ I factors as Π i, R ⧸ (P i ^ e i), where P i ranges over the prime factors of I and e i over the multiplicities.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                noncomputable def IsDedekindDomain.quotientEquivPiOfFinsetProdEq {R : Type u_1} [CommRing R] [IsDedekindDomain R] {ι : Type u_4} {s : Finset ι} (I : Ideal R) (P : ιIdeal R) (e : ι) (prime : is, Prime (P i)) (coprime : is, js, i jP i P j) (prod_eq : is, P i ^ e i = I) :
                R I ≃+* ((i : { x : ι // x s }) → R P i ^ e i)

                Chinese remainder theorem for a Dedekind domain: if the ideal I factors as ∏ i ∈ s, P i ^ e i, then R ⧸ I factors as Π (i : s), R ⧸ (P i ^ e i).

                This is a version of IsDedekindDomain.quotientEquivPiOfProdEq where we restrict the product to a finite subset s of a potentially infinite indexing type ι.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem IsDedekindDomain.exists_representative_mod_finset {R : Type u_1} [CommRing R] [IsDedekindDomain R] {ι : Type u_4} {s : Finset ι} (P : ιIdeal R) (e : ι) (prime : is, Prime (P i)) (coprime : is, js, i jP i P j) (x : (i : { x : ι // x s }) → R P i ^ e i) :
                  ∃ (y : R), ∀ (i : ι) (hi : i s), (Ideal.Quotient.mk (P i ^ e i)) y = x i, hi

                  Corollary of the Chinese remainder theorem: given elements x i : R / P i ^ e i, we can choose a representative y : R such that y ≡ x i (mod P i ^ e i).

                  theorem IsDedekindDomain.exists_forall_sub_mem_ideal {R : Type u_1} [CommRing R] [IsDedekindDomain R] {ι : Type u_4} {s : Finset ι} (P : ιIdeal R) (e : ι) (prime : is, Prime (P i)) (coprime : is, js, i jP i P j) (x : { x : ι // x s }R) :
                  ∃ (y : R), ∀ (i : ι) (hi : i s), y - x i, hi P i ^ e i

                  Corollary of the Chinese remainder theorem: given elements x i : R, we can choose a representative y : R such that y - x i ∈ P i ^ e i.

                  The bijection between the (normalized) prime factors of r and the (normalized) prime factors of span {r}

                  Equations
                  Instances For

                    The bijection normalizedFactorsEquivSpanNormalizedFactors between the set of prime factors of r and the set of prime factors of the ideal ⟨r⟩ preserves multiplicities. See count_normalizedFactorsSpan_eq_count for the version stated in terms of multisets count.

                    The bijection normalized_factors_equiv_span_normalized_factors.symm between the set of prime factors of the ideal ⟨r⟩ and the set of prime factors of r preserves multiplicities.

                    The bijection between the set of prime factors of the ideal ⟨r⟩ and the set of prime factors of r preserves count of the corresponding multisets. See multiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_multiplicity for the version stated in terms of multiplicity.

                    @[reducible, inline]
                    noncomputable abbrev primesOverFinset {A : Type u_4} [CommRing A] (p : Ideal A) (B : Type u_5) [CommRing B] [IsDedekindDomain B] [Algebra A B] :

                    The finite set of all prime factors of the pushforward of p.

                    Equations
                    Instances For
                      theorem coe_primesOverFinset {A : Type u_4} [CommRing A] {p : Ideal A} (hpb : p ) [hpm : p.IsMaximal] (B : Type u_5) [CommRing B] [IsDedekindDomain B] [Algebra A B] [NoZeroSMulDivisors A B] :
                      theorem primesOver_finite {A : Type u_4} [CommRing A] (p : Ideal A) [hpm : p.IsMaximal] (B : Type u_5) [CommRing B] [IsDedekindDomain B] [Algebra A B] [NoZeroSMulDivisors A B] [Algebra.IsIntegral A B] :
                      theorem primesOver_ncard_ne_zero {A : Type u_4} [CommRing A] (p : Ideal A) [hpm : p.IsMaximal] (B : Type u_5) [CommRing B] [IsDedekindDomain B] [Algebra A B] [NoZeroSMulDivisors A B] [Algebra.IsIntegral A B] :
                      theorem one_le_primesOver_ncard {A : Type u_4} [CommRing A] (p : Ideal A) [hpm : p.IsMaximal] (B : Type u_5) [CommRing B] [IsDedekindDomain B] [Algebra A B] [NoZeroSMulDivisors A B] [Algebra.IsIntegral A B] :