Complements on Dedekind-domain factorization

Facts about Associates.count and FractionalIdeal.count that Mathlib does not carry, together with unit-level factorization of invertible fractional ideals.

Main results

• IsDedekindDomain.HeightOneSpectrum.le_count_associates_iff_le_pow: the multiplicity of v in a nonzero J is at least k exactly when v ^ k contains J. The multiplicity here is Associates.count, not FractionalIdeal.count — hence the associates token, matching Mathlib's Ideal.count_associates_factors_eq for the same expression. Mathlib reads that multiplicity as divisibility of Associates; a consumer comparing two multiplicities across a ring extension wants a containment of ideals, and shows the two ideals contain the same prime powers.
• FractionalIdeal.count_div: the multiplicity of I / J is the difference of the multiplicities of I and J. Mathlib's count API has count_mul, count_inv, count_pow and count_zpow but no division form, so every consumer that clears a denominator repeats the same rewrites.
• FractionalIdeal.count_spanSingleton_div: the same on principal fractional ideals. This is the one the S-integer class-group computation in TauCeti/RingTheory/DedekindDomain/SInteger/ClassGroup.lean uses, at both R and 𝒪_S — which is why the ring is a variable rather than fixed — advancing TauCetiRoadmap/EllipticCurves/README.md §Layer 6 (Mordell–Weil), whose weak-Mordell–Weil argument needs the S-class group to be finite. It is also the step that carries count_toPrincipalIdeal_eq_neg_log_valuation below. count_div is its general form and has no consumer in this repository yet.
• FractionalIdeal.count_toPrincipalIdeal_eq_neg_log_valuation: the multiplicity at v of the principal fractional ideal of a nonzero rational function u : Kˣ is -WithZero.log (v.valuation K u). This is the passage between the two ways this library measures a principal ideal at a height one prime — Mathlib's count and the adic valuation.
• Ideal.hasFiniteMulSupport_asIdeal_pow_of_le_count: a family of prime powers whose exponents are bounded by the multiplicities of a fixed nonzero ideal has finite multiplicative support. Mathlib's Ideal.hasFiniteMulSupport is the case of the multiplicities themselves; a consumer defining an ideal as ∏ᵥ 𝔭ᵥ ^ e v for exponents it only knows to be dominated by an actual factorisation — as the minimal discriminant ideal of an elliptic curve is dominated by the discriminant of any integral model — needs the bounded form to see that the product is finite.
• IsDedekindDomain.HeightOneSpectrum.unitOfPrime: a height-one prime regarded as an invertible fractional ideal.
• FractionalIdeal.hasFiniteMulSupport_zpow_count: a family of powers indexed by the height one primes, with the multiplicities of a fixed fractional ideal as exponents, has finite multiplicative support. The bases are an arbitrary family in an arbitrary DivInvMonoid, since nothing but the vanishing of almost all exponents is at stake; the unit-level factorization below is the case of the primes themselves.
• FractionalIdeal.finprod_unitOfPrime_zpow_count: unique factorization of an invertible fractional ideal, transported along Units.coeHom.
• FractionalIdeal.mem_closure_unitOfPrime_of_count_eq_zero: an invertible fractional ideal whose multiplicities vanish outside a set T of height one primes lies in the subgroup generated by the primes of T.

All these declarations are general facts about an arbitrary Dedekind domain, mentioning no particular ring extension.

le_count_associates_iff_le_pow is adapted from Michael Stoll's elliptic-curves formalisation (github.com/MichaelStollBayreuth/EllipticCurves, EllipticCurves/Mathlib/Basic.lean:381 at the roadmap's pin 66889eada51a, Apache 2.0, by Michael Stoll); following this repository's convention for adapted material, the upstream authorship is credited here rather than in the copyright header. count_div and count_spanSingleton_div are new here — they have no counterpart in that source. count_toPrincipalIdeal_eq_neg_log_valuation is this repository's own, relocated here from TauCeti/AlgebraicGeometry/WeilDivisor/Dedekind/Basic.lean: nothing in its statement or proof mentions a Weil divisor, and stating it under TauCeti.AlgebraicGeometry put it out of reach of the RingTheory consumers that need it, which is exactly the boundary TauCeti/RingTheory/ClassGroup/HeightOneSpectrum.lean records in its module docstring.

The unit-level prime factorization FractionalIdeal.finprod_unitOfPrime_zpow_count is adapted from Michael Stoll's EllipticCurves/Mathlib/FractionalIdeal.lean at commit 66889eada51a of the MichaelStollBayreuth/EllipticCurves repository (Apache 2.0).

noncomputable def IsDedekindDomain.HeightOneSpectrum.unitOfPrime {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : (FractionalIdeal (nonZeroDivisors R) K)ˣ

A height-one prime, regarded as an invertible fractional ideal.

Equations

• v.unitOfPrime K = Units.mk0 ↑v.asIdeal ⋯

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.coe_unitOfPrime {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : ↑(v.unitOfPrime K) = ↑v.asIdeal

The fractional ideal underlying v.unitOfPrime K is v.asIdeal.

theorem IsDedekindDomain.HeightOneSpectrum.le_count_associates_iff_le_pow {A : Type u_2} [CommRing A] [IsDedekindDomain A] (v : HeightOneSpectrum A) {J : Ideal A} (hJ : J ≠ ⊥) (k : ℕ) : k ≤ (Associates.mk v.asIdeal).count (Associates.mk J).factors ↔ J ≤ v.asIdeal ^ k

The multiplicity of v in a nonzero ideal J is at least k exactly when v ^ k contains J.

theorem Ideal.hasFiniteMulSupport_asIdeal_pow_of_le_count {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ 0) (e : IsDedekindDomain.HeightOneSpectrum R → ℕ) (he : ∀ (v : IsDedekindDomain.HeightOneSpectrum R), e v ≤ (Associates.mk v.asIdeal).count (Associates.mk I).factors) : Function.HasFiniteMulSupport fun (v : IsDedekindDomain.HeightOneSpectrum R) => v.asIdeal ^ e v

A family of prime powers whose exponents are bounded by the multiplicities of a nonzero ideal has finite multiplicative support. This permits products of such prime powers to be handled as finite products.

theorem FractionalIdeal.hasFiniteMulSupport_zpow_count {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {G : Type u_3} [DivInvMonoid G] (I : FractionalIdeal (nonZeroDivisors R) K) (f : IsDedekindDomain.HeightOneSpectrum R → G) : (Function.mulSupport fun (v : IsDedekindDomain.HeightOneSpectrum R) => f v ^ count K v I).Finite

A prime-indexed family of powers with the multiplicities of a fractional ideal as exponents has finite multiplicative support. Only finitely many primes occur in a fractional ideal, so only finitely many exponents are nonzero, whatever DivInvMonoid the bases live in.

theorem FractionalIdeal.hasFiniteMulSupport_unitOfPrime_zpow {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : (Function.mulSupport fun (v : IsDedekindDomain.HeightOneSpectrum R) => v.unitOfPrime K ^ count K v ↑I).Finite

Only finitely many factors in the unit-level prime factorization are nontrivial.

theorem FractionalIdeal.finprod_unitOfPrime_zpow_count {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : I = ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.unitOfPrime K ^ count K v ↑I

Unique factorization of an invertible fractional ideal as a product of prime powers.

theorem FractionalIdeal.mem_closure_unitOfPrime_of_count_eq_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {T : Set (IsDedekindDomain.HeightOneSpectrum R)} {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ} (h : ∀ v ∉ T, count K v ↑I = 0) : I ∈ Subgroup.closure ((fun (v : IsDedekindDomain.HeightOneSpectrum R) => v.unitOfPrime K) '' T)

An invertible fractional ideal whose multiplicities vanish outside T lies in the subgroup generated by the primes of T.

theorem FractionalIdeal.count_div {A : Type u_3} [CommRing A] [IsDedekindDomain A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] (w : IsDedekindDomain.HeightOneSpectrum A) {I J : FractionalIdeal (nonZeroDivisors A) K} (hI : I ≠ 0) (hJ : J ≠ 0) : count K w (I / J) = count K w I - count K w J

The multiplicity of a quotient is the difference of the multiplicities. Mathlib's count API has count_mul, count_inv, count_pow and count_zpow but no division form, so every consumer that clears a denominator repeats the same rewrites.

theorem FractionalIdeal.count_spanSingleton_div {A : Type u_3} [CommRing A] [IsDedekindDomain A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] (w : IsDedekindDomain.HeightOneSpectrum A) {x y : K} (hx : x ≠ 0) (hy : y ≠ 0) : count K w (spanSingleton (nonZeroDivisors A) (x / y)) = count K w (spanSingleton (nonZeroDivisors A) x) - count K w (spanSingleton (nonZeroDivisors A) y)

The multiplicity of x / y is the difference of the multiplicities of x and y: count_div read on principal fractional ideals, which is the form the S-integer class-group computation uses.

theorem FractionalIdeal.count_toPrincipalIdeal_eq_neg_log_valuation {A : Type u_3} [CommRing A] [IsDedekindDomain A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] (v : IsDedekindDomain.HeightOneSpectrum A) (u : Kˣ) : count K v ↑((toPrincipalIdeal A K) u) = -((IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑u).log

The multiplicity of a principal fractional ideal is the sign-flipped logarithm of the valuation. Stated at the multiplicative-units level u : Kˣ, matching Mathlib's toPrincipalIdeal A K : Kˣ →* _.