Prime factorization of fractional ideals

DefinitionSupport of the prime exponents of a fractional ideal#✓fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\). For a unit fractional ideal \(I\) of \(R\) in \(K\), this is the finite set of height-one primes \(v\) of \(R\) at which the \(v\)-adic valuation of \(I\) is nonzero.

noncomputable def unitsSupportFinset (u : (FractionalIdeal R⁰ K)ˣ) :
    Finset (HeightOneSpectrum R) :=
  (Filter.eventually_cofinite.mp (finite_factors (u : FractionalIdeal R⁰ K))).toFinset

Used by 2

Used byReconstructing a fractional ideal from its prime exponents · Prime exponents of an invertible fractional ideal

DefinitionPrime exponents of an invertible fractional ideal#✓fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\), and let \(I\) be a unit of the monoid of fractional ideals of \(R\) in \(K\). The prime exponents of \(I\) form the finitely supported function from the height-one primes of \(R\) to \(\mathbb{Z}\) that sends each height-one prime \(v\) to the exponent \(\operatorname{ord}_v(I)\) of \(v\) in the factorization \(I = \prod_v v^{\operatorname{ord}_v(I)}\); its support is the finite set of \(v\) with \(\operatorname{ord}_v(I) \neq 0\).

noncomputable def unitsToFinsupp (u : (FractionalIdeal R⁰ K)ˣ) :
    HeightOneSpectrum R →₀ ℤ :=
  Finsupp.onFinset (unitsSupportFinset K u) (fun v => count K v (u : FractionalIdeal R⁰ K))
    (fun v hv => (mem_unitsSupportFinset K u v).mpr hv)

Uses 1 · Used by 5

Statement usesSupport of the prime exponents of a fractional ideal

Used byThe coprime primes generate the coprime ideals · Prime factorization isomorphism for fractional ideals · Reconstructing a fractional ideal from its prime exponents · Recovering prime exponents from a product of prime powers · Prime exponents are additive

TheoremProducts of prime powers are nonzero#✓fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\). For every finitely supported function \(e\) from the height-one primes of \(R\) to \(\mathbb{Z}\), the fractional ideal \(\prod_v v^{e(v)}\) of \(R\) in \(K\), the product over the primes \(v\) with \(e(v) \neq 0\), is nonzero.

theorem finsuppProd_ne_zero (e : HeightOneSpectrum R →₀ ℤ) :
    e.prod (fun v n => (v.asIdeal : FractionalIdeal R⁰ K) ^ n) ≠ 0

Used by 1

Used byFractional ideal with prescribed prime exponents

DefinitionFractional ideal with prescribed prime exponents#✓fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\). For a finitely supported function \(e\) from the height-one primes of \(R\) to \(\mathbb{Z}\), this is the fractional ideal \(\prod_v v^{e(v)}\) of \(R\) in \(K\), the product over the primes \(v\) with \(e(v) \neq 0\), regarded as a unit of the monoid of fractional ideals (it is nonzero, hence invertible).

noncomputable def finsuppToUnits (e : HeightOneSpectrum R →₀ ℤ) :
    (FractionalIdeal R⁰ K)ˣ :=
  Units.mk0 _ (finsuppProd_ne_zero K e)

Uses 1 · Used by 5

Statement usesProducts of prime powers are nonzero

Used byThe coprime primes generate the coprime ideals · Valuations of a product of prime powers · Prime factorization isomorphism for fractional ideals · Reconstructing a fractional ideal from its prime exponents · Recovering prime exponents from a product of prime powers

TheoremValuations of a product of prime powers#✓fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\). For every finitely supported function \(e\) from the height-one primes of \(R\) to \(\mathbb{Z}\) and every height-one prime \(v\) of \(R\), the \(v\)-adic valuation of the fractional ideal \(\prod_w w^{e(w)}\), the product over the primes \(w\) with \(e(w) \neq 0\), equals \(e(v)\).

@[simp]
theorem count_finsuppToUnits (v : HeightOneSpectrum R) (e : HeightOneSpectrum R →₀ ℤ) :
    count K v (↑(finsuppToUnits K e) : FractionalIdeal R⁰ K) = e v

Uses 1

Statement usesFractional ideal with prescribed prime exponents

TheoremReconstructing a fractional ideal from its prime exponents#✓fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\), and for a unit fractional ideal \(I\) of \(R\) in \(K\) and a height-one prime \(v\) of \(R\) write \(\operatorname{val}_v(I)\) for the \(v\)-adic valuation of \(I\). Every unit fractional ideal \(I\) of \(R\) in \(K\) equals \(\prod_v v^{\operatorname{val}_v(I)}\), the product over the height-one primes \(v\) of \(R\) with \(\operatorname{val}_v(I) \neq 0\).

theorem toUnits_left_inv (u : (FractionalIdeal R⁰ K)ˣ) :
    finsuppToUnits K (unitsToFinsupp K u) = u

Uses 3 · Used by 2

Statement usesFractional ideal with prescribed prime exponents · Prime exponents of an invertible fractional ideal

Proof usesSupport of the prime exponents of a fractional ideal

Used byThe coprime primes generate the coprime ideals · Prime factorization isomorphism for fractional ideals

TheoremRecovering prime exponents from a product of prime powers#✓fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\), and let \(e\) be a finitely supported function from the height-one primes of \(R\) to \(\mathbb{Z}\). The prime-exponent function of the fractional ideal \(\prod_w w^{e(w)}\), the product over the primes \(w\) with \(e(w) \neq 0\), is \(e\): its \(v\)-adic valuation is \(e(v)\) for every height-one prime \(v\) of \(R\).

theorem toUnits_right_inv (e : HeightOneSpectrum R →₀ ℤ) :
    unitsToFinsupp K (finsuppToUnits K e) = e

Uses 2 · Used by 1

Statement usesFractional ideal with prescribed prime exponents · Prime exponents of an invertible fractional ideal

Used byPrime factorization isomorphism for fractional ideals

TheoremPrime exponents are additive#✓fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\), and for a unit fractional ideal \(I\) of \(R\) in \(K\) and a height-one prime \(v\) of \(R\) write \(\operatorname{val}_v(I)\) for the \(v\)-adic valuation of \(I\). For all unit fractional ideals \(I\) and \(J\) of \(R\) in \(K\) and every height-one prime \(v\) of \(R\), \(\operatorname{val}_v(IJ) = \operatorname{val}_v(I) + \operatorname{val}_v(J)\).

theorem unitsToFinsupp_mul (u v : (FractionalIdeal R⁰ K)ˣ) :
    unitsToFinsupp K (u * v) = unitsToFinsupp K u + unitsToFinsupp K v

Uses 1 · Used by 1

Statement usesPrime exponents of an invertible fractional ideal

Used byPrime factorization isomorphism for fractional ideals

DefinitionPrime factorization isomorphism for fractional ideals#✓fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\), and for a unit fractional ideal \(I\) of \(R\) in \(K\) and a height-one prime \(v\) of \(R\) write \(\operatorname{val}_v(I)\) for the \(v\)-adic valuation of \(I\). The factorization isomorphism is the group isomorphism from the unit group of the fractional ideals of \(R\) in \(K\) to the additive group of finitely supported functions from the height-one primes of \(R\) to \(\mathbb{Z}\) (written multiplicatively) that sends \(I\) to the function \(v \mapsto \operatorname{val}_v(I)\). Its inverse sends \(e\) to \(\prod_v v^{e(v)}\), the product over the primes \(v\) with \(e(v) \neq 0\).

FractionalIdeal.factorizationMulEquiv · 15 lines

noncomputable def factorizationMulEquiv :
    (FractionalIdeal R⁰ K)ˣ ≃* Multiplicative (HeightOneSpectrum R →₀ ℤ) where
  toFun u := Multiplicative.ofAdd (unitsToFinsupp K u)
  invFun e := finsuppToUnits K (Multiplicative.toAdd e)
  left_inv u := by
    change finsuppToUnits K
      (Multiplicative.toAdd (Multiplicative.ofAdd (unitsToFinsupp K u))) = u
    rw [toAdd_ofAdd]
    exact toUnits_left_inv K u
  right_inv e := by
    change Multiplicative.ofAdd
      (unitsToFinsupp K (finsuppToUnits K (Multiplicative.toAdd e))) = e
    rw [toUnits_right_inv, ofAdd_toAdd]
  map_mul' u v := by
    rw [← ofAdd_add, unitsToFinsupp_mul]

Uses 5 · Used by 5

Statement usesFractional ideal with prescribed prime exponents · Reconstructing a fractional ideal from its prime exponents · Recovering prime exponents from a product of prime powers · Prime exponents of an invertible fractional ideal · Prime exponents are additive

Used byFactorization of a prime of a number field · The kernel of the free-group map lies in the commutator subgroup · Primes not dividing the modulus are coprime to it · Exponent function of a prime ideal · Inverse factorization of a single prime power

TheoremExponent function of a prime ideal#✓fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\) and let \(w\) be a height-one prime of \(R\). The factorization isomorphism sends the fractional ideal \(w\), as a unit fractional ideal of \(R\) in \(K\), to the function on height-one primes of \(R\) that is \(1\) at \(w\) and \(0\) elsewhere.

theorem factorizationMulEquiv_prime_self (w : HeightOneSpectrum R) :
    Multiplicative.toAdd
        (factorizationMulEquiv K
          (Units.mk0 _ (coeIdeal_ne_zero.mpr w.ne_bot))) =
      Finsupp.single w 1

Uses 1 · Used by 1

Statement usesPrime factorization isomorphism for fractional ideals

Used byFactorization of a prime of a number field

TheoremInverse factorization of a single prime power#✓fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\), let \(w\) be a height-one prime of \(R\) and let \(n \in \mathbb{Z}\). The inverse of the factorization isomorphism sends the function on height-one primes of \(R\) that is \(n\) at \(w\) and \(0\) elsewhere to the fractional ideal \(w^n\).

theorem symm_single_zpow (w : HeightOneSpectrum R) (n : ℤ) :
    (↑((factorizationMulEquiv K).symm (Multiplicative.ofAdd (Finsupp.single w n))) :
      FractionalIdeal R⁰ K) = (w.asIdeal : FractionalIdeal R⁰ K) ^ n

Uses 1

Statement usesPrime factorization isomorphism for fractional ideals

TheoremFinitely many primes contain a nonzero element#✓fully proved

In a Dedekind domain \(A\), every nonzero element \(a\) lies in only finitely many prime ideals of \(A\).

theorem Ideal.finite_setOf_isPrime_and_mem {a : A} (ha : a ≠ 0) :
    Set.Finite {P : Ideal A | P.IsPrime ∧ a ∈ P}

Sources

• ATLAS NumberTheoryI Lemma 3.6.

TheoremFinitely many primes contain a nonzero ideal#✓fully proved

In a Dedekind domain \(A\), every nonzero ideal \(I\) is contained in only finitely many prime ideals of \(A\).

theorem Ideal.finite_setOf_isPrime_and_le {I : Ideal A} (hI : I ≠ ⊥) :
    {p : Ideal A | p.IsPrime ∧ I ≤ p}.Finite

Sources

• ATLAS NumberTheoryI Corollary 3.7.

TheoremVanishing multiplicity of a prime factor#✓fully proved

Let \(A\) be a Dedekind domain, let \(\mathfrak p\) be a prime ideal of \(A\) and let \(I\) be a nonzero ideal of \(A\). Then the multiplicity of \(\mathfrak p\) in the factorization of \(I\) into prime ideals is zero if and only if \(I \not\subseteq \mathfrak p\).

In particular, if \(\mathfrak p\) and \(\mathfrak q\) are distinct nonzero prime ideals of \(A\), then the multiplicity of \(\mathfrak p\) in the factorization of \(\mathfrak q\) is zero.

theorem Ideal.count_normalizedFactors_eq_zero_iff
    {𝔭 I : Ideal A} (hp : 𝔭.IsPrime) (hI : I ≠ ⊥) :
    Multiset.count 𝔭 (UniqueFactorizationMonoid.normalizedFactors I) = 0 ↔
      ¬(I ≤ 𝔭)

Sources

• ATLAS NumberTheoryI Lemma 3.9.

TheoremFractional ideals have finite support#✓fully proved

Let \(A\) be a Dedekind domain with field of fractions \(K\), and let \(I\) be a fractional ideal of \(A\) in \(K\). For a nonzero prime ideal \(\mathfrak p\) of \(A\), let \(v_{\mathfrak p}(I) \in \mathbb Z\) be the exponent of \(\mathfrak p\) in the factorization of \(I\) into prime ideals, with \(v_{\mathfrak p}(0) = 0\). Then \(v_{\mathfrak p}(I) \neq 0\) for only finitely many nonzero prime ideals \(\mathfrak p\) of \(A\).

In particular, for \(x \in K^\times\) the valuations \(v_{\mathfrak p}(xA)\) vanish for all but finitely many \(\mathfrak p\).

theorem FractionalIdeal.count_eq_zero_for_all_but_finitely_many
    (I : FractionalIdeal A⁰ K) :
    {v : IsDedekindDomain.HeightOneSpectrum A |
      FractionalIdeal.count K v I ≠ 0}.Finite

Sources

• ATLAS NumberTheoryI Corollary 3.10. The book's hypothesis \(I \neq 0\) is dropped, since every valuation of the zero ideal is zero.

TheoremIdeal multiplicity is unchanged by localization at a maximal ideal#✓fully proved

Let \(R\) be a Dedekind domain, \(\mathfrak p\) a maximal ideal of \(R\), and \(R_{\mathfrak p}\) a local ring that is a localization of \(R\) at \(\mathfrak p\), with maximal ideal \(\mathfrak m\). Then for every ideal \(I\) of \(R\), the multiplicity of \(\mathfrak m\) in the extended ideal \(I R_{\mathfrak p}\) equals the multiplicity of \(\mathfrak p\) in \(I\). Here the multiplicity of an ideal \(J\) in an ideal \(K\) is the largest \(n\) with \(J^n \mid K\), or \(\infty\) if \(J^n \mid K\) for every \(n\).

theorem emultiplicity_maximalIdeal_map_eq
    {R Rₚ : Type*} [CommRing R] [IsDedekindDomain R]
    (p : Ideal R) [p.IsMaximal] [CommRing Rₚ] [Algebra R Rₚ]
    [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] (I : Ideal R) :
    emultiplicity (IsLocalRing.maximalIdeal Rₚ)
        (I.map (algebraMap R Rₚ)) =
      emultiplicity p I

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.