# 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.instInvNonZeroDivisors (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] :
Inv ()
Equations
• = { inv := fun (I : ) => 1 / I }
theorem FractionalIdeal.inv_eq (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] {I : } :
I⁻¹ = 1 / I
theorem FractionalIdeal.inv_zero' (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] :
0⁻¹ = 0
theorem FractionalIdeal.inv_nonzero (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] {J : } (h : J 0) :
J⁻¹ = 1 / J,
theorem FractionalIdeal.coe_inv_of_nonzero (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] {J : } (h : J 0) :
J⁻¹ =
theorem FractionalIdeal.mem_inv_iff {K : Type u_3} [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] {I : } (hI : I 0) {x : K} :
x I⁻¹ yI, x * y 1
theorem FractionalIdeal.inv_anti_mono {K : Type u_3} [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] {I : } {J : } (hI : I 0) (hJ : J 0) (hIJ : I J) :
theorem FractionalIdeal.le_self_mul_inv {K : Type u_3} [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] {I : } (hI : I 1) :
I I * I⁻¹
theorem FractionalIdeal.coe_ideal_le_self_mul_inv (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] (I : Ideal R₁) :
I I * (I)⁻¹
theorem FractionalIdeal.right_inverse_eq (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] (I : ) (J : ) (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) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] {I : } :
I * I⁻¹ = 1 ∃ (J : ), I * J = 1
theorem FractionalIdeal.mul_inv_cancel_iff_isUnit (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] {I : } :
I * I⁻¹ = 1
@[simp]
theorem FractionalIdeal.map_inv (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] {K' : Type u_5} [Field K'] [Algebra R₁ K'] [IsFractionRing R₁ K'] (I : ) (h : K ≃ₐ[R₁] K') :
@[simp]
theorem FractionalIdeal.spanSingleton_inv (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] (x : K) :
theorem FractionalIdeal.spanSingleton_div_spanSingleton (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] (x : K) (y : K) :
theorem FractionalIdeal.spanSingleton_div_self (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] {x : K} (hx : x 0) :
theorem FractionalIdeal.coe_ideal_span_singleton_div_self (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] {x : R₁} (hx : x 0) :
(Ideal.span {x}) / (Ideal.span {x}) = 1
theorem FractionalIdeal.spanSingleton_mul_inv (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] {x : K} (hx : x 0) :
theorem FractionalIdeal.coe_ideal_span_singleton_mul_inv (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] {x : R₁} (hx : x 0) :
(Ideal.span {x}) * ((Ideal.span {x}))⁻¹ = 1
theorem FractionalIdeal.spanSingleton_inv_mul (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] {x : K} (hx : x 0) :
theorem FractionalIdeal.coe_ideal_span_singleton_inv_mul (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] {x : R₁} (hx : x 0) :
((Ideal.span {x}))⁻¹ * (Ideal.span {x}) = 1
theorem FractionalIdeal.mul_generator_self_inv (K : Type u_3) [] {R₁ : Type u_6} [CommRing R₁] [Algebra R₁ K] [] (I : ) [(I).IsPrincipal] (h : I 0) :
theorem FractionalIdeal.invertible_of_principal (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] (I : ) [(I).IsPrincipal] (h : I 0) :
I * I⁻¹ = 1
theorem FractionalIdeal.invertible_iff_generator_nonzero (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] (I : ) [(I).IsPrincipal] :
I * I⁻¹ = 1
theorem FractionalIdeal.isPrincipal_inv (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] (I : ) [(I).IsPrincipal] (h : I 0) :
(I⁻¹).IsPrincipal
noncomputable instance FractionalIdeal.instInvOneClassNonZeroDivisors (K : Type u_3) [] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [] :
Equations
def IsDedekindDomainInv (A : Type u_2) [] [] :

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
Instances For
theorem isDedekindDomainInv_iff {A : Type u_2} {K : Type u_3} [] [] [] [Algebra A K] [] :
∀ (I : ), I I * I⁻¹ = 1
theorem FractionalIdeal.adjoinIntegral_eq_one_of_isUnit {A : Type u_2} {K : Type u_3} [] [] [] [Algebra A K] [] (x : K) (hx : ) (hI : ) :
theorem IsDedekindDomainInv.mul_inv_eq_one {A : Type u_2} {K : Type u_3} [] [] [] [Algebra A K] [] (h : ) {I : } (hI : I 0) :
I * I⁻¹ = 1
theorem IsDedekindDomainInv.inv_mul_eq_one {A : Type u_2} {K : Type u_3} [] [] [] [Algebra A K] [] (h : ) {I : } (hI : I 0) :
I⁻¹ * I = 1
theorem IsDedekindDomainInv.isUnit {A : Type u_2} {K : Type u_3} [] [] [] [Algebra A K] [] (h : ) {I : } (hI : I 0) :
theorem IsDedekindDomainInv.isNoetherianRing {A : Type u_2} [] [] (h : ) :
theorem IsDedekindDomainInv.integrallyClosed {A : Type u_2} [] [] (h : ) :
theorem IsDedekindDomainInv.dimensionLEOne {A : Type u_2} [] [] (h : ) :
theorem IsDedekindDomainInv.isDedekindDomain {A : Type u_2} [] [] (h : ) :

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} [] [] [Algebra A K] [] [] {I : } (hI : I ) :
1 (I)⁻¹
theorem exists_multiset_prod_cons_le_and_prod_not_le {A : Type u_2} [] [] (hNF : ¬) {I : } {M : } (hI0 : I ) (hIM : I M) [hM : M.IsMaximal] :
∃ (Z : ), (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} [] [] [Algebra A K] [] [] {I : } (hI0 : I ) (hI1 : I ) :
¬(I)⁻¹ 1
theorem FractionalIdeal.exists_not_mem_one_of_ne_bot {A : Type u_2} {K : Type u_3} [] [] [Algebra A K] [] [] {I : } (hI0 : I ) (hI1 : I ) :
x(I)⁻¹, x1
theorem FractionalIdeal.mul_inv_cancel_of_le_one {A : Type u_2} {K : Type u_3} [] [] [Algebra A K] [] [h : ] {I : } (hI0 : I ) (hI : (I * (I)⁻¹)⁻¹ 1) :
I * (I)⁻¹ = 1
theorem FractionalIdeal.coe_ideal_mul_inv {A : Type u_2} {K : Type u_3} [] [] [Algebra A K] [] [h : ] (I : ) (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} [] [] [Algebra A K] [] [] {I : } (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} [] [] [Algebra A K] [] [] {J : } (hJ : J 0) {I : } {I' : } :
I * J I' * J I I'
theorem FractionalIdeal.mul_left_le_iff {A : Type u_2} {K : Type u_3} [] [] [Algebra A K] [] [] {J : } (hJ : J 0) {I : } {I' : } :
J * I J * I' I I'
theorem FractionalIdeal.mul_right_strictMono {A : Type u_2} {K : Type u_3} [] [] [Algebra A K] [] [] {I : } (hI : I 0) :
StrictMono fun (x : ) => x * I
theorem FractionalIdeal.mul_left_strictMono {A : Type u_2} {K : Type u_3} [] [] [Algebra A K] [] [] {I : } (hI : I 0) :
StrictMono fun (x : ) => I * x
theorem FractionalIdeal.div_eq_mul_inv {A : Type u_2} {K : Type u_3} [] [] [Algebra A K] [] [] (I : ) (J : ) :
I / J = I * J⁻¹

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

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) [] [] [] [Algebra A K] [] :
Equations
• = let __spread.0 := ; Semifield.mk zpowRec (fun (q : ℚ≥0) (a : ) => q * a)
instance FractionalIdeal.cancelCommMonoidWithZero {A : Type u_2} (K : Type u_3) [] [] [] [Algebra 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
• = let __spread.0 := inferInstance; CancelCommMonoidWithZero.mk
instance Ideal.cancelCommMonoidWithZero {A : Type u_2} [] [] :
Equations
• One or more equations did not get rendered due to their size.
instance Ideal.isDomain {A : Type u_2} [] [] :
Equations
• =
theorem Ideal.dvd_iff_le {A : Type u_2} [] [] {I : } {J : } :
I J J I

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

theorem Ideal.dvdNotUnit_iff_lt {A : Type u_2} [] [] {I : } {J : } :
J < I
instance instWfDvdMonoidIdeal {A : Type u_2} [] [] :
Equations
• =
instance Ideal.uniqueFactorizationMonoid {A : Type u_2} [] [] :
Equations
• =
instance Ideal.normalizationMonoid {A : Type u_2} [] [] :
Equations
• Ideal.normalizationMonoid = normalizationMonoidOfUniqueUnits
@[simp]
theorem Ideal.dvd_span_singleton {A : Type u_2} [] [] {I : } {x : A} :
I Ideal.span {x} x I
theorem Ideal.isPrime_of_prime {A : Type u_2} [] [] {P : } (h : ) :
P.IsPrime
theorem Ideal.prime_of_isPrime {A : Type u_2} [] [] {P : } (hP : P ) (h : P.IsPrime) :
theorem Ideal.prime_iff_isPrime {A : Type u_2} [] [] {P : } (hP : 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} [] [] {P : } :
P.IsPrime 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} [] [] {a : A} :
theorem Ideal.prime_generator_of_prime {A : Type u_2} [] [] {P : } (h : ) :
theorem Ideal.mem_normalizedFactors_iff {A : Type u_2} [] [] {p : } {I : } (hI : I ) :
p.IsPrime I p
theorem Ideal.pow_right_strictAnti {A : Type u_2} [] [] (I : ) (hI0 : I ) (hI1 : I ) :
StrictAnti fun (x : ) => I ^ x
theorem Ideal.pow_lt_self {A : Type u_2} [] [] (I : ) (hI0 : I ) (hI1 : I ) (e : ) (he : 2 e) :
I ^ e < I
theorem Ideal.exists_mem_pow_not_mem_pow_succ {A : Type u_2} [] [] (I : ) (hI0 : I ) (hI1 : I ) (e : ) :
xI ^ e, xI ^ (e + 1)
theorem Ideal.eq_prime_pow_of_succ_lt_of_le {A : Type u_2} [] [] {P : } {I : } [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} [] [] {P : } [P_prime : P.IsPrime] (hP : P ) (i : ) :
P ^ (i + 1) < P ^ i
theorem Associates.le_singleton_iff {A : Type u_2} [] [] (x : A) (n : ) (I : ) :
theorem FractionalIdeal.le_inv_comm {A : Type u_2} {K : Type u_3} [] [] [] [Algebra A K] [] {I : } {J : } (hI : I 0) (hJ : J 0) :
theorem FractionalIdeal.inv_le_comm {A : Type u_2} {K : Type u_3} [] [] [] [Algebra A K] [] {I : } {J : } (hI : I 0) (hJ : J 0) :
theorem Ideal.exist_integer_multiples_not_mem {A : Type u_2} {K : Type u_3} [] [] [] [Algebra A K] [] {J : } (hJ : J ) {ι : Type u_4} (s : ) (f : ιK) {j : ι} (hjs : j s) (hjf : f j 0) :
∃ (a : K), (is, IsLocalization.IsInteger A (a * f i)) is, a * f iJ

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

### 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} [] [] (I : ) (J : ) :
(I J) * (I J) = I * J
instance Ideal.instNormalizedGCDMonoid {A : Type u_2} [] [] :

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

Equations
• Ideal.instNormalizedGCDMonoid = let __src := Ideal.normalizationMonoid;
@[simp]
theorem Ideal.gcd_eq_sup {A : Type u_2} [] [] (I : ) (J : ) :
gcd I J = I J
@[simp]
theorem Ideal.lcm_eq_inf {A : Type u_2} [] [] (I : ) (J : ) :
lcm I J = I J
theorem Ideal.isCoprime_iff_gcd {A : Type u_2} [] [] {I : } {J : } :
gcd I J = 1
theorem Ideal.factors_span_eq {K : Type u_3} [] {p : } :
= Multiset.map (fun (q : ) => Ideal.span {q})
theorem prod_normalizedFactors_eq_self {T : Type u_4} [] [] {I : } (hI : I ) :
theorem count_le_of_ideal_ge {T : Type u_4} [] [] {I : } {J : } (h : I J) (hI : I ) (K : ) :
theorem sup_eq_prod_inf_factors {T : Type u_4} [] [] {I : } {J : } (hI : I ) (hJ : J ) :
theorem irreducible_pow_sup {T : Type u_4} [] [] {I : } {J : } (hI : I ) (hJ : ) (n : ) :
J ^ n I =
theorem irreducible_pow_sup_of_le {T : Type u_4} [] [] {I : } {J : } (hJ : ) (n : ) (hn : n ) :
J ^ n I = J ^ n
theorem irreducible_pow_sup_of_ge {T : Type u_4} [] [] {I : } {J : } (hI : I ) (hJ : ) (n : ) (hn : n) :
J ^ n I = J ^ ().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_iff {R : Type u_1} :
∀ {inst : } (x y : ), x = y x.asIdeal = y.asIdeal
theorem IsDedekindDomain.HeightOneSpectrum.ext {R : Type u_1} :
∀ {inst : } (x y : ), x.asIdeal = y.asIdealx = y
structure IsDedekindDomain.HeightOneSpectrum (R : Type u_1) [] :
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 :
• isPrime : self.asIdeal.IsPrime
• ne_bot : self.asIdeal
Instances For
theorem IsDedekindDomain.HeightOneSpectrum.isPrime {R : Type u_1} [] (self : ) :
self.asIdeal.IsPrime
theorem IsDedekindDomain.HeightOneSpectrum.ne_bot {R : Type u_1} [] (self : ) :
self.asIdeal
instance IsDedekindDomain.HeightOneSpectrum.isMaximal {R : Type u_1} [] [] :
v.asIdeal.IsMaximal
Equations
• =
theorem IsDedekindDomain.HeightOneSpectrum.prime {R : Type u_1} [] [] :
Prime v.asIdeal

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem IsDedekindDomain.HeightOneSpectrum.iInf_localization_eq_bot (R : Type u_1) (K : Type u_3) [] [] [] [Algebra R K] [hK : ] :
⨅ (v : ), 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.

@[simp]
theorem idealFactorsFunOfQuotHom_coe_coe {R : Type u_1} {A : Type u_2} [] [] [] {I : } {J : } {f : R I →+* A J} (hf : ) (X : { p : // p I }) :
( X) = Ideal.comap (Ideal.map f ())
def idealFactorsFunOfQuotHom {R : Type u_1} {A : Type u_2} [] [] [] {I : } {J : } {f : R I →+* A J} (hf : ) :
{ p : // p I } →o { p : // p J }

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

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

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

Equations
Instances For
theorem idealFactorsEquivOfQuotEquiv_symm {R : Type u_1} {A : Type u_2} [] [] [] {I : } {J : } [] (f : R I ≃+* A J) :
.symm =
theorem idealFactorsEquivOfQuotEquiv_is_dvd_iso {R : Type u_1} {A : Type u_2} [] [] [] {I : } {J : } [] (f : R I ≃+* A J) {L : } {M : } (hL : L I) (hM : M I) :
( L, hL) ( M, hM) L M
theorem idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors {R : Type u_1} {A : Type u_2} [] [] [] {I : } {J : } [] (f : R I ≃+* A J) (hJ : J ) {L : } (hL : ) :
def normalizedFactorsEquivOfQuotEquiv {R : Type u_1} {A : Type u_2} [] [] [] {I : } {J : } [] (f : R I ≃+* A J) (hI : I ) (hJ : 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.
Instances For
@[simp]
theorem normalizedFactorsEquivOfQuotEquiv_symm {R : Type u_1} {A : Type u_2} [] [] [] {I : } {J : } [] (f : R I ≃+* A J) (hI : I ) (hJ : J ) :
theorem normalizedFactorsEquivOfQuotEquiv_multiplicity_eq_multiplicity {R : Type u_1} {A : Type u_2} [] [] [] {I : } {J : } [] (f : R I ≃+* A J) [DecidableRel fun (x x_1 : ) => x x_1] [DecidableRel fun (x x_1 : ) => x x_1] (hI : I ) (hJ : J ) (L : ) (hL : ) :
multiplicity ((() L, hL)) J =

The map normalizedFactorsEquivOfQuotEquiv preserves multiplicities.

theorem Ring.DimensionLeOne.prime_le_prime_iff_eq {R : Type u_1} [] {P : } {Q : } [hP : P.IsPrime] [hQ : Q.IsPrime] (hP0 : P ) :
P Q P = Q
theorem Ideal.coprime_of_no_prime_ge {R : Type u_1} [] {I : } {J : } (h : ∀ (P : ), I PJ P¬P.IsPrime) :
theorem Ideal.IsPrime.mul_mem_pow {R : Type u_1} [] [] (I : ) [hI : I.IsPrime] {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} [] [] (I : ) [hI : I.IsPrime] {a : R} {b : R} {n : } (h : a * b I ^ n) :
a I ^ n b I
theorem Ideal.count_normalizedFactors_eq {R : Type u_1} [] [] {p : } {x : } [hp : p.IsPrime] {n : } (hle : x p ^ n) [DecidableEq ()] (hlt : ¬x p ^ (n + 1)) :
theorem Ideal.le_mul_of_no_prime_factors {R : Type u_1} [] [] {I : } {J : } {K : } (coprime : ∀ (P : ), J PK P¬P.IsPrime) (hJ : I J) (hK : I K) :
I J * K
theorem Ideal.le_of_pow_le_prime {R : Type u_1} [] [] {I : } {P : } [hP : P.IsPrime] {n : } (h : I ^ n P) :
I P
theorem Ideal.pow_le_prime_iff {R : Type u_1} [] [] {I : } {P : } [_hP : P.IsPrime] {n : } (hn : n 0) :
I ^ n P I P
theorem Ideal.prod_le_prime {R : Type u_1} [] [] {ι : Type u_4} {s : } {f : ι} {P : } [hP : P.IsPrime] :
is, f i P is, f i P
theorem IsDedekindDomain.inf_prime_pow_eq_prod {R : Type u_1} [] [] {ι : Type u_4} (s : ) (f : ι) (e : ι) (prime : is, Prime (f i)) (coprime : is, js, i jf i f j) :
(s.inf fun (i : ι) => f i ^ e i) = is, f i ^ e i

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

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

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

Equations
Instances For
noncomputable def IsDedekindDomain.quotientEquivPiFactors {R : Type u_1} [] [] {I : } (hI : I ) :
R I ≃+* ((P : { x : // x .toFinset }) → R P ^ )

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

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

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

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

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

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

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

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

theorem span_singleton_dvd_span_singleton_iff_dvd {R : Type u_1} [] [] {a : R} {b : R} :
@[simp]
theorem Ideal.squarefree_span_singleton {R : Type u_1} [] [] {a : R} :
theorem singleton_span_mem_normalizedFactors_of_mem_normalizedFactors {R : Type u_1} [] [] {a : R} {b : R} (ha : ) :
theorem multiplicity_eq_multiplicity_span {R : Type u_1} [] [] [DecidableRel fun (x x_1 : R) => x x_1] [DecidableRel fun (x x_1 : ) => x x_1] {a : R} {b : R} :
noncomputable def normalizedFactorsEquivSpanNormalizedFactors {R : Type u_1} [] [] {r : R} (hr : r 0) :
{d : R | } {I : | }

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

Equations
Instances For
theorem multiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_multiplicity {R : Type u_1} [] [] [DecidableRel fun (x x_1 : R) => x x_1] [DecidableRel fun (x x_1 : ) => x x_1] {r : R} {d : R} (hr : r 0) (hd : ) :
= multiplicity (( 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 multiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_multiplicity {R : Type u_1} [] [] [DecidableRel fun (x x_1 : R) => x x_1] [DecidableRel fun (x x_1 : ) => x x_1] {r : R} (hr : r 0) (I : {I : | }) :
multiplicity (( 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.

theorem count_span_normalizedFactors_eq {R : Type u_1} [] [] [] [DecidableEq ()] [DecidableRel fun (x x_1 : R) => x x_1] [DecidableRel fun (x x_1 : ) => x x_1] {r : R} {X : R} (hr : r 0) (hX : ) :
= Multiset.count (normalize X)

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} [] [] [] [DecidableEq ()] [DecidableRel fun (x x_1 : R) => x x_1] [DecidableRel fun (x x_1 : ) => x x_1] {r : R} {X : R} (hr : r 0) (hX₁ : = 1) (hX : ) :
theorem count_associates_factors_eq {R : Type u_1} [] [] [DecidableEq ()] [DecidableEq (Associates ())] [(p : Associates ()) → ] (I : ) (J : ) (hI : I 0) (hJ : J.IsPrime) (hJ₀ : J ) :
().count ().factors =

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.