Documentation

Mathlib.RingTheory.DedekindDomain.Factorization

Factorization of ideals and fractional 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.

Similarly, every nonzero fractional 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 integers. We define FractionalIdeal.count K v I (abbreviated as val_v(I) in the documentation) to be n_v, and we prove some of its properties. If I = 0, we define val_v(I) = 0.

Main definitions #

Main results #

Implementation notes #

Since we are only interested in the factorization of nonzero fractional ideals, we define val_v(0) = 0 so that every val_v is in and we can avoid having to use WithTop.

Tags #

dedekind domain, fractional ideal, 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] [IsDedekindDomain R] {I : Ideal R} (hI : I 0) :
    {v : IsDedekindDomain.HeightOneSpectrum R | v.asIdeal I}.Finite

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

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

    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} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I : Ideal R} (hI : I 0) :
    (Function.mulSupport fun (v : IsDedekindDomain.HeightOneSpectrum R) => v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors)).Finite

    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} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I : Ideal R} (hI : I 0) :
    (Function.mulSupport fun (v : IsDedekindDomain.HeightOneSpectrum R) => v.asIdeal ^ (-((Associates.mk v.asIdeal).count (Associates.mk I).factors))).Finite

    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} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (I : Ideal R) (hI : I 0) :
    ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I

    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} [CommRing R] [IsDedekindDomain R] (I : Ideal R) :
    Associates.mk (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I) 0
    theorem Ideal.finprod_count {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (I : Ideal R) (hI : I 0) :
    (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I)).factors = (Associates.mk v.asIdeal).count (Associates.mk I).factors

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

    theorem Ideal.finprod_heightOneSpectrum_factorization {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} (hI : I 0) :
    ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I = I

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

    theorem Ideal.finprod_heightOneSpectrum_factorization_coe {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I : Ideal R} (hI : I 0) :
    ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors) = I

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

    Factorization of fractional ideals of Dedekind domains #

    theorem FractionalIdeal.finprod_heightOneSpectrum_factorization {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I 0) {a : R} {J : Ideal R} (haJ : I = FractionalIdeal.spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * J) :
    ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.asIdeal ^ (((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) = I

    If I is a nonzero fractional ideal, a ∈ R, and J is an ideal of R such that I = a⁻¹J, then I is equal to the product ∏_v v^(val_v(J) - val_v(a)).

    theorem FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {n : R} (hn : n 0) (d : (nonZeroDivisors R)) :
    ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.asIdeal ^ (((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {n})).factors) - ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {d})).factors)) = FractionalIdeal.spanSingleton (nonZeroDivisors R) (IsLocalization.mk' K n d)

    For a nonzero k = r/s ∈ K, the fractional ideal (k) is equal to the product ∏_v v^(val_v(r) - val_v(s)).

    theorem FractionalIdeal.finprod_heightOneSpectrum_factorization_principal {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I 0) (k : K) (hk : I = FractionalIdeal.spanSingleton (nonZeroDivisors R) k) :
    ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.asIdeal ^ (((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {Classical.choose })).factors) - ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {(Classical.choose )})).factors)) = I

    For a nonzero k = r/s ∈ K, the fractional ideal (k) is equal to the product ∏_v v^(val_v(r) - val_v(s)).

    If I is a nonzero fractional ideal, a ∈ R, and J is an ideal of R such that I = a⁻¹J, then we define val_v(I) as (val_v(J) - val_v(a)). If I = 0, we set val_v(I) = 0.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem FractionalIdeal.count_ne_zero {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I 0) :
      FractionalIdeal.count K v I = ((Associates.mk v.asIdeal).count (Associates.mk (Classical.choose )).factors) - ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {Classical.choose })).factors)
      theorem FractionalIdeal.count_well_defined {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I 0) {a : R} {J : Ideal R} (h_aJ : I = FractionalIdeal.spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * J) :
      FractionalIdeal.count K v I = ((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)

      val_v(I) does not depend on the choice of a and J used to represent I.

      For nonzero I, I', val_v(I*I') = val_v(I) + val_v(I').

      For nonzero I, I', val_v(I*I') = val_v(I) + val_v(I'). If I or I' is zero, then val_v(I*I') = 0.

      theorem FractionalIdeal.count_prod {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {ι : Type u_3} (s : Finset ι) (I : ιFractionalIdeal (nonZeroDivisors R) K) (hS : is, I i 0) :
      FractionalIdeal.count K v (is, I i) = is, FractionalIdeal.count K v (I i)

      For every n ∈ ℕ and every ideal I, val_v(I^n) = n*val_v(I).

      val_v(v) = 1, when v is regarded as a fractional ideal.

      theorem FractionalIdeal.count_pow_self {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ) :
      FractionalIdeal.count K v (v.asIdeal ^ n) = n

      val_v(v^n) = n for every n ∈ ℕ.

      val_v(I⁻ⁿ) = -val_v(Iⁿ) for every n ∈ ℤ.

      val_v(Iⁿ) = n*val_v(I) for every n ∈ ℤ.

      theorem FractionalIdeal.count_zpow_self {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ) :
      FractionalIdeal.count K v (v.asIdeal ^ n) = n

      val_v(v^n) = n for every n ∈ ℤ.

      If v ≠ w are two maximal ideals of R, then val_v(w) = 0.

      val_v(∏_{w ≠ v} w^{exps w}) = 0.

      theorem FractionalIdeal.count_finprod {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (exps : IsDedekindDomain.HeightOneSpectrum R) (h_exps : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, exps v = 0) :
      FractionalIdeal.count K v (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.asIdeal ^ exps v) = exps v

      If exps is finitely supported, then val_v(∏_w w^{exps w}) = exps v.

      theorem FractionalIdeal.count_coe {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {J : Ideal R} (hJ : J 0) :
      FractionalIdeal.count K v J = ((Associates.mk v.asIdeal).count (Associates.mk J).factors)

      If I is a nonzero fractional ideal, then I is equal to the product ∏_v v^(count K v I).

      theorem FractionalIdeal.finite_factors' {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I 0) {a : R} {J : Ideal R} (haJ : I = FractionalIdeal.spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * J) :
      ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, ((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = 0

      If I ≠ 0, then val_v(I) = 0 for all but finitely many maximal ideals of R.

      theorem FractionalIdeal.finite_factors {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (I : FractionalIdeal (nonZeroDivisors R) K) :
      ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, FractionalIdeal.count K v I = 0

      val_v(I) = 0 for all but finitely many maximal ideals of R.