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 : FractionalIdeal (nonZeroDivisors R₁) K} {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 : 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') :
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

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 : Ideal A} {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 : 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'

    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
    • One or more equations did not get rendered due to their size.
    instance Ideal.isDomain {A : Type u_2} [CommRing A] [IsDedekindDomain 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
    Equations
    • =
    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 : Ideal A} {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 : FractionalIdeal (nonZeroDivisors A) K} {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 : FractionalIdeal (nonZeroDivisors A) K} {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 : Ideal A) (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 : 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.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 irreducible_pow_sup {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I : Ideal T} {J : Ideal T} (hI : I ) (hJ : Irreducible J) (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_iff {R : Type u_1} :
    ∀ {inst : CommRing R} (x y : IsDedekindDomain.HeightOneSpectrum R), x = y x.asIdeal = y.asIdeal
    theorem IsDedekindDomain.HeightOneSpectrum.ext {R : Type u_1} :
    ∀ {inst : CommRing R} (x y : IsDedekindDomain.HeightOneSpectrum R), x.asIdeal = y.asIdealx = y

    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
      Equations
      • =

      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.

        @[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 }) :
        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_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 : Ideal R} {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 ) :
              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) :

              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 : 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 : Ideal R} {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 : 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 : 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} [CommRing R] [IsDedekindDomain R] {p : Ideal R} {x : Ideal R} [hp : p.IsPrime] {n : } (hle : x p ^ n) [DecidableEq (Ideal R)] (hlt : ¬x p ^ (n + 1)) :
              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 PK P¬P.IsPrime) (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 : P.IsPrime] {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 : P.IsPrime] {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 : P.IsPrime] :
              is, f i P is, 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 : 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.

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

                    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.

                      theorem count_associates_factors_eq {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [DecidableEq (Ideal R)] [DecidableEq (Associates (Ideal R))] [(p : Associates (Ideal R)) → Decidable (Irreducible p)] (I : Ideal R) (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.