mathlib3 documentation

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 #

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

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

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.

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.

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

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.

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

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

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

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