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

• IsDedekindDomain.HeightOneSpectrum defines the type of nonzero prime ideals of R.

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.

TODO

In #38133, many declarations were moved from the root namespace into Ideal or IsDedekindDomain. The deprecations have the effect that downstream files now have to use the fully qualified name even when the corresponding namespace is opened.

After the deprecations have been removed, the shorter names can be restored:

• In Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind:
  • Ideal.span_singleton_dvd_span_singleton_iff_dvd → span_singleton_dvd_span_singleton_iff_dvd in line 75 (as of 2026-04-17)
  • Ideal.normalizedFactorsEquivSpanNormalizedFactors → normalizedFactorsEquivSpanNormalizedFactors in line 115
  • Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity → emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity in line 129
  • Ideal.normalizedFactorsEquivSpanNormalizedFactors → normalizedFactorsEquivSpanNormalizedFactors in line 221
• In Mathlib.NumberTheory.NumberField.ClassNumber:
  • Ideal.prod_normalizedFactors_eq_self → prod_normalizedFactors_eq_self in line 122
• In Mathlib.NumberTheory.RamificationInertia.Basic, one could add open IsDedekindDomain around line 498 and then remove many IsDedekindDomain. prefixes below.

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

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)⁻¹, x ∉ 1

@[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) : P.IsPrime

theorem Ideal.prime_of_isPrime {A : Type u_2} [CommRing A] [IsDedekindDomain A] {P : Ideal A} (hP : P ≠ ⊥) (h : P.IsPrime) : Prime P

theorem Ideal.prime_of_mem_primesOver {A : Type u_2} [CommRing A] [IsDedekindDomain A] {R : Type u_4} [CommRing R] [Algebra R A] {p : Ideal R} [IsDomain R] [Module.IsTorsionFree R A] (hp : p ≠ ⊥) {P : Ideal A} (hP : P ∈ p.primesOver A) : Prime P

theorem Ideal.prime_iff_isPrime {A : Type u_2} [CommRing A] [IsDedekindDomain A] {P : Ideal A} (hP : P ≠ ⊥) : Prime P ↔ P.IsPrime

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

theorem Ideal.isPrime_iff_bot_or_prime {A : Type u_2} [CommRing A] [IsDedekindDomain A] {P : Ideal A} : P.IsPrime ↔ P = ⊥ ∨ Prime P

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.prime_span_singleton_iff {A : Type u_2} [CommRing A] [IsDedekindDomain A] {a : A} : Prime (span {a}) ↔ Prime a

theorem Ideal.prime_generator_of_prime {A : Type u_2} [CommRing A] [IsDedekindDomain A] {P : Ideal A} (h : Prime P) [Submodule.IsPrincipal P] : Prime (Submodule.IsPrincipal.generator P)

theorem Ideal.mem_normalizedFactors_iff {A : Type u_2} [CommRing A] [IsDedekindDomain A] {p I : Ideal A} (hI : I ≠ ⊥) : p ∈ UniqueFactorizationMonoid.normalizedFactors I ↔ p.IsPrime ∧ I ≤ p

theorem Ideal.mem_primesOver_iff_mem_normalizedFactors {R : Type u_1} (A : Type u_2) [CommRing R] [CommRing A] [IsDedekindDomain A] {p : Ideal R} [h : p.IsMaximal] [Algebra R A] [IsDomain R] [Module.IsTorsionFree R A] (hp : p ≠ ⊥) {P : Ideal A} : P ∈ p.primesOver A ↔ P ∈ UniqueFactorizationMonoid.normalizedFactors (map (algebraMap R A) p)

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 : ℕ) : ∃ x ∈ I ^ e, x ∉ I ^ (e + 1)

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 Associates.le_singleton_iff {A : Type u_2} [CommRing A] [IsDedekindDomain A] (x : A) (n : ℕ) (I : Ideal A) : Associates.mk I ^ n ≤ Associates.mk (Ideal.span {x}) ↔ x ∈ I ^ n

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) : I ≤ J⁻¹ ↔ J ≤ I⁻¹

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) : I⁻¹ ≤ J ↔ J⁻¹ ≤ I

@[simp]

theorem FractionalIdeal.inv_le_inv_iff {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) : I⁻¹ ≤ J⁻¹ ↔ J ≤ I

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), (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ ↑J

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 * (J ⊓ K) = I * J ⊓ I * K

theorem Ideal.inf_mul {A : Type u_2} [CommRing A] [IsDedekindDomain A] (I J K : Ideal A) : (I ⊓ J) * K = I * K ⊓ J * 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 * (J ⊓ K✝) = I * J ⊓ I * 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) : (I ⊓ J) * 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) : (I ⊔ J) * (I ⊓ J) = I * J

@[implicit_reducible]

noncomputable instance Ideal.instNormalizedGCDMonoid {A : Type u_2} [CommRing A] [IsDedekindDomain A] : NormalizedGCDMonoid (Ideal A)

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 = I ⊔ J

@[simp]

theorem Ideal.lcm_eq_inf {A : Type u_2} [CommRing A] [IsDedekindDomain A] (I J : Ideal A) : lcm I J = I ⊓ J

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 Ideal.factors_span_eq {K : Type u_3} [Field K] {p : Polynomial K} : UniqueFactorizationMonoid.factors (span {p}) = Multiset.map (fun (q : Polynomial K) => span {q}) (UniqueFactorizationMonoid.factors p)

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) : (I ⊓ J) * (I ⊔ J) = I * J

theorem Ideal.prod_normalizedFactors_eq_self {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I : Ideal T} (hI : I ≠ ⊥) : (UniqueFactorizationMonoid.normalizedFactors I).prod = I

@[deprecated Ideal.prod_normalizedFactors_eq_self (since := "2026-04-16")]

theorem prod_normalizedFactors_eq_self {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I : Ideal T} (hI : I ≠ ⊥) : (UniqueFactorizationMonoid.normalizedFactors I).prod = I

Alias of Ideal.prod_normalizedFactors_eq_self.

theorem Ideal.count_le_of_ideal_ge {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I J : Ideal T} (h : I ≤ J) (hI : I ≠ ⊥) (K : Ideal T) : Multiset.count K (UniqueFactorizationMonoid.normalizedFactors J) ≤ Multiset.count K (UniqueFactorizationMonoid.normalizedFactors I)

@[deprecated Ideal.count_le_of_ideal_ge (since := "2026-04-16")]

theorem count_le_of_ideal_ge {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I J : Ideal T} (h : I ≤ J) (hI : I ≠ ⊥) (K : Ideal T) : Multiset.count K (UniqueFactorizationMonoid.normalizedFactors J) ≤ Multiset.count K (UniqueFactorizationMonoid.normalizedFactors I)

Alias of Ideal.count_le_of_ideal_ge.

theorem Ideal.sup_eq_prod_inf_factors {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I J : Ideal T} (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : I ⊔ J = (UniqueFactorizationMonoid.normalizedFactors I ∩ UniqueFactorizationMonoid.normalizedFactors J).prod

@[deprecated Ideal.sup_eq_prod_inf_factors (since := "2026-04-16")]

theorem sup_eq_prod_inf_factors {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I J : Ideal T} (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : I ⊔ J = (UniqueFactorizationMonoid.normalizedFactors I ∩ UniqueFactorizationMonoid.normalizedFactors J).prod

Alias of Ideal.sup_eq_prod_inf_factors.

theorem Ideal.irreducible_pow_sup {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I J : Ideal T} (hI : I ≠ ⊥) (hJ : Irreducible J) (n : ℕ) : J ^ n ⊔ I = J ^ min (Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)) n

@[deprecated Ideal.irreducible_pow_sup (since := "2026-04-16")]

theorem irreducible_pow_sup {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I J : Ideal T} (hI : I ≠ ⊥) (hJ : Irreducible J) (n : ℕ) : J ^ n ⊔ I = J ^ min (Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)) n

Alias of Ideal.irreducible_pow_sup.

theorem Ideal.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 ^ n ⊔ I = J ^ n

@[deprecated Ideal.irreducible_pow_sup_of_le (since := "2026-04-16")]

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 ^ n ⊔ I = J ^ n

Alias of Ideal.irreducible_pow_sup_of_le.

theorem Ideal.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 ^ n ⊔ I = J ^ multiplicity J I

@[deprecated Ideal.irreducible_pow_sup_of_ge (since := "2026-04-16")]

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 ^ n ⊔ I = J ^ multiplicity J I

Alias of Ideal.irreducible_pow_sup_of_ge.

theorem Ideal.eq_prime_pow_mul_coprime {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I : Ideal T} (hI : I ≠ ⊥) (P : Ideal T) [hpm : P.IsMaximal] : ∃ (Q : Ideal T), P ⊔ Q = ⊤ ∧ I = P ^ Multiset.count P (UniqueFactorizationMonoid.normalizedFactors I) * Q

theorem Ideal.map_prime_of_equiv {T : Type u_4} [CommRing T] [IsDedekindDomain T] {R : Type u_5} [CommRing R] [IsDedekindDomain R] (f : T ≃+* R) {I : Ideal T} (hI : Prime I) (h : I ≠ ⊥) : Prime (map f I)

@[deprecated Ideal.map_prime_of_equiv (since := "2026-04-16")]

theorem map_prime_of_equiv {T : Type u_4} [CommRing T] [IsDedekindDomain T] {R : Type u_5} [CommRing R] [IsDedekindDomain R] (f : T ≃+* R) {I : Ideal T} (hI : Prime I) (h : I ≠ ⊥) : Prime (Ideal.map f I)

Alias of Ideal.map_prime_of_equiv.

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.

structure IsDedekindDomain.HeightOneSpectrum (R : Type u_1) [CommRing R] : Type u_1

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.

• asIdeal : Ideal R
• isPrime : self.asIdeal.IsPrime
• ne_bot : self.asIdeal ≠ ⊥

theorem IsDedekindDomain.HeightOneSpectrum.ext_iff {R : Type u_1} {inst✝ : CommRing R} {x y : HeightOneSpectrum R} : x = y ↔ x.asIdeal = y.asIdeal

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

instance IsDedekindDomain.HeightOneSpectrum.isMaximal {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) : v.asIdeal.IsMaximal

theorem IsDedekindDomain.HeightOneSpectrum.prime {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) : Prime v.asIdeal

@[implicit_reducible]

instance IsDedekindDomain.HeightOneSpectrum.instCoeIdeal {R : Type u_1} [CommRing R] : Coe (HeightOneSpectrum R) (Ideal R)

Equations

• IsDedekindDomain.HeightOneSpectrum.instCoeIdeal = { coe := fun (P : IsDedekindDomain.HeightOneSpectrum R) => P.asIdeal }

def IsDedekindDomain.HeightOneSpectrum.ofPrime {R : Type u_1} [CommRing R] [IsDedekindDomain R] {p : Ideal R} (hp : Prime p) : HeightOneSpectrum R

The (nonzero) prime elements of the monoid with zero Ideal R correspond to an element of type HeightOneSpectrum R.

See IsDedekindDomain.HeightOneSpectrum.prime for the inverse direction.

Equations

• IsDedekindDomain.HeightOneSpectrum.ofPrime hp = { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.ofPrime_asIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] {p : Ideal R} (hp : Prime p) : (ofPrime hp).asIdeal = p

theorem IsDedekindDomain.HeightOneSpectrum.irreducible {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) : Irreducible v.asIdeal

theorem IsDedekindDomain.HeightOneSpectrum.associates_irreducible {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) : Irreducible (Associates.mk v.asIdeal)

def IsDedekindDomain.HeightOneSpectrum.equivMaximalSpectrum {R : Type u_1} [CommRing R] [IsDedekindDomain R] (hR : ¬IsField R) : HeightOneSpectrum R ≃ MaximalSpectrum R

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.

theorem IsDedekindDomain.HeightOneSpectrum.ideal_ne_top_iff_exists {R : Type u_1} [CommRing R] [IsDedekindDomain R] (hR : ¬IsField R) (I : Ideal R) : I ≠ ⊤ ↔ ∃ (P : HeightOneSpectrum R), I ≤ P.asIdeal

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

theorem IsDedekindDomain.HeightOneSpectrum.isCoprime_of_ne {R : Type u_1} [CommRing R] [IsDedekindDomain R] (P Q : HeightOneSpectrum R) (hPQ : P ≠ Q) : IsCoprime P.asIdeal Q.asIdeal

theorem IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne {R : Type u_1} [CommRing R] [IsDedekindDomain R] (P Q : HeightOneSpectrum R) (hPQ : P ≠ Q) (n m : ℕ) : IsCoprime (P.asIdeal ^ n) (Q.asIdeal ^ m)

theorem IsDedekindDomain.HeightOneSpectrum.iInf_localization_eq_bot (R : Type u_1) (K : Type u_3) [CommRing R] [Field K] [IsDedekindDomain R] [Algebra R K] [hK : IsFractionRing R K] : ⨅ (v : HeightOneSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ = ⊥

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 IsDedekindDomain.HeightOneSpectrum.comap {R : Type u_1} [CommRing R] {S : Type u_4} [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) (v : HeightOneSpectrum S) : HeightOneSpectrum R

A surjective ring homomorphism f : R →+* S induces a map from HeightOneSpectrum S to HeightOneSpectrum R sending v to v.asIdeal.comap f.

Equations

• IsDedekindDomain.HeightOneSpectrum.comap f hf v = { asIdeal := Ideal.comap f v.asIdeal, isPrime := ⋯, ne_bot := ⋯ }

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.comap_asIdeal {R : Type u_1} [CommRing R] {S : Type u_4} [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) (v : HeightOneSpectrum S) : (comap f hf v).asIdeal = Ideal.comap f v.asIdeal

def IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv {R : Type u_1} [CommRing R] {S : Type u_4} [CommRing S] (e : R ≃+* S) : HeightOneSpectrum R ≃ HeightOneSpectrum S

The isomorphism between HeightOneSpectrums of isomorphic rings.

Equations

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

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv_symm_apply {R : Type u_1} [CommRing R] {S : Type u_4} [CommRing S] (e : R ≃+* S) (v : HeightOneSpectrum S) : (equivOfRingEquiv e).symm v = comap ↑e ⋯ v

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv_apply {R : Type u_1} [CommRing R] {S : Type u_4} [CommRing S] (e : R ≃+* S) (v : HeightOneSpectrum R) : (equivOfRingEquiv e) v = comap ↑e.symm ⋯ v

theorem IsDedekindDomain.HeightOneSpectrum.RingEquiv.nontrivial_heightOneSpectrum {R : Type u_5} {S : Type u_6} [CommRing R] [CommRing S] [Nontrivial (HeightOneSpectrum S)] (e : R ≃+* S) : Nontrivial (HeightOneSpectrum R)

def IsDedekindDomain.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.

@[simp]

theorem IsDedekindDomain.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 }) : ↑((idealFactorsFunOfQuotHom hf) X) = Ideal.comap (Ideal.Quotient.mk J) (Ideal.map f (Ideal.map (Ideal.Quotient.mk I) ↑X))

@[deprecated IsDedekindDomain.idealFactorsFunOfQuotHom (since := "2026-04-16")]

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 }

Alias of IsDedekindDomain.idealFactorsFunOfQuotHom.

---

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

• @idealFactorsFunOfQuotHom = @IsDedekindDomain.idealFactorsFunOfQuotHom

@[simp]

theorem IsDedekindDomain.idealFactorsFunOfQuotHom_id {A : Type u_2} [CommRing A] [IsDedekindDomain A] {J : Ideal A} : idealFactorsFunOfQuotHom ⋯ = OrderHom.id

@[deprecated IsDedekindDomain.idealFactorsFunOfQuotHom_id (since := "2026-04-16")]

theorem idealFactorsFunOfQuotHom_id {A : Type u_2} [CommRing A] [IsDedekindDomain A] {J : Ideal A} : IsDedekindDomain.idealFactorsFunOfQuotHom ⋯ = OrderHom.id

Alias of IsDedekindDomain.idealFactorsFunOfQuotHom_id.

theorem IsDedekindDomain.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) : (idealFactorsFunOfQuotHom hg).comp (idealFactorsFunOfQuotHom hf) = idealFactorsFunOfQuotHom ⋯

@[deprecated IsDedekindDomain.idealFactorsFunOfQuotHom_comp (since := "2026-04-16")]

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) : (IsDedekindDomain.idealFactorsFunOfQuotHom hg).comp (IsDedekindDomain.idealFactorsFunOfQuotHom hf) = IsDedekindDomain.idealFactorsFunOfQuotHom ⋯

Alias of IsDedekindDomain.idealFactorsFunOfQuotHom_comp.

def IsDedekindDomain.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

• IsDedekindDomain.idealFactorsEquivOfQuotEquiv f = OrderIso.ofHomInv (IsDedekindDomain.idealFactorsFunOfQuotHom ⋯) (IsDedekindDomain.idealFactorsFunOfQuotHom ⋯) ⋯ ⋯

@[deprecated IsDedekindDomain.idealFactorsEquivOfQuotEquiv (since := "2026-04-16")]

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}

Alias of IsDedekindDomain.idealFactorsEquivOfQuotEquiv.

---

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

• @idealFactorsEquivOfQuotEquiv = @IsDedekindDomain.idealFactorsEquivOfQuotEquiv

theorem IsDedekindDomain.idealFactorsEquivOfQuotEquiv_symm {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) : (idealFactorsEquivOfQuotEquiv f).symm = idealFactorsEquivOfQuotEquiv f.symm

@[deprecated IsDedekindDomain.idealFactorsEquivOfQuotEquiv_symm (since := "2026-04-16")]

theorem idealFactorsEquivOfQuotEquiv_symm {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) : (IsDedekindDomain.idealFactorsEquivOfQuotEquiv f).symm = IsDedekindDomain.idealFactorsEquivOfQuotEquiv f.symm

Alias of IsDedekindDomain.idealFactorsEquivOfQuotEquiv_symm.

theorem IsDedekindDomain.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) : ↑((idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩) ∣ ↑((idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩) ↔ L ∣ M

@[deprecated IsDedekindDomain.idealFactorsEquivOfQuotEquiv_is_dvd_iso (since := "2026-04-16")]

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) : ↑((IsDedekindDomain.idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩) ∣ ↑((IsDedekindDomain.idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩) ↔ L ∣ M

Alias of IsDedekindDomain.idealFactorsEquivOfQuotEquiv_is_dvd_iso.

theorem IsDedekindDomain.idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors {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) (hJ : J ≠ ⊥) {L : Ideal R} (hL : L ∈ UniqueFactorizationMonoid.normalizedFactors I) : ↑((idealFactorsEquivOfQuotEquiv f) ⟨L, ⋯⟩) ∈ UniqueFactorizationMonoid.normalizedFactors J

@[deprecated IsDedekindDomain.idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors (since := "2026-04-16")]

theorem idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors {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) (hJ : J ≠ ⊥) {L : Ideal R} (hL : L ∈ UniqueFactorizationMonoid.normalizedFactors I) : ↑((IsDedekindDomain.idealFactorsEquivOfQuotEquiv f) ⟨L, ⋯⟩) ∈ UniqueFactorizationMonoid.normalizedFactors J

Alias of IsDedekindDomain.idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors.

def IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv {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) (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : ↑{L : Ideal R | L ∈ UniqueFactorizationMonoid.normalizedFactors I} ≃ ↑{M : Ideal A | M ∈ UniqueFactorizationMonoid.normalizedFactors J}

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.

@[deprecated IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv (since := "2026-04-16")]

def normalizedFactorsEquivOfQuotEquiv {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) (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : ↑{L : Ideal R | L ∈ UniqueFactorizationMonoid.normalizedFactors I} ≃ ↑{M : Ideal A | M ∈ UniqueFactorizationMonoid.normalizedFactors J}

Alias of IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv.

---

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

Equations

• @normalizedFactorsEquivOfQuotEquiv = @IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv

@[simp]

theorem IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_symm {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) (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : (normalizedFactorsEquivOfQuotEquiv f hI hJ).symm = normalizedFactorsEquivOfQuotEquiv f.symm hJ hI

@[deprecated IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_symm (since := "2026-04-16")]

theorem normalizedFactorsEquivOfQuotEquiv_symm {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) (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : (IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv f hI hJ).symm = IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv f.symm hJ hI

Alias of IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_symm.

theorem IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity {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) (hI : I ≠ ⊥) (hJ : J ≠ ⊥) (L : Ideal R) (hL : L ∈ UniqueFactorizationMonoid.normalizedFactors I) : emultiplicity (↑((normalizedFactorsEquivOfQuotEquiv f hI hJ) ⟨L, hL⟩)) J = emultiplicity L I

The map normalizedFactorsEquivOfQuotEquiv preserves multiplicities.

@[deprecated IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity (since := "2026-04-16")]

theorem normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity {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) (hI : I ≠ ⊥) (hJ : J ≠ ⊥) (L : Ideal R) (hL : L ∈ UniqueFactorizationMonoid.normalizedFactors I) : emultiplicity (↑((IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv f hI hJ) ⟨L, hL⟩)) J = emultiplicity L I

Alias of IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity.

---

The map normalizedFactorsEquivOfQuotEquiv preserves multiplicities.

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

See also Ideal.IsMaximal.mul_mem_pow for maximal ideal.

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

See also Ideal.IsMaximal.mem_pow_mul for maximal ideal.

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) (hlt : ¬x ≤ p ^ (n + 1)) : Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n

theorem Ideal.count_associates_factors_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I J : Ideal R} (hI : I ≠ 0) (hJ : J.IsPrime) (hJ₀ : J ≠ ⊥) : (Associates.mk J).count (Associates.mk I).factors = Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)

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.

@[deprecated Ideal.count_associates_factors_eq (since := "2026-04-16")]

theorem count_associates_factors_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I J : Ideal R} (hI : I ≠ 0) (hJ : J.IsPrime) (hJ₀ : J ≠ ⊥) : (Associates.mk J).count (Associates.mk I).factors = Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)

Alias of Ideal.count_associates_factors_eq.

---

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] {a a₀ x : R} {n : ℕ} (hx : Prime x) (ha : ¬x ∣ a) (heq : a₀ = x ^ n * a) : (Associates.mk (span {x})).count (Associates.mk (span {a₀})).factors = n

Variant of UniqueFactorizationMonoid.count_normalizedFactors_eq for associated Ideals.

theorem Ideal.count_associates_eq' {R : Type u_1} [CommRing R] [IsDedekindDomain R] {a x : R} (hx : Prime x) {n : ℕ} (hle : x ^ n ∣ a) (hlt : ¬x ^ (n + 1) ∣ a) : (Associates.mk (span {x})).count (Associates.mk (span {a})).factors = n

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 ≤ P → K ≤ P → ¬P.IsPrime) (hJ : I ≤ J) (hK : I ≤ K) : I ≤ J * K

theorem IsDedekindDomain.HeightOneSpectrum.inf_pow_eq_prod {R : Type u_1} [CommRing R] {ι : Type u_4} [IsDedekindDomain R] (s : Finset ι) (e : ι → ℕ) (f : ι → HeightOneSpectrum R) (coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j) : (s.inf fun (i : ι) => (f i).asIdeal ^ e i) = ∏ i ∈ s, (f i).asIdeal ^ e i

The intersection of distinct prime powers in a Dedekind domain is the product of these prime powers. See IsDedekindDomain.inf_pow_eq_prod_of_prime for the version in terms of Ideal R.

theorem IsDedekindDomain.inf_pow_eq_prod_of_prime {R : Type u_1} [CommRing R] {ι : Type u_4} [IsDedekindDomain R] (s : Finset ι) (f : ι → Ideal R) (e : ι → ℕ) (prime : ∀ i ∈ s, Prime (f i)) (coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j) : (s.inf fun (i : ι) => f i ^ e i) = ∏ i ∈ s, f i ^ e i

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

@[deprecated IsDedekindDomain.inf_pow_eq_prod_of_prime (since := "2026-03-10")]

theorem IsDedekindDomain.inf_prime_pow_eq_prod {R : Type u_1} [CommRing R] {ι : Type u_4} [IsDedekindDomain R] (s : Finset ι) (f : ι → Ideal R) (e : ι → ℕ) (prime : ∀ i ∈ s, Prime (f i)) (coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j) : (s.inf fun (i : ι) => f i ^ e i) = ∏ i ∈ s, f i ^ e i

Alias of IsDedekindDomain.inf_pow_eq_prod_of_prime.

---

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

noncomputable def IsDedekindDomain.HeightOneSpectrum.quotientEquivPiOfProdEq {R : Type u_1} [CommRing R] {ι : Type u_4} [IsDedekindDomain R] [Fintype ι] (I : Ideal R) (P : ι → HeightOneSpectrum R) (e : ι → ℕ) (coprime : Pairwise fun (i j : ι) => P i ≠ P j) (prod_eq : ∏ i : ι, (P i).asIdeal ^ e i = I) : R ⧸ I ≃+* ((i : ι) → R ⧸ (P i).asIdeal ^ 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). See IsDedekindDomain.quotientEquivPiOfProdEq for the version in terms of Ideal R.

Equations

• IsDedekindDomain.HeightOneSpectrum.quotientEquivPiOfProdEq I P e coprime prod_eq = (Ideal.quotEquivOfEq ⋯).trans (Ideal.quotientInfRingEquivPiQuotient (fun (i : ι) => (P i).asIdeal ^ e i) ⋯)

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

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

noncomputable def IsDedekindDomain.quotientEquivPiFactors {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ ⊥) : R ⧸ I ≃+* ((P : ↥(UniqueFactorizationMonoid.factors I).toFinset) → R ⧸ ↑P ^ Multiset.count (↑P) (UniqueFactorizationMonoid.factors I))

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.

@[simp]

theorem IsDedekindDomain.quotientEquivPiFactors_mk {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ ⊥) (x : R) : (quotientEquivPiFactors hI) ((Ideal.Quotient.mk I) x) = fun (_P : ↥(UniqueFactorizationMonoid.factors I).toFinset) => (Ideal.Quotient.mk (↑_P ^ Multiset.count (↑_P) (UniqueFactorizationMonoid.factors I))) x

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 : ∀ i ∈ s, Prime (P i)) (coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j) (prod_eq : ∏ i ∈ s, P i ^ e i = I) : R ⧸ I ≃+* ((i : ↥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

• IsDedekindDomain.quotientEquivPiOfFinsetProdEq I P e prime coprime prod_eq = IsDedekindDomain.quotientEquivPiOfProdEq I (fun (i : ↥s) => P ↑i) (fun (i : ↥s) => e ↑i) ⋯ ⋯ ⋯

theorem IsDedekindDomain.exists_representative_mod_finset {R : Type u_1} [CommRing R] [IsDedekindDomain R] {ι : Type u_4} {s : Finset ι} (P : ι → Ideal R) (e : ι → ℕ) (prime : ∀ i ∈ s, Prime (P i)) (coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j) (x : (i : ↥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 : ∀ i ∈ s, Prime (P i)) (coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j) (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.

theorem Ideal.span_singleton_dvd_span_singleton_iff_dvd {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a b : R} : span {a} ∣ span {b} ↔ a ∣ b

@[deprecated Ideal.span_singleton_dvd_span_singleton_iff_dvd (since := "2026-04-16")]

theorem span_singleton_dvd_span_singleton_iff_dvd {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a b : R} : Ideal.span {a} ∣ Ideal.span {b} ↔ a ∣ b

Alias of Ideal.span_singleton_dvd_span_singleton_iff_dvd.

@[simp]

theorem Ideal.squarefree_span_singleton {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a : R} : Squarefree (span {a}) ↔ Squarefree a

theorem Ideal.singleton_span_mem_normalizedFactors_of_mem_normalizedFactors {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] {a b : R} (ha : a ∈ UniqueFactorizationMonoid.normalizedFactors b) : span {a} ∈ UniqueFactorizationMonoid.normalizedFactors (span {b})

@[deprecated Ideal.singleton_span_mem_normalizedFactors_of_mem_normalizedFactors (since := "2026-04-16")]

theorem singleton_span_mem_normalizedFactors_of_mem_normalizedFactors {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] {a b : R} (ha : a ∈ UniqueFactorizationMonoid.normalizedFactors b) : Ideal.span {a} ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.span {b})

Alias of Ideal.singleton_span_mem_normalizedFactors_of_mem_normalizedFactors.

theorem Ideal.emultiplicity_eq_emultiplicity_span {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a b : R} : emultiplicity (span {a}) (span {b}) = emultiplicity a b

@[deprecated Ideal.emultiplicity_eq_emultiplicity_span (since := "2026-04-16")]

theorem emultiplicity_eq_emultiplicity_span {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a b : R} : emultiplicity (Ideal.span {a}) (Ideal.span {b}) = emultiplicity a b

Alias of Ideal.emultiplicity_eq_emultiplicity_span.

noncomputable def Ideal.normalizedFactorsEquivSpanNormalizedFactors {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] {r : R} (hr : r ≠ 0) : ↑{d : R | d ∈ UniqueFactorizationMonoid.normalizedFactors r} ≃ ↑{I : Ideal R | I ∈ UniqueFactorizationMonoid.normalizedFactors (span {r})}

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

Equations

• Ideal.normalizedFactorsEquivSpanNormalizedFactors hr = Equiv.ofBijective (fun (d : ↑{d : R | d ∈ UniqueFactorizationMonoid.normalizedFactors r}) => ⟨Ideal.span {↑d}, ⋯⟩) ⋯

@[deprecated Ideal.normalizedFactorsEquivSpanNormalizedFactors (since := "2026-04-16")]

def normalizedFactorsEquivSpanNormalizedFactors {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] {r : R} (hr : r ≠ 0) : ↑{d : R | d ∈ UniqueFactorizationMonoid.normalizedFactors r} ≃ ↑{I : Ideal R | I ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})}

Alias of Ideal.normalizedFactorsEquivSpanNormalizedFactors.

---

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

Equations

• @normalizedFactorsEquivSpanNormalizedFactors = @Ideal.normalizedFactorsEquivSpanNormalizedFactors

theorem Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] {r d : R} (hr : r ≠ 0) (hd : d ∈ UniqueFactorizationMonoid.normalizedFactors r) : emultiplicity d r = emultiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr) ⟨d, hd⟩)) (span {r})

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.

@[deprecated Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity (since := "2026-04-16")]

theorem emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] {r d : R} (hr : r ≠ 0) (hd : d ∈ UniqueFactorizationMonoid.normalizedFactors r) : emultiplicity d r = emultiplicity (↑((Ideal.normalizedFactorsEquivSpanNormalizedFactors hr) ⟨d, hd⟩)) (Ideal.span {r})

Alias of Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity.

---

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.

theorem Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] {r : R} (hr : r ≠ 0) (I : ↑{I : Ideal R | I ∈ UniqueFactorizationMonoid.normalizedFactors (span {r})}) : emultiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = emultiplicity (↑I) (span {r})

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.

@[deprecated Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity (since := "2026-04-16")]

theorem emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] {r : R} (hr : r ≠ 0) (I : ↑{I : Ideal R | I ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})}) : emultiplicity (↑((Ideal.normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = emultiplicity (↑I) (Ideal.span {r})

Alias of Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity.

---

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.

theorem Ideal.count_span_normalizedFactors_eq {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] [DecidableEq R] {r X : R} (hr : r ≠ 0) (hX : Prime X) : Multiset.count (span {X}) (UniqueFactorizationMonoid.normalizedFactors (span {r})) = Multiset.count (normalize X) (UniqueFactorizationMonoid.normalizedFactors r)

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.

@[deprecated Ideal.count_span_normalizedFactors_eq (since := "2026-04-16")]

theorem count_span_normalizedFactors_eq {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] [DecidableEq R] {r X : R} (hr : r ≠ 0) (hX : Prime X) : Multiset.count (Ideal.span {X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})) = Multiset.count (normalize X) (UniqueFactorizationMonoid.normalizedFactors r)

Alias of Ideal.count_span_normalizedFactors_eq.

---

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.

theorem Ideal.count_span_normalizedFactors_eq_of_normUnit {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] [DecidableEq R] {r X : R} (hr : r ≠ 0) (hX₁ : normUnit X = 1) (hX : Prime X) : Multiset.count (span {X}) (UniqueFactorizationMonoid.normalizedFactors (span {r})) = Multiset.count X (UniqueFactorizationMonoid.normalizedFactors r)

@[deprecated Ideal.count_span_normalizedFactors_eq_of_normUnit (since := "2026-04-16")]

theorem count_span_normalizedFactors_eq_of_normUnit {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] [DecidableEq R] {r X : R} (hr : r ≠ 0) (hX₁ : normUnit X = 1) (hX : Prime X) : Multiset.count (Ideal.span {X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})) = Multiset.count X (UniqueFactorizationMonoid.normalizedFactors r)

Alias of Ideal.count_span_normalizedFactors_eq_of_normUnit.

@[reducible, inline]

noncomputable abbrev IsDedekindDomain.primesOverFinset {A : Type u_4} [CommRing A] (p : Ideal A) (B : Type u_5) [CommRing B] [IsDedekindDomain B] [Algebra A B] : Finset (Ideal B)

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

Equations

• IsDedekindDomain.primesOverFinset p B = (UniqueFactorizationMonoid.factors (Ideal.map (algebraMap A B) p)).toFinset

@[deprecated IsDedekindDomain.primesOverFinset (since := "2026-04-16")]

def primesOverFinset {A : Type u_4} [CommRing A] (p : Ideal A) (B : Type u_5) [CommRing B] [IsDedekindDomain B] [Algebra A B] : Finset (Ideal B)

Alias of IsDedekindDomain.primesOverFinset.

---

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

Equations

• @primesOverFinset = @IsDedekindDomain.primesOverFinset

theorem IsDedekindDomain.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] [IsDomain A] [Module.IsTorsionFree A B] : ↑(primesOverFinset p B) = p.primesOver B

@[deprecated IsDedekindDomain.coe_primesOverFinset (since := "2026-04-16")]

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] [IsDomain A] [Module.IsTorsionFree A B] : ↑(IsDedekindDomain.primesOverFinset p B) = p.primesOver B

Alias of IsDedekindDomain.coe_primesOverFinset.

theorem IsDedekindDomain.mem_primesOverFinset_iff {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] [IsDomain A] [Module.IsTorsionFree A B] {P : Ideal B} : P ∈ primesOverFinset p B ↔ P ∈ p.primesOver B

@[deprecated IsDedekindDomain.mem_primesOverFinset_iff (since := "2026-04-16")]

theorem mem_primesOverFinset_iff {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] [IsDomain A] [Module.IsTorsionFree A B] {P : Ideal B} : P ∈ IsDedekindDomain.primesOverFinset p B ↔ P ∈ p.primesOver B

Alias of IsDedekindDomain.mem_primesOverFinset_iff.

theorem IsLocalRing.primesOverFinset_eq {R : Type u_1} [CommRing R] (A : Type u_4) [CommRing A] [IsDomain A] [IsLocalRing A] [IsDedekindDomain A] [Algebra R A] [FaithfulSMul R A] [Module.Finite R A] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : IsDedekindDomain.primesOverFinset p A = {maximalIdeal A}

noncomputable def IsDedekindDomain.HeightOneSpectrum.equivPrimesOver {A : Type u_4} [CommRing A] {p : Ideal A} [hpm : p.IsMaximal] (B : Type u_5) [CommRing B] [IsDedekindDomain B] [Algebra A B] [IsDomain A] [Module.IsTorsionFree A B] (hp : p ≠ 0) : { v : HeightOneSpectrum B // v.asIdeal ∣ Ideal.map (algebraMap A B) p } ≃ ↑(p.primesOver B)

The bijection between the elements of the height one prime spectrum of B that divide the lift of the maximal ideal p in B and the primes over p in B.

Equations

• IsDedekindDomain.HeightOneSpectrum.equivPrimesOver B hp = Set.BijOn.equiv IsDedekindDomain.HeightOneSpectrum.asIdeal ⋯

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.equivPrimesOver_apply {A : Type u_4} [CommRing A] {p : Ideal A} [hpm : p.IsMaximal] (B : Type u_5) [CommRing B] [IsDedekindDomain B] [Algebra A B] [IsDomain A] [Module.IsTorsionFree A B] (hp : p ≠ 0) (v : { v : HeightOneSpectrum B // v.asIdeal ∣ Ideal.map (algebraMap A B) p }) : ↑((equivPrimesOver B hp) v) = (↑v).asIdeal

def IsDedekindDomain.HeightOneSpectrum.under (A : Type u_4) [CommRing A] {B : Type u_5} [CommRing B] [IsDedekindDomain B] [Algebra A B] [IsDomain A] [Algebra.IsIntegral A B] (w : HeightOneSpectrum B) : HeightOneSpectrum A

The pullback of a height one prime in B to A.

Equations

• IsDedekindDomain.HeightOneSpectrum.under A w = { asIdeal := Ideal.under A w.asIdeal, isPrime := ⋯, ne_bot := ⋯ }

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.under_asIdeal (A : Type u_4) [CommRing A] {B : Type u_5} [CommRing B] [IsDedekindDomain B] [Algebra A B] [IsDomain A] [Algebra.IsIntegral A B] (w : HeightOneSpectrum B) : (under A w).asIdeal = Ideal.under A w.asIdeal

theorem IsDedekindDomain.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] [IsDomain A] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B] : (p.primesOver B).Finite

@[deprecated IsDedekindDomain.primesOver_finite (since := "2026-04-16")]

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] [IsDomain A] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B] : (p.primesOver B).Finite

Alias of IsDedekindDomain.primesOver_finite.

@[implicit_reducible]

noncomputable instance IsDedekindDomain.instFintypeElemIdealPrimesOver {A : Type u_4} [CommRing A] (p : Ideal A) [hpm : p.IsMaximal] (B : Type u_5) [CommRing B] [IsDedekindDomain B] [Algebra A B] [IsDomain A] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B] : Fintype ↑(p.primesOver B)

Equations

• IsDedekindDomain.instFintypeElemIdealPrimesOver p B = ⋯.fintype

theorem IsDedekindDomain.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] [IsDomain A] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B] : (p.primesOver B).ncard ≠ 0

@[deprecated IsDedekindDomain.primesOver_ncard_ne_zero (since := "2026-04-16")]

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] [IsDomain A] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B] : (p.primesOver B).ncard ≠ 0

Alias of IsDedekindDomain.primesOver_ncard_ne_zero.

theorem IsDedekindDomain.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] [IsDomain A] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B] : 1 ≤ (p.primesOver B).ncard

@[deprecated IsDedekindDomain.one_le_primesOver_ncard (since := "2026-04-16")]

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] [IsDomain A] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B] : 1 ≤ (p.primesOver B).ncard

Alias of IsDedekindDomain.one_le_primesOver_ncard.