Dedekind domains and ideals

In this file, we show a ring is a Dedekind domain iff all fractional ideals are invertible. Then we prove some results on the unique factorization monoid structure of the ideals.

Main definitions

• IsDedekindDomainInv alternatively defines a Dedekind domain as an integral domain where every nonzero fractional ideal is invertible.
• isDedekindDomainInv_iff shows that this does note depend on the choice of field of fractions.
• IsDedekindDomain.HeightOneSpectrum defines the type of nonzero prime ideals of R.

Main results:

• isDedekindDomain_iff_isDedekindDomainInv
• Ideal.uniqueFactorizationMonoid

Implementation notes

The definitions that involve a field of fractions choose a canonical field of fractions, but are independent of that choice. The ..._iff lemmas express this independence.

Often, definitions assume that Dedekind domains are not fields. We found it more practical to add a (h : ¬ IsField A) assumption whenever this is explicitly needed.

References

• D. Marcus, Number Fields
• J.W.S. Cassels, A. Frölich, Algebraic Number Theory
• J. Neukirch, Algebraic Number Theory

Tags

dedekind domain, dedekind ring

noncomputable instance FractionalIdeal.instInvNonZeroDivisors (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] : Inv (FractionalIdeal (nonZeroDivisors R₁) K)

Equations

• FractionalIdeal.instInvNonZeroDivisors K = { inv := fun (I : FractionalIdeal (nonZeroDivisors R₁) K) => 1 / I }

theorem FractionalIdeal.inv_eq (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} : I⁻¹ = 1 / I

theorem FractionalIdeal.inv_zero' (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] : 0⁻¹ = 0

theorem FractionalIdeal.inv_nonzero (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0) : J⁻¹ = ⟨↑1 / ↑J, ⋯⟩

theorem FractionalIdeal.coe_inv_of_nonzero (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0) : ↑J⁻¹ = IsLocalization.coeSubmodule K ⊤ / ↑J

theorem FractionalIdeal.mem_inv_iff {K : Type u_3} [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} (hI : I ≠ 0) {x : K} : x ∈ I⁻¹ ↔ ∀ y ∈ I, x * y ∈ 1

theorem FractionalIdeal.inv_anti_mono {K : Type u_3} [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I J : FractionalIdeal (nonZeroDivisors R₁) K} (hI : I ≠ 0) (hJ : J ≠ 0) (hIJ : I ≤ J) : J⁻¹ ≤ I⁻¹

theorem FractionalIdeal.le_self_mul_inv {K : Type u_3} [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} (hI : I ≤ 1) : I ≤ I * I⁻¹

theorem FractionalIdeal.coe_ideal_le_self_mul_inv (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (I : Ideal R₁) : ↑I ≤ ↑I * (↑I)⁻¹

theorem FractionalIdeal.right_inverse_eq (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (I J : FractionalIdeal (nonZeroDivisors R₁) K) (h : I * J = 1) : J = I⁻¹

I⁻¹ is the inverse of I if I has an inverse.

theorem FractionalIdeal.mul_inv_cancel_iff (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} : I * I⁻¹ = 1 ↔ ∃ (J : FractionalIdeal (nonZeroDivisors R₁) K), I * J = 1

theorem FractionalIdeal.mul_inv_cancel_iff_isUnit (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} : I * I⁻¹ = 1 ↔ IsUnit I

@[simp]

theorem FractionalIdeal.map_inv (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {K' : Type u_5} [Field K'] [Algebra R₁ K'] [IsFractionRing R₁ K'] (I : FractionalIdeal (nonZeroDivisors R₁) K) (h : K ≃ₐ[R₁] K') : FractionalIdeal.map (↑h) I⁻¹ = (FractionalIdeal.map (↑h) I)⁻¹

@[simp]

theorem FractionalIdeal.spanSingleton_inv (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (x : K) : (FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x)⁻¹ = FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x⁻¹

theorem FractionalIdeal.spanSingleton_div_spanSingleton (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (x y : K) : FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x / FractionalIdeal.spanSingleton (nonZeroDivisors R₁) y = FractionalIdeal.spanSingleton (nonZeroDivisors R₁) (x / y)

theorem FractionalIdeal.spanSingleton_div_self (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : K} (hx : x ≠ 0) : FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x / FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x = 1

theorem FractionalIdeal.coe_ideal_span_singleton_div_self (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : R₁} (hx : x ≠ 0) : ↑(Ideal.span {x}) / ↑(Ideal.span {x}) = 1

theorem FractionalIdeal.spanSingleton_mul_inv (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : K} (hx : x ≠ 0) : FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x * (FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x)⁻¹ = 1

theorem FractionalIdeal.coe_ideal_span_singleton_mul_inv (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : R₁} (hx : x ≠ 0) : ↑(Ideal.span {x}) * (↑(Ideal.span {x}))⁻¹ = 1

theorem FractionalIdeal.spanSingleton_inv_mul (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : K} (hx : x ≠ 0) : (FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x)⁻¹ * FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x = 1

theorem FractionalIdeal.coe_ideal_span_singleton_inv_mul (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : R₁} (hx : x ≠ 0) : (↑(Ideal.span {x}))⁻¹ * ↑(Ideal.span {x}) = 1

theorem FractionalIdeal.mul_generator_self_inv (K : Type u_3) [Field K] {R₁ : Type u_6} [CommRing R₁] [Algebra R₁ K] [IsLocalization (nonZeroDivisors R₁) K] (I : FractionalIdeal (nonZeroDivisors R₁) K) [(↑I).IsPrincipal] (h : I ≠ 0) : I * FractionalIdeal.spanSingleton (nonZeroDivisors R₁) (Submodule.IsPrincipal.generator ↑I)⁻¹ = 1

theorem FractionalIdeal.invertible_of_principal (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (I : FractionalIdeal (nonZeroDivisors R₁) K) [(↑I).IsPrincipal] (h : I ≠ 0) : I * I⁻¹ = 1

theorem FractionalIdeal.invertible_iff_generator_nonzero (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (I : FractionalIdeal (nonZeroDivisors R₁) K) [(↑I).IsPrincipal] : I * I⁻¹ = 1 ↔ Submodule.IsPrincipal.generator ↑I ≠ 0

theorem FractionalIdeal.isPrincipal_inv (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (I : FractionalIdeal (nonZeroDivisors R₁) K) [(↑I).IsPrincipal] (h : I ≠ 0) : (↑I⁻¹).IsPrincipal

theorem FractionalIdeal.den_mem_inv {K : Type u_3} [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} (hI : I ≠ ⊥) : (algebraMap R₁ K) ↑I.den ∈ I⁻¹

theorem FractionalIdeal.num_le_mul_inv {K : Type u_3} [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (I : FractionalIdeal (nonZeroDivisors R₁) K) : ↑I.num ≤ I * I⁻¹

theorem FractionalIdeal.bot_lt_mul_inv {K : Type u_3} [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} (hI : I ≠ ⊥) : ⊥ < I * I⁻¹

noncomputable instance FractionalIdeal.instInvOneClassNonZeroDivisors {K : Type u_3} [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] : InvOneClass (FractionalIdeal (nonZeroDivisors R₁) K)

Equations

• FractionalIdeal.instInvOneClassNonZeroDivisors = InvOneClass.mk ⋯

def IsDedekindDomainInv (A : Type u_2) [CommRing A] [IsDomain A] : Prop

A Dedekind domain is an integral domain such that every fractional ideal has an inverse.

This is equivalent to IsDedekindDomain. In particular we provide a fractional_ideal.comm_group_with_zero instance, assuming IsDedekindDomain A, which implies IsDedekindDomainInv. For integral ideals, IsDedekindDomain(_inv) implies only Ideal.cancelCommMonoidWithZero.

Equations

• IsDedekindDomainInv A = ∀ (I : FractionalIdeal (nonZeroDivisors A) (FractionRing A)), I ≠ ⊥ → I * I⁻¹ = 1

theorem isDedekindDomainInv_iff {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] : IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal (nonZeroDivisors A) K), I ≠ ⊥ → I * I⁻¹ = 1

theorem FractionalIdeal.adjoinIntegral_eq_one_of_isUnit {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (x : K) (hx : IsIntegral A x) (hI : IsUnit (FractionalIdeal.adjoinIntegral (nonZeroDivisors A) x hx)) : FractionalIdeal.adjoinIntegral (nonZeroDivisors A) x hx = 1

theorem IsDedekindDomainInv.mul_inv_eq_one {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (h : IsDedekindDomainInv A) {I : FractionalIdeal (nonZeroDivisors A) K} (hI : I ≠ 0) : I * I⁻¹ = 1

theorem IsDedekindDomainInv.inv_mul_eq_one {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (h : IsDedekindDomainInv A) {I : FractionalIdeal (nonZeroDivisors A) K} (hI : I ≠ 0) : I⁻¹ * I = 1

theorem IsDedekindDomainInv.isUnit {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (h : IsDedekindDomainInv A) {I : FractionalIdeal (nonZeroDivisors A) K} (hI : I ≠ 0) : IsUnit I

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

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

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

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

Showing one side of the equivalence between the definitions IsDedekindDomainInv and IsDedekindDomain of Dedekind domains.

theorem one_mem_inv_coe_ideal {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDomain A] {I : Ideal A} (hI : I ≠ ⊥) : 1 ∈ (↑I)⁻¹

theorem exists_multiset_prod_cons_le_and_prod_not_le {A : Type u_2} [CommRing A] [IsDedekindDomain A] (hNF : ¬IsField A) {I M : Ideal A} (hI0 : I ≠ ⊥) (hIM : I ≤ M) [hM : M.IsMaximal] : ∃ (Z : Multiset (PrimeSpectrum A)), (M ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I

Specialization of exists_primeSpectrum_prod_le_and_ne_bot_of_domain to Dedekind domains: Let I : Ideal A be a nonzero ideal, where A is a Dedekind domain that is not a field. Then exists_primeSpectrum_prod_le_and_ne_bot_of_domain states we can find a product of prime ideals that is contained within I. This lemma extends that result by making the product minimal: let M be a maximal ideal that contains I, then the product including M is contained within I and the product excluding M is not contained within I.

theorem FractionalIdeal.not_inv_le_one_of_ne_bot {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {I : Ideal A} (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) : ¬(↑I)⁻¹ ≤ 1

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

theorem FractionalIdeal.mul_inv_cancel_of_le_one {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [h : IsDedekindDomain A] {I : Ideal A} (hI0 : I ≠ ⊥) (hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1) : ↑I * (↑I)⁻¹ = 1

theorem FractionalIdeal.coe_ideal_mul_inv {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [h : IsDedekindDomain A] (I : Ideal A) (hI0 : I ≠ ⊥) : ↑I * (↑I)⁻¹ = 1

Nonzero integral ideals in a Dedekind domain are invertible.

We will use this to show that nonzero fractional ideals are invertible, and finally conclude that fractional ideals in a Dedekind domain form a group with zero.

theorem FractionalIdeal.mul_inv_cancel {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {I : FractionalIdeal (nonZeroDivisors A) K} (hne : I ≠ 0) : I * I⁻¹ = 1

Nonzero fractional ideals in a Dedekind domain are units.

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

theorem FractionalIdeal.mul_right_le_iff {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {J : FractionalIdeal (nonZeroDivisors A) K} (hJ : J ≠ 0) {I I' : FractionalIdeal (nonZeroDivisors A) K} : I * J ≤ I' * J ↔ I ≤ I'

theorem FractionalIdeal.mul_left_le_iff {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {J : FractionalIdeal (nonZeroDivisors A) K} (hJ : J ≠ 0) {I I' : FractionalIdeal (nonZeroDivisors A) K} : J * I ≤ J * I' ↔ I ≤ I'

theorem FractionalIdeal.mul_right_strictMono {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {I : FractionalIdeal (nonZeroDivisors A) K} (hI : I ≠ 0) : StrictMono fun (x : FractionalIdeal (nonZeroDivisors A) K) => x * I

theorem FractionalIdeal.mul_left_strictMono {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {I : FractionalIdeal (nonZeroDivisors A) K} (hI : I ≠ 0) : StrictMono fun (x : FractionalIdeal (nonZeroDivisors A) K) => I * x

theorem FractionalIdeal.div_eq_mul_inv {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (I J : FractionalIdeal (nonZeroDivisors A) K) : I / J = I * J⁻¹

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

theorem isDedekindDomain_iff_isDedekindDomainInv {A : Type u_2} [CommRing A] [IsDomain A] : IsDedekindDomain A ↔ IsDedekindDomainInv A

IsDedekindDomain and IsDedekindDomainInv are equivalent ways to express that an integral domain is a Dedekind domain.

noncomputable instance FractionalIdeal.semifield {A : Type u_2} (K : Type u_3) [CommRing A] [Field K] [IsDedekindDomain A] [Algebra A K] [IsFractionRing A K] : Semifield (FractionalIdeal (nonZeroDivisors A) K)

Equations

• FractionalIdeal.semifield K = Semifield.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x : ℚ≥0) => HMul.hMul ↑x) ⋯

instance FractionalIdeal.cancelCommMonoidWithZero {A : Type u_2} (K : Type u_3) [CommRing A] [Field K] [IsDedekindDomain A] [Algebra A K] [IsFractionRing A K] : CancelCommMonoidWithZero (FractionalIdeal (nonZeroDivisors A) K)

Fractional ideals have cancellative multiplication in a Dedekind domain.

Although this instance is a direct consequence of the instance FractionalIdeal.semifield, we define this instance to provide a computable alternative.

Equations

• FractionalIdeal.cancelCommMonoidWithZero K = CancelCommMonoidWithZero.mk

instance Ideal.cancelCommMonoidWithZero {A : Type u_2} [CommRing A] [IsDedekindDomain A] : CancelCommMonoidWithZero (Ideal A)

Equations

• Ideal.cancelCommMonoidWithZero = CancelCommMonoidWithZero.mk

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

theorem Ideal.dvd_iff_le {A : Type u_2} [CommRing A] [IsDedekindDomain A] {I J : Ideal A} : I ∣ J ↔ J ≤ I

For ideals in a Dedekind domain, to divide is to contain.

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

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

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

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

Equations

• Ideal.normalizationMonoid = normalizationMonoidOfUniqueUnits

@[simp]

theorem Ideal.dvd_span_singleton {A : Type u_2} [CommRing A] [IsDedekindDomain A] {I : Ideal A} {x : A} : I ∣ Ideal.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_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 (Ideal.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.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_not_mem_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

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), (∀ 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.

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

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

• Ideal.instNormalizedGCDMonoid = NormalizedGCDMonoid.mk ⋯ ⋯

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

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

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 {R : Type u_1} {inst✝ : CommRing R} {x y : IsDedekindDomain.HeightOneSpectrum R} (asIdeal : x.asIdeal = y.asIdeal) : x = y

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

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

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

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

def IsDedekindDomain.HeightOneSpectrum.equivMaximalSpectrum {R : Type u_1} [CommRing R] [IsDedekindDomain R] (hR : ¬IsField R) : IsDedekindDomain.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.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 : IsDedekindDomain.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

Equations

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

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

Equations

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

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.

Equations

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

@[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] [Ring.DimensionLEOne R] {P Q : Ideal R} [hP : P.IsPrime] [hQ : Q.IsPrime] (hP0 : P ≠ ⊥) : P ≤ Q ↔ P = Q

theorem Ideal.coprime_of_no_prime_ge {R : Type u_1} [CommRing R] {I J : Ideal R} (h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime) : IsCoprime I J

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 at these ideals as associated elements of the monoid of 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).

Equations

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

noncomputable def IsDedekindDomain.quotientEquivPiFactors {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ ⊥) : R ⧸ I ≃+* ((P : { x : Ideal R // x ∈ (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) : (IsDedekindDomain.quotientEquivPiFactors hI) ((Ideal.Quotient.mk I) x) = fun (_P : { x : Ideal R // x ∈ (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 : { 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.

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 : { 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 : ∀ i ∈ s, Prime (P i)) (coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P 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.

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 (Ideal.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}

Equations

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

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.

Equations

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

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

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