Fractional-Ideal Prime-Valuation Faithfulness

Abstract

All nonzero-prime valuation coordinates faithfully recover a nonzero fractional ideal.

Theorem 1.1 (All prime-ideal valuations determine the fractional ideal).

$$\begin{gathered} \forall R,K:Type, \\ \mathrm{CommRing}(R)\wedge \mathrm{Field}(K)\wedge \mathrm{Algebra}(R,K)\wedge \mathrm{IsFractionRing}(R,K)\wedge \mathrm{IsDedekindDomain}(R)\Rightarrow \\ \forall I,J\in \mathrm{NonzeroFractionalIdeals}(R,K), \\ \forall p\in \mathrm{HeightOneSpectrum}(R),\mathrm{count}(K,p,I)=\mathrm{count}(K,p,J)\Rightarrow I=J. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Embeddings/FractionalIdealPrimeValuationFaithfulness.prime_valuation_observers_faithful (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let R be a Dedekind domain and K a fraction field of R. The two objects are nonzero fractional ideals, exactly the carrier on which the prime-ideal exponents form group coordinates.

Each element of the height-one spectrum represents a nonzero prime ideal. The displayed premise compares the canonical integer count at every such prime.

The pinned library reconstruction theorem expresses each nonzero fractional ideal as the finite product of those prime powers. Pointwise equality of all exponents therefore identifies the two ideals.

References

• Truth anchor: D5/S3/Factorization/Embeddings/FractionalIdealPrimeValuationFaithfulness.prime_valuation_observers_faithful