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 #

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.

Equations
Instances For
    theorem Ideal.finite_factors {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {I : Ideal R} (hI : I 0) :

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

    theorem Associates.finite_factors {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {I : Ideal R} (hI : I 0) :
    ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 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.

    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 ideal I equals the finprod ∏_v v^(val_v(I)).

    theorem Ideal.finprod_heightOneSpectrum_factorization_coe {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (I : Ideal R) (hI : I 0) :

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