Theorems · Theorem · commutative algebra

FractionalIdeal.finprod_heightOneSpectrum_factorization

∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {I : FractionalIdeal (nonZeroDivisors R) K},
  I ≠ 0 →
    ∀ {a : R} {J : Ideal R},
      I = FractionalIdeal.spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * ↑J →
        ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R),
            ↑v.asIdeal ^
              (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
                ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) =
          I

If I is a nonzero fractional ideal, a ∈ R, and J is an ideal of R such that I = a⁻¹J, then I is equal to the product ∏_v v^(val_v(J) - val_v(a)).

Defined in

Mathlib.RingTheory.DedekindDomain.Factorization

Cited by

2 results in Mathlib

Foundations

Depth 155 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFieldAlgebraIsFractionRingIsDedekindDomain