# mathlib3documentation

ring_theory.dedekind_domain.factorization

# Factorization of ideals of Dedekind domains #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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_height_one_spectrum_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, max_pow_dividing returns the maximal power of v dividing I.

Equations
theorem ideal.finite_factors {R : Type u_1} [comm_ring R] [is_domain R] {I : ideal R} (hI : I 0) :
{v : | v.as_ideal I}.finite

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

theorem associates.finite_factors {R : Type u_1} [comm_ring R] [is_domain R] {I : ideal R} (hI : I 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_mul_support {R : Type u_1} [comm_ring R] [is_domain R] {I : ideal R} (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_mul_support_coe {R : Type u_1} [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ K] {I : ideal R} (hI : I 0) :

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_mul_support_inv {R : Type u_1} [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ K] {I : ideal R} (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.finprod_not_dvd {R : Type u_1} [comm_ring R] [is_domain R] (I : ideal R) (hI : I 0) :

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

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

theorem ideal.finprod_height_one_spectrum_factorization {R : Type u_1} [comm_ring R] [is_domain R] (I : ideal R) (hI : I 0) :
finprod (λ (v : , v.max_pow_dividing I) = I

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

theorem ideal.finprod_height_one_spectrum_factorization_coe {R : Type u_1} [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ K] (I : ideal R) (hI : I 0) :
finprod (λ (v : , (v.as_ideal) ^ .count .factors)) = I

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