# Documentation

Mathlib.RingTheory.DedekindDomain.Factorization

# Factorization of 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. TODO: Extend the results in this file to fractional ideals of R.

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

## Tags #

dedekind domain, 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.

Instances For
theorem Ideal.finite_factors {R : Type u_1} [] [] [] {I : } (hI : I 0) :
Set.Finite {v | v.asIdeal I}

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.count (Associates.mk v.asIdeal) ()) = 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) :

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) :
Set.Finite (Function.mulSupport fun v => v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) ()))

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) :
Set.Finite (Function.mulSupport fun v => v.asIdeal ^ (-↑(Associates.count (Associates.mk v.asIdeal) ())))

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.count (Associates.mk v.asIdeal) () + 1)

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 : ) :
theorem Ideal.finprod_count {R : Type u_1} [] [] [] (I : ) (hI : I 0) :

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) :

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.count (Associates.mk v.asIdeal) ()) = I

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