# mathlibdocumentation

ring_theory.dedekind_domain.ideal

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

• `is_dedekind_domain_inv` alternatively defines a Dedekind domain as an integral domain where every nonzero fractional ideal is invertible.
• `is_dedekind_domain_inv_iff` shows that this does note depend on the choice of field of fractions.
• `is_dedekind_domain.height_one_spectrum` defines the type of nonzero prime ideals of `R`.

## Main results: #

• `is_dedekind_domain_iff_is_dedekind_domain_inv`
• `ideal.unique_factorization_monoid`

## 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 : ¬ is_field A)` assumption whenever this is explicitly needed.

## Tags #

dedekind domain, dedekind ring

@[protected, instance]
noncomputable def fractional_ideal.has_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] :
Equations
theorem fractional_ideal.inv_eq (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {I : K} :
I⁻¹ = 1 / I
theorem fractional_ideal.inv_zero' (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] :
0⁻¹ = 0
theorem fractional_ideal.inv_nonzero (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {J : K} (h : J 0) :
J⁻¹ = 1 / J, _⟩
theorem fractional_ideal.coe_inv_of_nonzero (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {J : K} (h : J 0) :
theorem fractional_ideal.mem_inv_iff {K : Type u_3} [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {I : K} (hI : I 0) {x : K} :
x I⁻¹ (y : K), y I x * y 1
theorem fractional_ideal.inv_anti_mono {K : Type u_3} [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {I J : K} (hI : I 0) (hJ : J 0) (hIJ : I J) :
theorem fractional_ideal.le_self_mul_inv {K : Type u_3} [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {I : K} (hI : I 1) :
I I * I⁻¹
theorem fractional_ideal.coe_ideal_le_self_mul_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] (I : ideal R₁) :
theorem fractional_ideal.right_inverse_eq (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] (I J : K) (h : I * J = 1) :
J = I⁻¹

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

theorem fractional_ideal.mul_inv_cancel_iff (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {I : K} :
I * I⁻¹ = 1 (J : , I * J = 1
theorem fractional_ideal.mul_inv_cancel_iff_is_unit (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {I : K} :
I * I⁻¹ = 1
@[simp]
theorem fractional_ideal.map_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {K' : Type u_5} [field K'] [algebra R₁ K'] [ K'] (I : K) (h : K ≃ₐ[R₁] K') :
@[simp]
theorem fractional_ideal.span_singleton_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] (x : K) :
@[simp]
theorem fractional_ideal.span_singleton_div_span_singleton (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] (x y : K) :
theorem fractional_ideal.span_singleton_div_self (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {x : K} (hx : x 0) :
theorem fractional_ideal.coe_ideal_span_singleton_div_self (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {x : R₁} (hx : x 0) :
theorem fractional_ideal.span_singleton_mul_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {x : K} (hx : x 0) :
theorem fractional_ideal.coe_ideal_span_singleton_mul_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {x : R₁} (hx : x 0) :
theorem fractional_ideal.span_singleton_inv_mul (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {x : K} (hx : x 0) :
theorem fractional_ideal.coe_ideal_span_singleton_inv_mul (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {x : R₁} (hx : x 0) :
theorem fractional_ideal.mul_generator_self_inv (K : Type u_3) [field K] {R₁ : Type u_1} [comm_ring R₁] [algebra R₁ K] [ K] (I : K) [I.is_principal] (h : I 0) :
theorem fractional_ideal.invertible_of_principal (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] (I : K) [I.is_principal] (h : I 0) :
I * I⁻¹ = 1
theorem fractional_ideal.invertible_iff_generator_nonzero (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] (I : K) [I.is_principal] :
I * I⁻¹ = 1
theorem fractional_ideal.is_principal_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] (I : K) [I.is_principal] (h : I 0) :
@[protected, instance]
noncomputable def fractional_ideal.inv_one_class (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] :
Equations
def is_dedekind_domain_inv (A : Type u_2) [comm_ring A] [is_domain A] :
Prop

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

This is equivalent to `is_dedekind_domain`. In particular we provide a `fractional_ideal.comm_group_with_zero` instance, assuming `is_dedekind_domain A`, which implies `is_dedekind_domain_inv`. For integral ideals, `is_dedekind_domain`(`_inv`) implies only `ideal.cancel_comm_monoid_with_zero`.

Equations
theorem is_dedekind_domain_inv_iff {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] :
(I : , I I * I⁻¹ = 1
theorem fractional_ideal.adjoin_integral_eq_one_of_is_unit {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] (x : K) (hx : x) (hI : is_unit ) :
theorem is_dedekind_domain_inv.mul_inv_eq_one {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] (h : is_dedekind_domain_inv A) {I : K} (hI : I 0) :
I * I⁻¹ = 1
theorem is_dedekind_domain_inv.inv_mul_eq_one {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] (h : is_dedekind_domain_inv A) {I : K} (hI : I 0) :
I⁻¹ * I = 1
@[protected]
theorem is_dedekind_domain_inv.is_unit {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] (h : is_dedekind_domain_inv A) {I : K} (hI : I 0) :

Showing one side of the equivalence between the definitions `is_dedekind_domain_inv` and `is_dedekind_domain` of Dedekind domains.

theorem exists_multiset_prod_cons_le_and_prod_not_le {A : Type u_2} [comm_ring A] [is_domain A] (hNF : ¬) {I M : ideal A} (hI0 : I ) (hIM : I M) [hM : M.is_maximal] :
(Z : ,

Specialization of `exists_prime_spectrum_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_prime_spectrum_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 fractional_ideal.exists_not_mem_one_of_ne_bot {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] (hNF : ¬) {I : ideal A} (hI0 : I ) (hI1 : I ) :
(x : K), x (I)⁻¹ x 1
theorem fractional_ideal.one_mem_inv_coe_ideal {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {I : ideal A} (hI : I ) :
theorem fractional_ideal.mul_inv_cancel_of_le_one {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] [h : is_dedekind_domain A] {I : ideal A} (hI0 : I ) (hI : (I * (I)⁻¹)⁻¹ 1) :
I * (I)⁻¹ = 1
theorem fractional_ideal.coe_ideal_mul_inv {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] [h : is_dedekind_domain 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.

@[protected]
theorem fractional_ideal.mul_inv_cancel {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {I : 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 `comm_group_with_zero` instance defined below.

theorem fractional_ideal.mul_right_le_iff {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {J : K} (hJ : J 0) {I I' : K} :
I * J I' * J I I'
theorem fractional_ideal.mul_left_le_iff {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {J : K} (hJ : J 0) {I I' : K} :
J * I J * I' I I'
theorem fractional_ideal.mul_right_strict_mono {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {I : K} (hI : I 0) :
theorem fractional_ideal.mul_left_strict_mono {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {I : K} (hI : I 0) :
@[protected]
theorem fractional_ideal.div_eq_mul_inv {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] (I J : K) :
I / J = I * J⁻¹

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

`is_dedekind_domain` and `is_dedekind_domain_inv` are equivalent ways to express that an integral domain is a Dedekind domain.

@[protected, instance]
noncomputable def fractional_ideal.semifield {A : Type u_2} (K : Type u_3) [comm_ring A] [field K] [is_domain A] [ K] [ K] :
Equations
@[protected, instance]
def fractional_ideal.cancel_comm_monoid_with_zero {A : Type u_2} (K : Type u_3) [comm_ring A] [field K] [is_domain A] [ K] [ K] :

Fractional ideals have cancellative multiplication in a Dedekind domain.

Although this instance is a direct consequence of the instance `fractional_ideal.comm_group_with_zero`, we define this instance to provide a computable alternative.

Equations
@[protected, instance]
Equations
@[protected, instance]
def ideal.is_domain {A : Type u_2} [comm_ring A] [is_domain A]  :
theorem ideal.dvd_iff_le {A : Type u_2} [comm_ring A] [is_domain A] {I J : ideal A} :
I J J I

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

theorem ideal.dvd_not_unit_iff_lt {A : Type u_2} [comm_ring A] [is_domain A] {I J : ideal A} :
J J < I
@[protected, instance]
def ideal.wf_dvd_monoid {A : Type u_2} [comm_ring A] [is_domain A]  :
@[protected, instance]
@[protected, instance]
Equations
@[simp]
theorem ideal.dvd_span_singleton {A : Type u_2} [comm_ring A] [is_domain A] {I : ideal A} {x : A} :
I ideal.span {x} x I
theorem ideal.is_prime_of_prime {A : Type u_2} [comm_ring A] [is_domain A] {P : ideal A} (h : prime P) :
theorem ideal.prime_of_is_prime {A : Type u_2} [comm_ring A] [is_domain A] {P : ideal A} (hP : P ) (h : P.is_prime) :
theorem ideal.prime_iff_is_prime {A : Type u_2} [comm_ring A] [is_domain A] {P : ideal A} (hP : P ) :

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

theorem ideal.is_prime_iff_bot_or_prime {A : Type u_2} [comm_ring A] [is_domain A] {P : ideal A} :

In a Dedekind domain, the the prime ideals are the zero ideal together with the prime elements of the monoid with zero `ideal A`.

theorem ideal.strict_anti_pow {A : Type u_2} [comm_ring A] [is_domain A] (I : ideal A) (hI0 : I ) (hI1 : I ) :
theorem ideal.pow_lt_self {A : Type u_2} [comm_ring A] [is_domain 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} [comm_ring A] [is_domain A] (I : ideal A) (hI0 : I ) (hI1 : I ) (e : ) :
(x : A) (H : x I ^ e), x I ^ (e + 1)
theorem ideal.eq_prime_pow_of_succ_lt_of_le {A : Type u_2} [comm_ring A] [is_domain A] {P I : ideal A} [P_prime : P.is_prime] (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} [comm_ring A] [is_domain A] {P : ideal A} [P_prime : P.is_prime] (hP : P ) (i : ) :
P ^ (i + 1) < P ^ i
theorem associates.le_singleton_iff {A : Type u_2} [comm_ring A] [is_domain A] (x : A) (n : ) (I : ideal A) :
theorem ideal.exist_integer_multiples_not_mem {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {J : ideal A} (hJ : J ) {ι : Type u_1} (s : finset ι) (f : ι K) {j : ι} (hjs : j s) (hjf : f j 0) :
(a : K), ( (i : ι), i s (a * f i)) (i : ι) (H : i s), a * f i J

Strengthening of `is_localization.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 `normalized_gcd_monoid (ideal A)`.

@[simp]
theorem ideal.sup_mul_inf {A : Type u_2} [comm_ring A] [is_domain A] (I J : ideal A) :
(I J) * (I J) = I * J
@[protected, instance]

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

Equations
@[simp]
theorem ideal.gcd_eq_sup {A : Type u_2} [comm_ring A] [is_domain A] (I J : ideal A) :
= I J
@[simp]
theorem ideal.lcm_eq_inf {A : Type u_2} [comm_ring A] [is_domain A] (I J : ideal A) :
= I J
theorem ideal.inf_eq_mul_of_coprime {A : Type u_2} [comm_ring A] [is_domain A] {I J : ideal A} (coprime : I J = ) :
I J = I * J
theorem prod_normalized_factors_eq_self {T : Type u_4} [comm_ring T] [is_domain T] {I : ideal T} (hI : I ) :
theorem count_le_of_ideal_ge {T : Type u_4} [comm_ring T] [is_domain T] {I J : ideal T} (h : I J) (hI : I ) (K : ideal T) :
theorem sup_eq_prod_inf_factors {T : Type u_4} [comm_ring T] [is_domain T] {I J : ideal T} (hI : I ) (hJ : J ) :
theorem irreducible_pow_sup {T : Type u_4} [comm_ring T] [is_domain T] {I J : ideal T} (hI : I ) (hJ : irreducible J) (n : ) :
J ^ n I =
theorem irreducible_pow_sup_of_le {T : Type u_4} [comm_ring T] [is_domain T] {I J : ideal T} (hJ : irreducible J) (n : ) (hn : n I) :
J ^ n I = J ^ n
theorem irreducible_pow_sup_of_ge {T : Type u_4} [comm_ring T] [is_domain T] {I J : ideal T} (hI : I ) (hJ : irreducible J) (n : ) (hn : I n) :
J ^ n I = 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 `height_one_spectrum` and provide lemmas to recover the facts that prime ideals of height one are prime and irreducible.

theorem is_dedekind_domain.height_one_spectrum.ext {R : Type u_1} {_inst_1 : comm_ring R} {_inst_5 : is_domain R} {_inst_6 : is_dedekind_domain R} (h : x.as_ideal = y.as_ideal) :
x = y
@[nolint, ext]

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.

Instances for `is_dedekind_domain.height_one_spectrum`
• is_dedekind_domain.height_one_spectrum.has_sizeof_inst
theorem is_dedekind_domain.height_one_spectrum.ext_iff {R : Type u_1} {_inst_1 : comm_ring R} {_inst_5 : is_domain R} {_inst_6 : is_dedekind_domain R}  :
x = y
@[protected, instance]

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

Equations
theorem is_dedekind_domain.height_one_spectrum.infi_localization_eq_bot (R : Type u_1) (K : Type u_3) [comm_ring R] [field K] [is_domain R] [ K] [hK : K] :

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 ideal_factors_fun_of_quot_hom {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [is_domain A] {I : ideal R} {J : ideal A} {f : R I →+* A J} (hf : function.surjective f) :
{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
@[simp]
theorem ideal_factors_fun_of_quot_hom_coe_coe {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [is_domain A] {I : ideal R} {J : ideal A} {f : R I →+* A J} (hf : function.surjective f) (X : {p : | p I}) :
X) = X))
@[simp]
theorem ideal_factors_fun_of_quot_hom_id {A : Type u_2} [comm_ring A] [is_domain A] {J : ideal A} :
theorem ideal_factors_fun_of_quot_hom_comp {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [is_domain A] {I : ideal R} {J : ideal A} {B : Type u_4} [comm_ring B] [is_domain B] {L : ideal B} {f : R I →+* A J} {g : A J →+* B L} (hf : function.surjective f) (hg : function.surjective g) :
def ideal_factors_equiv_of_quot_equiv {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [is_domain A] {I : ideal R} {J : ideal A} [is_domain R] (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
@[simp]
theorem ideal_factors_equiv_of_quot_equiv_symm_apply_coe_carrier {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [is_domain A] {I : ideal R} {J : ideal A} [is_domain R] (f : R I ≃+* A J) (a : {p : | p J}) :
@[simp]
theorem ideal_factors_equiv_of_quot_equiv_apply_coe_carrier {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [is_domain A] {I : ideal R} {J : ideal A} [is_domain R] (f : R I ≃+* A J) (a : {p : | p I}) :
theorem ideal_factors_equiv_of_quot_equiv_symm {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [is_domain A] {I : ideal R} {J : ideal A} [is_domain R] (f : R I ≃+* A J) :
theorem ideal_factors_equiv_of_quot_equiv_is_dvd_iso {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [is_domain A] {I : ideal R} {J : ideal A} [is_domain R] (f : R I ≃+* A J) {L M : ideal R} (hL : L I) (hM : M I) :
L, hL⟩) M, hM⟩) L M
@[simp]
theorem normalized_factors_equiv_of_quot_equiv_apply {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [is_domain A] {I : ideal R} {J : ideal A} [is_domain R] (f : R I ≃+* A J) [decidable_eq (ideal R)] [decidable_eq (ideal A)] (hI : I ) (hJ : J ) (j : {L : | ) :
j = j, _⟩), _⟩
def normalized_factors_equiv_of_quot_equiv {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [is_domain A] {I : ideal R} {J : ideal A} [is_domain R] (f : R I ≃+* A J) [decidable_eq (ideal R)] [decidable_eq (ideal A)] (hI : I ) (hJ : J ) :
{L : | {M : |

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

Equations
@[simp]
theorem normalized_factors_equiv_of_quot_equiv_symm {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [is_domain A] {I : ideal R} {J : ideal A} [is_domain R] (f : R I ≃+* A J) [decidable_eq (ideal R)] [decidable_eq (ideal A)] (hI : I ) (hJ : J ) :
theorem normalized_factors_equiv_of_quot_equiv_multiplicity_eq_multiplicity {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [is_domain A] {I : ideal R} {J : ideal A} [is_domain R] (f : R I ≃+* A J) [decidable_eq (ideal R)] [decidable_eq (ideal A)] (hI : I ) (hJ : J ) (L : ideal R)  :
multiplicity ( L, hL⟩) J = I

The map `normalized_factors_equiv_of_quot_equiv` preserves multiplicities.

theorem ring.dimension_le_one.prime_le_prime_iff_eq {R : Type u_1} [comm_ring R] (h : ring.dimension_le_one R) {P Q : ideal R} [hP : P.is_prime] [hQ : Q.is_prime] (hP0 : P ) :
P Q P = Q
theorem ideal.coprime_of_no_prime_ge {R : Type u_1} [comm_ring R] {I J : ideal R} (h : (P : ideal R), I P J P ¬P.is_prime) :
I J =
theorem ideal.is_prime.mul_mem_pow {R : Type u_1} [comm_ring R] [is_domain R] (I : ideal R) [hI : I.is_prime] {a b : R} {n : } (h : a * b I ^ n) :
a I b I ^ n
theorem ideal.count_normalized_factors_eq {R : Type u_1} [comm_ring R] [is_domain R] {p x : ideal R} [hp : p.is_prime] {n : } (hle : x p ^ n) (hlt : ¬x p ^ (n + 1)) :
theorem ideal.le_mul_of_no_prime_factors {R : Type u_1} [comm_ring R] [is_domain R] {I J K : ideal R} (coprime : (P : ideal R), J P K P ¬P.is_prime) (hJ : I J) (hK : I K) :
I J * K
theorem ideal.le_of_pow_le_prime {R : Type u_1} [comm_ring R] [is_domain R] {I P : ideal R} [hP : P.is_prime] {n : } (h : I ^ n P) :
I P
theorem ideal.pow_le_prime_iff {R : Type u_1} [comm_ring R] [is_domain R] {I P : ideal R} [hP : P.is_prime] {n : } (hn : n 0) :
I ^ n P I P
theorem ideal.prod_le_prime {R : Type u_1} [comm_ring R] [is_domain R] {ι : Type u_2} {s : finset ι} {f : ι } {P : ideal R} [hP : P.is_prime] :
s.prod (λ (i : ι), f i) P (i : ι) (H : i s), f i P
theorem is_dedekind_domain.inf_prime_pow_eq_prod {R : Type u_1} [comm_ring R] [is_domain R] {ι : Type u_2} (s : finset ι) (f : ι ) (e : ι ) (prime : (i : ι), i s _root_.prime (f i)) (coprime : (i : ι), i s (j : ι), j s i j f i f j) :
s.inf (λ (i : ι), f i ^ e i) = s.prod (λ (i : ι), f i ^ e i)

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

noncomputable def is_dedekind_domain.quotient_equiv_pi_of_prod_eq {R : Type u_1} [comm_ring R] [is_domain R] {ι : Type u_2} [fintype ι] (I : ideal R) (P : ι ) (e : ι ) (prime : (i : ι), _root_.prime (P i)) (coprime : (i j : ι), i j P i P j) (prod_eq : finset.univ.prod (λ (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
noncomputable def is_dedekind_domain.quotient_equiv_pi_factors {R : Type u_1} [comm_ring R] [is_domain R] {I : ideal R} (hI : I ) :
R I ≃+* Π (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
• = (λ (P : , is_dedekind_domain.quotient_equiv_pi_factors._proof_1 is_dedekind_domain.quotient_equiv_pi_factors._proof_2 _
@[simp]
theorem is_dedekind_domain.quotient_equiv_pi_factors_mk {R : Type u_1} [comm_ring R] [is_domain R] {I : ideal R} (hI : I ) (x : R) :
= λ (P : ,
noncomputable def ideal.quotient_mul_equiv_quotient_prod {R : Type u_1} [comm_ring R] [is_domain R] (I J : ideal R) (coprime : I J = ) :
R I * J ≃+* (R I) × R J

Chinese remainder theorem, specialized to two ideals.

Equations
• coprime = coprime)
theorem multiplicity_eq_multiplicity_span {R : Type u_1} [comm_ring R] [is_domain R] {a b : R} :
@[simp]
theorem normalized_factors_equiv_span_normalized_factors_symm_apply {R : Type u_1} [comm_ring R] [is_domain R] [decidable_eq R] [decidable_eq (ideal R)] {r : R} (hr : r 0) (b : {I : | ) :
noncomputable def normalized_factors_equiv_span_normalized_factors {R : Type u_1} [comm_ring R] [is_domain R] [decidable_eq R] [decidable_eq (ideal R)] {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
@[simp]
theorem normalized_factors_equiv_span_normalized_factors_apply_coe_carrier {R : Type u_1} [comm_ring R] [is_domain R] [decidable_eq R] [decidable_eq (ideal R)] {r : R} (hr : r 0) (d : {d : R | ) :
= (s : R) (x : d s), s

The bijection `normalized_factors_equiv_span_normalized_factors` between the set of prime factors of `r` and the set of prime factors of the ideal `⟨r⟩` preserves multiplicities.

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.