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.

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

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

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.

@[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 prod_normalizedFactors_eq_self {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I : Ideal T} (hI : I ≠ ⊥) : (UniqueFactorizationMonoid.normalizedFactors I).prod = I

theorem count_le_of_ideal_ge {T : Type u_4} [CommRing T] [IsDedekindDomain T] [DecidableEq (Ideal 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)

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

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 : ℕ) : J ^ n ⊔ I = J ^ min (Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)) 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 ^ n ⊔ I = 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 ^ n ⊔ I = 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] : ∃ (Q : Ideal T), P ⊔ Q = ⊤ ∧ I = P ^ Multiset.count P (UniqueFactorizationMonoid.normalizedFactors I) * Q

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)

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

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.

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

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

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

@[simp]

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

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

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.

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

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

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) : ↑((idealFactorsEquivOfQuotEquiv f) ⟨L, ⋯⟩) ∈ UniqueFactorizationMonoid.normalizedFactors J

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}

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

@[simp]

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 ≠ ⊥) : (normalizedFactorsEquivOfQuotEquiv f hI hJ).symm = normalizedFactorsEquivOfQuotEquiv f.symm hJ hI

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 (↑((normalizedFactorsEquivOfQuotEquiv f hI hJ) ⟨L, hL⟩)) J = emultiplicity L I

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

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)) : Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n

theorem count_associates_factors_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] [DecidableEq (Ideal R)] [DecidableEq (Associates (Ideal R))] [(p : Associates (Ideal R)) → Decidable (Irreducible p)] {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.

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) : (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] [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) : (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.inf_prime_pow_eq_prod {R : Type u_1} [CommRing R] [IsDedekindDomain R] {ι : Type u_4} (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.

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

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.

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

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

@[simp]

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

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})

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

noncomputable 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})}

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

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 (↑((normalizedFactorsEquivSpanNormalizedFactors hr) ⟨d, hd⟩)) (Ideal.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.

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 (↑((normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = emultiplicity (↑I) (Ideal.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.

theorem count_span_normalizedFactors_eq {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] [DecidableEq R] [DecidableEq (Ideal 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)

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 count_span_normalizedFactors_eq_of_normUnit {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] [DecidableEq R] [DecidableEq (Ideal 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)

@[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] : Finset (Ideal B)

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

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] : ↑(primesOverFinset p B) = p.primesOver B

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 ∈ primesOverFinset p B ↔ P ∈ p.primesOver B

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 ≠ ⊥) : 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.

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

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

noncomputable instance 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)

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

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