Ideal.finite_mulSupport_coe
theorem Ideal.finite_mulSupport_coe :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
[inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] {I : Ideal R},
I ≠ 0 →
(Function.mulSupport fun v =>
↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors)).Finite
This theorem states that for any non-zero ideal `I` in a commutative ring `R`, which is also a Dedekind domain, there are only a finite number of maximal ideals `v` such that the power `v` raised to `val_v(I)`, when considered as a fractional ideal, is not equal to the unit ideal `(1)`. Here `v.asIdeal` represents the ideal associated with `v`, `Associates.mk v.asIdeal` and `Associates.mk I` are the class representatives of the ideals in the 'Associates' of the ring `R`, and `.factors` gives the prime factorization of the class representative. The `Function.mulSupport` for a function is the set of points where the function does not equal the multiplicative identity, in this case `1`. The theorem is asserting the finiteness of this set.
More concisely: In a commutative Dedekind domain, the number of maximal ideals `v` such that `v^(val_v(I))` is not a unit (i.e., not equal to the ideal (1)) for a given non-zero ideal `I`, is finite.
|
Ideal.finite_factors
theorem Ideal.finite_factors :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I : Ideal R},
I ≠ 0 → {v | v.asIdeal ∣ I}.Finite
This theorem states that in a Dedekind domain `R`, which is a commutative ring, any nonzero ideal `I` can only be divided by finitely many maximal ideals. Here, "dividing an ideal" means that the maximal ideal is a factor of the given ideal `I`. This theorem essentially describes an important property of Dedekind domains, where every nonzero ideal can be uniquely factored into a product of maximal ideals.
More concisely: In a commutative Dedekind domain, every nonzero ideal can be expressed as a finite product of maximal ideals.
|
Ideal.finite_mulSupport
theorem Ideal.finite_mulSupport :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I : Ideal R},
I ≠ 0 → (Function.mulSupport fun v => v.maxPowDividing I).Finite
The theorem `Ideal.finite_mulSupport` states that for every nonzero ideal `I` in a commutative ring `R` that also satisfies the property of being a Dedekind domain, there are only finitely many maximal ideals `v` such that the `v` raised to the power of `val_v(I)` is not the unit ideal. In other words, the set of all maximal ideals `v` where the ideal generated by `v` to the power `val_v(I)` does not equal the unit ideal (or equivalently, `v.maxPowDividing I` is not 1) is finite. The function `val_v(I)` in the context of this theorem is considered to be a function from the ideals of `R` to the non-negative integers, typically representing some form of valuation.
More concisely: In a commutative Dedekind domain R, the set of maximal ideals v such that v raised to the power of val_v(I) is not the unit ideal for a nonzero ideal I is finite.
|
Ideal.finprod_heightOneSpectrum_factorization
theorem Ideal.finprod_heightOneSpectrum_factorization :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (I : Ideal R),
I ≠ 0 → (finprod fun v => v.maxPowDividing I) = I
This theorem states that for any commutative ring `R` that is a Dedekind domain and any non-zero ideal `I` in `R`, the value of `I` is equal to the finite product of the maximum power of each `v` that divides `I`. Here, the finite product is over all `v` in the multiplicative support of the function. In mathematical notation, this is the statement that `I = ∏_v v^(val_v(I))`, where `val_v(I)` is the maximum power of `v` that divides `I`.
More concisely: For any commutative Dedekind domain `R` and non-zero ideal `I`, the ideal `I` is equal to the product of the `v` in its multiplicative support raised to the power of their valuation on `I`. That is, `I = ∏\_v v^(val\_v(I))`.
|
Ideal.finprod_not_dvd
theorem Ideal.finprod_not_dvd :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
(I : Ideal R),
I ≠ 0 →
¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
finprod fun v => v.maxPowDividing I
This theorem states that for any nonzero ideal `I` of a valuation `v` in a Dedekind domain `R`, the ideal `v` raised to the power of `(val_v(I) + 1)` does not divide the finite product of `v` raised to the power of `val_v(I)` over all `v`. Here, `val_v(I)` is the count of the occurrence of `v.asIdeal` in the factorization of `I` into prime ideals. The Dedekind domain is a commutative ring, has dimension one, and every nonzero prime ideal is maximal. The theorem implies that the power of an ideal in the product of ideals is strictly less than that in the ideal itself, which is a key characteristic in factorization in Dedekind domains.
More concisely: For any nonzero ideal I in a Dedekind domain of dimension one with every nonzero prime ideal maximal, the power of I in the product of powers of I over prime ideals containing I is strictly less than the power of I itself.
|
Ideal.finprod_heightOneSpectrum_factorization_coe
theorem Ideal.finprod_heightOneSpectrum_factorization_coe :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
[inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (I : Ideal R),
I ≠ 0 → (finprod fun v => ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors)) = ↑I
This theorem states that for any non-zero ideal `I` in a Dedekind domain `R`, which is also a field of fractions `K`, the ideal `I` can be expressed as the finite product of the fractional ideals `v.asIdeal` raised to the power of the count of `v.asIdeal` in the factorization of `I`. Here, the count and the product are taken over all non-zero integral ideals `v` of `R`. So, in simpler terms, it gives a unique factorization of a non-zero ideal into a product of prime ideals, each raised to a certain power, in the context of Dedekind domains.
More concisely: In a Dedekind domain with quotient field, any non-zero ideal can be expressed as a finite product of the corresponding fractional ideals of its prime ideals, each raised to a power equal to its multiplicity in the ideal's prime factorization.
|
Ideal.finprod_count
theorem Ideal.finprod_count :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
(I : Ideal R),
I ≠ 0 →
(Associates.mk v.asIdeal).count (Associates.mk (finprod fun v => v.maxPowDividing I)).factors =
(Associates.mk v.asIdeal).count (Associates.mk I).factors
This theorem is about the multiplicity of a prime ideal in a product over prime ideals in a Dedekind domain. Specifically, for a commutative ring `R` that is also a Dedekind domain, and for a given non-zero ideal `I` of `R`, and a height one prime ideal `v` of `R`, the multiplicity of `v` in the product over all height one prime ideals `v` of `v` to the power of the valuation of `I` at `v` equals the valuation of `I` at `v`. The valuation of an ideal `I` at a prime ideal `v` is defined as the largest non-negative integer `n` such that `v^n` divides `I`. This theorem essentially states a property that holds in the context of the factorization of ideals in Dedekind domains.
More concisely: In a Dedekind domain, for any ideal I and height one prime ideal v, the multiplicity of v in the product of I over all height one prime ideals equals the ideal valuation of I at v.
|
Ideal.finite_mulSupport_inv
theorem Ideal.finite_mulSupport_inv :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
[inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] {I : Ideal R},
I ≠ 0 →
(Function.mulSupport fun v =>
↑v.asIdeal ^ (-↑((Associates.mk v.asIdeal).count (Associates.mk I).factors))).Finite
This theorem states that for every non-zero ideal `I` in the domain `R`, which is a commutative ring and a Dedekind domain, and for which there exists a field of fractions `K`, there are finitely many maximal ideals `v` such that the multiplicative inverse of `v` raised to the value of `I` is not a unit ideal. In other words, the set of maximal ideals `v` for which `v` to the power of negative the count of `I` in the factorization of `v` does not result in a unit ideal, is finite.
More concisely: For every non-zero ideal `I` in a commutative Dedekind domain `R` with a field of fractions `K`, the set of maximal ideals `v` such that `v^(-n)` is not a unit ideal for some positive integer `n` representing the multiplicity of `I` in the prime factorization of `v`, is finite.
|
Associates.finite_factors
theorem Associates.finite_factors :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I : Ideal R},
I ≠ 0 →
∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite,
↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0
The theorem `Associates.finite_factors` states that in any commutative ring `R` that is also a Dedekind domain, for every nonzero ideal `I`, there are only finitely many maximal ideals `v` such that the multiplicity of `v` in the factorization of `I` (denoted as `val_v(I)`) is nonzero. In other words, only finitely many maximal ideals `v` contribute to the factorization of a given nonzero ideal `I`. The multiplicity of `v` is calculated as the count of `v` in the factors of `I` when both `I` and `v` are considered as elements of the ring's associated numbers (using the function `Associates.mk`). The theorem uses the 'cofinite filter', which is a way of specifying finiteness in a topological manner: a property holds 'cofinitely' if the set of elements for which it fails is finite.
More concisely: In a commutative Dedekind domain, every nonzero ideal has finitely many maximal ideals contributing to its factorization with non-zero multiplicity.
|