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 #

source
def IsDedekindDomain.HeightOneSpectrum.maxPowDividing {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (I : Ideal R) :
Ideal R

Given a maximal ideal v and an ideal I of R, maxPowDividing returns the maximal power of v dividing I.

Equations
Instances For
    source
    theorem Ideal.finite_factors {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ 0) :
    Set.Finite {v : IsDedekindDomain.HeightOneSpectrum R | v.asIdeal ∣ I}

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

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

    source
    theorem Ideal.finite_mulSupport {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ 0) :
    Set.Finite (Function.mulSupport fun (v : IsDedekindDomain.HeightOneSpectrum R) => IsDedekindDomain.HeightOneSpectrum.maxPowDividing v I)

    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.

    source
    theorem Ideal.finite_mulSupport_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) :
    Set.Finite (Function.mulSupport fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))

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

    source
    theorem Ideal.finite_mulSupport_inv {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) :
    Set.Finite (Function.mulSupport fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑v.asIdeal ^ (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))

    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.

    source
    theorem Ideal.finprod_not_dvd {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (I : Ideal R) (hI : I ≠ 0) :
    ¬v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1) ∣ finprod fun (v : IsDedekindDomain.HeightOneSpectrum R) => IsDedekindDomain.HeightOneSpectrum.maxPowDividing v I

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

    source
    theorem Associates.finprod_ne_zero {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (I : Ideal R) :
    Associates.mk (finprod fun (v : IsDedekindDomain.HeightOneSpectrum R) => IsDedekindDomain.HeightOneSpectrum.maxPowDividing v I) ≠ 0
    source
    theorem Ideal.finprod_count {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (I : Ideal R) (hI : I ≠ 0) :
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (finprod fun (v : IsDedekindDomain.HeightOneSpectrum R) => IsDedekindDomain.HeightOneSpectrum.maxPowDividing v I))) = Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))

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

    source
    theorem Ideal.finprod_heightOneSpectrum_factorization {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (I : Ideal R) (hI : I ≠ 0) :
    (finprod fun (v : IsDedekindDomain.HeightOneSpectrum R) => IsDedekindDomain.HeightOneSpectrum.maxPowDividing v I) = I

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

    source
    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) :
    (finprod fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))) = ↑I

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