Factorization of ideals and fractional ideals of Dedekind domains

Every nonzero ideal I of a Dedekind domain R can be factored as a product ∏_v v^{n_v} over the maximal ideals of R, where the exponents n_v are natural numbers.

Similarly, every nonzero fractional ideal I of a Dedekind domain R can be factored as a product ∏_v v^{n_v} over the maximal ideals of R, where the exponents n_v are integers. We define FractionalIdeal.count K v I (abbreviated as val_v(I) in the documentation) to be n_v, and we prove some of its properties. If I = 0, we define val_v(I) = 0.

Main definitions

• FractionalIdeal.count : If I is a nonzero fractional ideal, a ∈ R, and J is an ideal of R such that I = a⁻¹J, then we define val_v(I) as (val_v(J) - val_v(a)). If I = 0, we set val_v(I) = 0.

Main results

• Ideal.finite_factors : Only finitely many maximal ideals of R divide a given nonzero ideal.
• Ideal.finprod_heightOneSpectrum_factorization : The ideal I equals the finprod ∏_v v^(val_v(I)), where val_v(I) denotes the multiplicity of v in the factorization of I and v runs over the maximal ideals of R.
• FractionalIdeal.finprod_heightOneSpectrum_factorization : 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)).
  • FractionalIdeal.finprod_heightOneSpectrum_factorization' : If I is a nonzero fractional ideal, then I is equal to the product ∏_v v^(val_v(I)).
• FractionalIdeal.finprod_heightOneSpectrum_factorization_principal : For a nonzero k = r/s ∈ K, the fractional ideal (k) is equal to the product ∏_v v^(val_v(r) - val_v(s)).
• FractionalIdeal.finite_factors : If I ≠ 0, then val_v(I) = 0 for all but finitely many maximal ideals of R.

Implementation notes

Since we are only interested in the factorization of nonzero fractional ideals, we define val_v(0) = 0 so that every val_v is in ℤ and we can avoid having to use WithTop ℤ.

Tags

dedekind domain, fractional ideal, ideal, factorization

Factorization of ideals of Dedekind domains

def IsDedekindDomain.HeightOneSpectrum.maxPowDividing {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) (I : Ideal R) : Ideal R

Given a maximal ideal v and an ideal I of R, maxPowDividing returns the maximal power of v dividing I.

Equations

• v.maxPowDividing I = v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors

theorem Ideal.finite_factors {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ 0) : {v : IsDedekindDomain.HeightOneSpectrum R | v.asIdeal ∣ I}.Finite

Only finitely many maximal ideals of R divide a given nonzero ideal.

theorem Associates.finite_factors {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ 0) : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0

For every nonzero ideal I of v, there are finitely many maximal ideals v such that the multiplicity of v in the factorization of I, denoted val_v(I), is nonzero.

theorem Ideal.finite_mulSupport {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ 0) : (Function.mulSupport fun (v : IsDedekindDomain.HeightOneSpectrum R) => v.maxPowDividing I).Finite

For every nonzero ideal I of v, there are finitely many maximal ideals v such that v^(val_v(I)) is not the unit ideal.

theorem Ideal.finite_mulSupport_coe {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ 0) : (Function.mulSupport fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors)).Finite

For every nonzero ideal I of v, there are finitely many maximal ideals v such that v^(val_v(I)), regarded as a fractional ideal, is not (1).

theorem Ideal.finite_mulSupport_inv {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ 0) : (Function.mulSupport fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑v.asIdeal ^ (-↑((Associates.mk v.asIdeal).count (Associates.mk I).factors))).Finite

For every nonzero ideal I of v, there are finitely many maximal ideals v such that v^-(val_v(I)) is not the unit ideal.

theorem Ideal.finprod_not_dvd {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (I : Ideal R) (hI : I ≠ 0) : ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣ ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I

For every nonzero ideal I of v, v^(val_v(I) + 1) does not divide ∏_v v^(val_v(I)).

theorem Associates.finprod_ne_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] (I : Ideal R) : Associates.mk (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I) ≠ 0

theorem Ideal.finprod_count {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (I : Ideal R) (hI : I ≠ 0) : (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I)).factors = (Associates.mk v.asIdeal).count (Associates.mk I).factors

The multiplicity of v in ∏_v v^(val_v(I)) equals val_v(I).

theorem Ideal.finprod_heightOneSpectrum_factorization {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ 0) : ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I = I

The ideal I equals the finprod ∏_v v^(val_v(I)).

theorem Ideal.finprod_heightOneSpectrum_factorization_coe {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ 0) : ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = ↑I

The ideal I equals the finprod ∏_v v^(val_v(I)), when both sides are regarded as fractional ideals of R.

Factorization of fractional ideals of Dedekind domains

theorem FractionalIdeal.finprod_heightOneSpectrum_factorization {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I ≠ 0) {a : R} {J : Ideal R} (haJ : I = 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)).

theorem FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {n : R} (hn : n ≠ 0) (d : ↥(nonZeroDivisors R)) : ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {n})).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) = spanSingleton (nonZeroDivisors R) (IsLocalization.mk' K n d)

For a nonzero k = r/s ∈ K, the fractional ideal (k) is equal to the product ∏_v v^(val_v(r) - val_v(s)).

theorem FractionalIdeal.finprod_heightOneSpectrum_factorization_principal {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I ≠ 0) (k : K) (hk : I = spanSingleton (nonZeroDivisors R) k) : ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑(Classical.choose ⋯)})).factors)) = I

For a nonzero k = r/s ∈ K, the fractional ideal (k) is equal to the product ∏_v v^(val_v(r) - val_v(s)).

def FractionalIdeal.count {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (I : FractionalIdeal (nonZeroDivisors R) K) : ℤ

If I is a nonzero fractional ideal, a ∈ R, and J is an ideal of R such that I = a⁻¹J, then we define val_v(I) as (val_v(J) - val_v(a)). If I = 0, we set val_v(I) = 0.

Equations

• One or more equations did not get rendered due to their size.

theorem FractionalIdeal.count_zero {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) : count K v 0 = 0

val_v(0) = 0.

theorem FractionalIdeal.count_ne_zero {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I ≠ 0) : count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors)

theorem FractionalIdeal.count_well_defined {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I ≠ 0) {a : R} {J : Ideal R} (h_aJ : I = spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * ↑J) : count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)

val_v(I) does not depend on the choice of a and J used to represent I.

theorem FractionalIdeal.count_mul {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {I I' : FractionalIdeal (nonZeroDivisors R) K} (hI : I ≠ 0) (hI' : I' ≠ 0) : count K v (I * I') = count K v I + count K v I'

For nonzero I, I', val_v(I*I') = val_v(I) + val_v(I').

theorem FractionalIdeal.count_mul' {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (I I' : FractionalIdeal (nonZeroDivisors R) K) [Decidable (I ≠ 0 ∧ I' ≠ 0)] : count K v (I * I') = if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 0

For nonzero I, I', val_v(I*I') = val_v(I) + val_v(I'). If I or I' is zero, then val_v(I*I') = 0.

theorem FractionalIdeal.count_one {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) : count K v 1 = 0

val_v(1) = 0.

theorem FractionalIdeal.count_prod {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {ι : Type u_3} (s : Finset ι) (I : ι → FractionalIdeal (nonZeroDivisors R) K) (hS : ∀ i ∈ s, I i ≠ 0) : count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)

theorem FractionalIdeal.count_pow {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℕ) (I : FractionalIdeal (nonZeroDivisors R) K) : count K v (I ^ n) = ↑n * count K v I

For every n ∈ ℕ and every ideal I, val_v(I^n) = n*val_v(I).

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

val_v(v) = 1, when v is regarded as a fractional ideal.

theorem FractionalIdeal.count_pow_self {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℕ) : count K v (↑v.asIdeal ^ n) = ↑n

val_v(v^n) = n for every n ∈ ℕ.

theorem FractionalIdeal.count_neg_zpow {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℤ) (I : FractionalIdeal (nonZeroDivisors R) K) : count K v (I ^ (-n)) = -count K v (I ^ n)

val_v(I⁻ⁿ) = -val_v(Iⁿ) for every n ∈ ℤ.

theorem FractionalIdeal.count_inv {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (I : FractionalIdeal (nonZeroDivisors R) K) : count K v I⁻¹ = -count K v I

theorem FractionalIdeal.count_zpow {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℤ) (I : FractionalIdeal (nonZeroDivisors R) K) : count K v (I ^ n) = n * count K v I

val_v(Iⁿ) = n*val_v(I) for every n ∈ ℤ.

theorem FractionalIdeal.count_zpow_self {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℤ) : count K v (↑v.asIdeal ^ n) = n

val_v(v^n) = n for every n ∈ ℤ.

theorem FractionalIdeal.count_maximal_coprime {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {w : IsDedekindDomain.HeightOneSpectrum R} (hw : w ≠ v) : count K v ↑w.asIdeal = 0

If v ≠ w are two maximal ideals of R, then val_v(w) = 0.

theorem FractionalIdeal.count_maximal {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v w : IsDedekindDomain.HeightOneSpectrum R) [Decidable (w = v)] : count K v ↑w.asIdeal = if w = v then 1 else 0

theorem FractionalIdeal.count_finprod_coprime {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (exps : IsDedekindDomain.HeightOneSpectrum R → ℤ) : count K v (∏ᶠ (w : IsDedekindDomain.HeightOneSpectrum R) (_ : w ≠ v), ↑w.asIdeal ^ exps w) = 0

val_v(∏_{w ≠ v} w^{exps w}) = 0.

theorem FractionalIdeal.count_finsupp_prod {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (exps : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ) : count K v (exps.prod fun (x1 : IsDedekindDomain.HeightOneSpectrum R) (x2 : ℤ) => ↑x1.asIdeal ^ x2) = exps v

theorem FractionalIdeal.count_finprod {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (exps : IsDedekindDomain.HeightOneSpectrum R → ℤ) (h_exps : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, exps v = 0) : count K v (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ exps v) = exps v

If exps is finitely supported, then val_v(∏_w w^{exps w}) = exps v.

theorem FractionalIdeal.count_coe {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {J : Ideal R} (hJ : J ≠ 0) : count K v ↑J = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)

theorem FractionalIdeal.count_coe_nonneg {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (J : Ideal R) : 0 ≤ count K v ↑J

theorem FractionalIdeal.count_mono {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {I J : FractionalIdeal (nonZeroDivisors R) K} (hI : I ≠ 0) (h : I ≤ J) : count K v J ≤ count K v I

theorem FractionalIdeal.finprod_heightOneSpectrum_factorization' {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I ≠ 0) : ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ count K v I = I

If I is a nonzero fractional ideal, then I is equal to the product ∏_v v^(count K v I).

theorem FractionalIdeal.finite_factors' {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I ≠ 0) {a : R} {J : Ideal R} (haJ : I = spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * ↑J) : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = 0

If I ≠ 0, then val_v(I) = 0 for all but finitely many maximal ideals of R.

theorem FractionalIdeal.finite_factors {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (I : FractionalIdeal (nonZeroDivisors R) K) : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, count K v I = 0

val_v(I) = 0 for all but finitely many maximal ideals of R.