# 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 #

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 ().factors
Instances For
theorem Ideal.finite_factors {R : Type u_1} [] [] {I : } (hI : I 0) :
{v : | v.asIdeal I}.Finite

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

theorem Associates.finite_factors {R : Type u_1} [] [] {I : } (hI : I 0) :
∀ᶠ (v : ) in Filter.cofinite, ((Associates.mk v.asIdeal).count ().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} [] [] {I : } (hI : I 0) :
(Function.mulSupport fun (v : ) => 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} [] {K : Type u_2} [] [Algebra R K] [] [] {I : } (hI : I 0) :
(Function.mulSupport fun (v : ) => v.asIdeal ^ ((Associates.mk v.asIdeal).count ().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} [] {K : Type u_2} [] [Algebra R K] [] [] {I : } (hI : I 0) :
(Function.mulSupport fun (v : ) => v.asIdeal ^ (-((Associates.mk v.asIdeal).count ().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} [] [] (I : ) (hI : I 0) :
¬v.asIdeal ^ ((Associates.mk v.asIdeal).count ().factors + 1) ∏ᶠ (v : ), 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} [] [] (I : ) :
Associates.mk (∏ᶠ (v : ), v.maxPowDividing I) 0
theorem Ideal.finprod_count {R : Type u_1} [] [] (I : ) (hI : I 0) :
(Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : ), v.maxPowDividing I)).factors = (Associates.mk v.asIdeal).count ().factors

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

theorem Ideal.finprod_heightOneSpectrum_factorization {R : Type u_1} [] [] {I : } (hI : I 0) :
∏ᶠ (v : ), 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} [] (K : Type u_2) [] [Algebra R K] [] [] {I : } (hI : I 0) :
∏ᶠ (v : ), v.asIdeal ^ ((Associates.mk v.asIdeal).count ().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} [] {K : Type u_2} [] [Algebra R K] [] [] {I : } (hI : I 0) {a : R} {J : } (haJ : I = FractionalIdeal.spanSingleton () (() a)⁻¹ * J) :
∏ᶠ (v : ), v.asIdeal ^ (((Associates.mk v.asIdeal).count ().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} [] {K : Type u_2} [] [Algebra R K] [] [] {n : R} (hn : n 0) (d : ()) :
∏ᶠ (v : ), v.asIdeal ^ (((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {n})).factors) - ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {d})).factors)) =

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} [] {K : Type u_2} [] [Algebra R K] [] [] {I : } (hI : I 0) (k : K) (hk : ) :
∏ᶠ (v : ), v.asIdeal ^ (((Associates.mk v.asIdeal).count ().factors) - ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {()})).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} [] (K : Type u_2) [] [Algebra R K] [] [] (I : ) :

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.
Instances For
theorem FractionalIdeal.count_zero {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] :
= 0

val_v(0) = 0.

theorem FractionalIdeal.count_ne_zero {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] {I : } (hI : I 0) :
= ((Associates.mk v.asIdeal).count .factors) - ((Associates.mk v.asIdeal).count ().factors)
theorem FractionalIdeal.count_well_defined {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] {I : } (hI : I 0) {a : R} {J : } (h_aJ : I = FractionalIdeal.spanSingleton () (() a)⁻¹ * J) :
= ((Associates.mk v.asIdeal).count ().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} [] (K : Type u_2) [] [Algebra R K] [] [] {I : } {I' : } (hI : I 0) (hI' : I' 0) :

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

theorem FractionalIdeal.count_mul' {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] (I : ) (I' : ) :
FractionalIdeal.count K v (I * I') = if I 0 I' 0 then + 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} [] (K : Type u_2) [] [Algebra R K] [] [] :
= 0

val_v(1) = 0.

theorem FractionalIdeal.count_prod {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] {ι : Type u_3} (s : ) (I : ι) (hS : is, I i 0) :
FractionalIdeal.count K v (is, I i) = is, FractionalIdeal.count K v (I i)
theorem FractionalIdeal.count_pow {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] (n : ) (I : ) :
FractionalIdeal.count K v (I ^ n) = n *

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

theorem FractionalIdeal.count_self {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] :
FractionalIdeal.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} [] (K : Type u_2) [] [Algebra R K] [] [] (n : ) :
FractionalIdeal.count K v (v.asIdeal ^ n) = n

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

theorem FractionalIdeal.count_neg_zpow {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] (n : ) (I : ) :

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

theorem FractionalIdeal.count_inv {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] (I : ) :
= -
theorem FractionalIdeal.count_zpow {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] (n : ) (I : ) :
FractionalIdeal.count K v (I ^ n) = n *

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

theorem FractionalIdeal.count_zpow_self {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] (n : ) :
FractionalIdeal.count K v (v.asIdeal ^ n) = n

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

theorem FractionalIdeal.count_maximal_coprime {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] (hw : w v) :
FractionalIdeal.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} [] (K : Type u_2) [] [Algebra R K] [] [] :
FractionalIdeal.count K v w.asIdeal = if w = v then 1 else 0
theorem FractionalIdeal.count_finprod_coprime {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] (exps : ) :
FractionalIdeal.count K v (∏ᶠ (w : ) (_ : w v), w.asIdeal ^ exps w) = 0

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

theorem FractionalIdeal.count_finsupp_prod {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] (exps : ) :
FractionalIdeal.count K v (exps.prod fun (x : ) (x_1 : ) => x.asIdeal ^ x_1) = exps v
theorem FractionalIdeal.count_finprod {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] (exps : ) (h_exps : ∀ᶠ (v : ) in Filter.cofinite, exps v = 0) :
FractionalIdeal.count K v (∏ᶠ (v : ), 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} [] (K : Type u_2) [] [Algebra R K] [] [] {J : } (hJ : J 0) :
= ((Associates.mk v.asIdeal).count ().factors)
theorem FractionalIdeal.count_coe_nonneg {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] (J : ) :
0
theorem FractionalIdeal.count_mono {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] {I : } {J : } (hI : I 0) (h : I J) :
theorem FractionalIdeal.finprod_heightOneSpectrum_factorization' {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] {I : } (hI : I 0) :
∏ᶠ (v : ), v.asIdeal ^ = 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} [] {K : Type u_2} [] [Algebra R K] [] [] {I : } (hI : I 0) {a : R} {J : } (haJ : I = FractionalIdeal.spanSingleton () (() a)⁻¹ * J) :
∀ᶠ (v : ) in Filter.cofinite, ((Associates.mk v.asIdeal).count ().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} [] {K : Type u_2} [] [Algebra R K] [] [] (I : ) :
∀ᶠ (v : ) in Filter.cofinite, = 0

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