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][marcus1977number]
• [J.W.S. Cassels, A. Frölich, Algebraic Number Theory][cassels1967algebraic]
• [J. Neukirch, Algebraic Number Theory][Neukirch1992]

Tags

dedekind domain, dedekind ring

noncomputable instance FractionalIdeal.instInvFractionalIdealNonZeroDivisorsToMonoidWithZeroToSemiringToCommSemiringToCommRingToEuclideanDomain (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

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

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⁻¹ = { val := ↑1 / ↑J, property := ⋯ }

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 : FractionalIdeal (nonZeroDivisors R₁) K} {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 : FractionalIdeal (nonZeroDivisors R₁) K) (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 : K) (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) [Submodule.IsPrincipal ↑I] (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) [Submodule.IsPrincipal ↑I] (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) [Submodule.IsPrincipal ↑I] : 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) [Submodule.IsPrincipal ↑I] (h : I ≠ 0) : Submodule.IsPrincipal ↑I⁻¹

noncomputable instance FractionalIdeal.instInvOneClassFractionalIdealNonZeroDivisorsToMonoidWithZeroToSemiringToCommSemiringToCommRingToEuclideanDomain (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.instInvOneClassFractionalIdealNonZeroDivisorsToMonoidWithZeroToSemiringToCommSemiringToCommRingToEuclideanDomain K = 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 : Ideal A} {M : Ideal A} (hI0 : I ≠ ⊥) (hIM : I ≤ M) [hM : Ideal.IsMaximal M] : ∃ (Z : Multiset (PrimeSpectrum A)), Multiset.prod (M ::ₘ Multiset.map PrimeSpectrum.asIdeal Z) ≤ I ∧ ¬Multiset.prod (Multiset.map PrimeSpectrum.asIdeal Z) ≤ 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 : FractionalIdeal (nonZeroDivisors A) K} {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 : FractionalIdeal (nonZeroDivisors A) K} {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 : FractionalIdeal (nonZeroDivisors A) K) (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 = let __src := ⋯; Semifield.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯

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 = let __spread.0 := inferInstance; CancelCommMonoidWithZero.mk

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

Equations

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

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

Equations

• ⋯ = ⋯

theorem Ideal.dvd_iff_le {A : Type u_2} [CommRing A] [IsDedekindDomain A] {I : Ideal A} {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 : Ideal A} {J : Ideal A} : DvdNotUnit I J ↔ J < I

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

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} : Ideal.IsPrime P ↔ 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 : Ideal A} {I : Ideal A} (hI : I ≠ ⊥) : p ∈ UniqueFactorizationMonoid.normalizedFactors I ↔ Ideal.IsPrime p ∧ 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 : Ideal A} {I : Ideal A} [P_prime : Ideal.IsPrime P] (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 : Ideal.IsPrime P] (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 : FractionalIdeal (nonZeroDivisors A) K} {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 : FractionalIdeal (nonZeroDivisors A) K} {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 : Ideal A) (J : Ideal A) : (I ⊔ J) * (I ⊓ J) = I * J

instance Ideal.instNormalizedGCDMonoidIdealToSemiringToCommSemiringCancelCommMonoidWithZero {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.instNormalizedGCDMonoidIdealToSemiringToCommSemiringCancelCommMonoidWithZero = let __src := Ideal.normalizationMonoid; NormalizedGCDMonoid.mk ⋯ ⋯

@[simp]

theorem Ideal.gcd_eq_sup {A : Type u_2} [CommRing A] [IsDedekindDomain A] (I : Ideal A) (J : Ideal A) : gcd I J = I ⊔ J

@[simp]

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

theorem Ideal.inf_eq_mul_of_coprime {A : Type u_2} [CommRing A] [IsDedekindDomain A] {I : Ideal A} {J : Ideal A} (coprime : IsCoprime I J) : I ⊓ J = I * J

theorem Ideal.isCoprime_iff_gcd {A : Type u_2} [CommRing A] [IsDedekindDomain A] {I : Ideal A} {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 ≠ ⊥) : Multiset.prod (UniqueFactorizationMonoid.normalizedFactors I) = I

theorem count_le_of_ideal_ge {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I : Ideal T} {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 : Ideal T} {J : Ideal T} (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : I ⊔ J = Multiset.prod (UniqueFactorizationMonoid.normalizedFactors I ∩ UniqueFactorizationMonoid.normalizedFactors J)

theorem irreducible_pow_sup {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I : Ideal T} {J : 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 : Ideal T} {J : Ideal T} (hJ : Irreducible J) (n : ℕ) (hn : ↑n ≤ multiplicity J I) : J ^ n ⊔ I = J ^ n

theorem irreducible_pow_sup_of_ge {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I : Ideal T} {J : Ideal T} (hI : I ≠ ⊥) (hJ : Irreducible J) (n : ℕ) (hn : multiplicity J I ≤ ↑n) : J ^ n ⊔ I = J ^ (multiplicity J I).get ⋯

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.

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

theorem IsDedekindDomain.HeightOneSpectrum.ext_iff {R : Type u_1} : ∀ {inst : CommRing R} (x y : IsDedekindDomain.HeightOneSpectrum R), x = y ↔ x.asIdeal = y.asIdeal

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 : Ideal.IsPrime self.asIdeal
• ne_bot : self.asIdeal ≠ ⊥

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

Equations

• ⋯ = ⋯

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 (Ideal.primeCompl v.asIdeal) ⋯ = ⊥

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.

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

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_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) : OrderHom.comp (idealFactorsFunOfQuotHom hg) (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 = let_fun f_surj := ⋯; let_fun fsym_surj := ⋯; OrderIso.ofHomInv (idealFactorsFunOfQuotHom f_surj) (idealFactorsFunOfQuotHom fsym_surj) ⋯ ⋯

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

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 : Ideal R} {M : Ideal R} (hL : L ∣ I) (hM : M ∣ I) : ↑((idealFactorsEquivOfQuotEquiv f) { val := L, property := hL }) ∣ ↑((idealFactorsEquivOfQuotEquiv f) { val := M, property := 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) { val := L, property := ⋯ }) ∈ 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 (RingEquiv.symm f) hJ hI

theorem normalizedFactorsEquivOfQuotEquiv_multiplicity_eq_multiplicity {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) [DecidableRel fun (x x_1 : Ideal R) => x ∣ x_1] [DecidableRel fun (x x_1 : Ideal A) => x ∣ x_1] (hI : I ≠ ⊥) (hJ : J ≠ ⊥) (L : Ideal R) (hL : L ∈ UniqueFactorizationMonoid.normalizedFactors I) : multiplicity (↑((normalizedFactorsEquivOfQuotEquiv f hI hJ) { val := L, property := hL })) J = multiplicity 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 : Ideal R} {Q : Ideal R} [hP : Ideal.IsPrime P] [hQ : Ideal.IsPrime Q] (hP0 : P ≠ ⊥) : P ≤ Q ↔ P = Q

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

theorem Ideal.IsPrime.mul_mem_pow {R : Type u_1} [CommRing R] [IsDedekindDomain R] (I : Ideal R) [hI : Ideal.IsPrime I] {a : R} {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 : Ideal.IsPrime I] {a : R} {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 : Ideal R} {x : Ideal R} [hp : Ideal.IsPrime p] {n : ℕ} (hle : x ≤ p ^ n) (hlt : ¬x ≤ p ^ (n + 1)) : Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n

theorem Ideal.le_mul_of_no_prime_factors {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} {J : Ideal R} {K : Ideal R} (coprime : ∀ (P : Ideal R), J ≤ P → K ≤ P → ¬Ideal.IsPrime P) (hJ : I ≤ J) (hK : I ≤ K) : I ≤ J * K

theorem Ideal.le_of_pow_le_prime {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} {P : Ideal R} [hP : Ideal.IsPrime P] {n : ℕ} (h : I ^ n ≤ P) : I ≤ P

theorem Ideal.pow_le_prime_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} {P : Ideal R} [_hP : Ideal.IsPrime P] {n : ℕ} (hn : n ≠ 0) : I ^ n ≤ P ↔ I ≤ P

theorem Ideal.prod_le_prime {R : Type u_1} [CommRing R] [IsDedekindDomain R] {ι : Type u_4} {s : Finset ι} {f : ι → Ideal R} {P : Ideal R} [hP : Ideal.IsPrime P] : (Finset.prod s fun (i : ι) => f i) ≤ P ↔ ∃ i ∈ s, f i ≤ P

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) : (Finset.inf s fun (i : ι) => f i ^ e i) = Finset.prod s fun (i : ι) => 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 : (Finset.prod Finset.univ fun (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 = RingEquiv.trans (Ideal.quotEquivOfEq ⋯) (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 ∈ Multiset.toFinset (UniqueFactorizationMonoid.factors I) }) → 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 ∈ Multiset.toFinset (UniqueFactorizationMonoid.factors I) }) => (Ideal.Quotient.mk (↑_P ^ Multiset.count (↑_P) (UniqueFactorizationMonoid.factors I))) x

noncomputable def Ideal.quotientMulEquivQuotientProd {R : Type u_1} [CommRing R] [IsDedekindDomain R] (I : Ideal R) (J : Ideal R) (coprime : IsCoprime I J) : R ⧸ I * J ≃+* (R ⧸ I) × R ⧸ J

Chinese remainder theorem, specialized to two ideals.

Equations

• Ideal.quotientMulEquivQuotientProd I J coprime = RingEquiv.trans (Ideal.quotEquivOfEq ⋯) (Ideal.quotientInfEquivQuotientProd I J coprime)

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 : (Finset.prod s fun (i : ι) => 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 in 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 { val := i, property := 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 { val := i, property := 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 : R} {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 : R} {b : R} (ha : a ∈ UniqueFactorizationMonoid.normalizedFactors b) : Ideal.span {a} ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.span {b})

theorem multiplicity_eq_multiplicity_span {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [DecidableRel fun (x x_1 : R) => x ∣ x_1] [DecidableRel fun (x x_1 : Ideal R) => x ∣ x_1] {a : R} {b : R} : multiplicity (Ideal.span {a}) (Ideal.span {b}) = multiplicity 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

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

theorem multiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_multiplicity {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] [DecidableRel fun (x x_1 : R) => x ∣ x_1] [DecidableRel fun (x x_1 : Ideal R) => x ∣ x_1] {r : R} {d : R} (hr : r ≠ 0) (hd : d ∈ UniqueFactorizationMonoid.normalizedFactors r) : multiplicity d r = multiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr) { val := d, property := 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.

theorem multiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_multiplicity {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] [DecidableRel fun (x x_1 : R) => x ∣ x_1] [DecidableRel fun (x x_1 : Ideal R) => x ∣ x_1] {r : R} (hr : r ≠ 0) (I : ↑{I : Ideal R | I ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})}) : multiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = multiplicity (↑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.