Documentation

Mathlib.RingTheory.DedekindDomain.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 #

Main results: #

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 #

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] :
Equations
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) :
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⁻¹ yI, 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) :
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') :
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.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.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.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] :
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 ) :
noncomputable instance FractionalIdeal.instInvOneClassNonZeroDivisors {K : Type u_3} [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] :
Equations

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} [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] :
    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) :

    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)⁻¹, x1
    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.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.

    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] :
    Equations

    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
    Equations
    • Ideal.cancelCommMonoidWithZero = CancelCommMonoidWithZero.mk
    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
    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) :
    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.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 : ) :
    xI ^ e, xI ^ (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) :
    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) :
    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) :
    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), (∀ 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} [CommRing A] [IsDedekindDomain A] (I J : Ideal A) :
    (I J) * (I J) = I * J

    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} [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 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] :

    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.

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

      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

        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.
        Instances For
          @[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 }) :
          @[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) :
          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
          Instances For
            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

            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} [CommRing R] [CommRing A] [IsDedekindDomain A] {I : Ideal R} {J : Ideal A} [IsDedekindDomain R] (f : R I ≃+* A J) (hI : I ) (hJ : J ) :

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

              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 PK 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 : 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} [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
              Instances For
                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.
                Instances For
                  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 : 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} [CommRing R] [IsDedekindDomain R] {ι : Type u_4} {s : Finset ι} (P : ιIdeal R) (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} [CommRing R] [IsDedekindDomain R] {ι : Type u_4} {s : Finset ι} (P : ιIdeal R) (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.

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

                    Equations
                    Instances For

                      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.

                      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.

                      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.

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

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

                      Equations
                      Instances For
                        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] :
                        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