mathlib documentation

ideles / fractional_ideal

Factorization of fractional ideals of Dedekind domains #

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 fractional_ideal.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 nonzero fractional ideals, we chose to define val_v(I) = 0 so that every val_v is in ℤ and we can avoid having to use with_top ℤ.

Tags #

dedekind domain, fractional ideal, factorization

Factorization of fractional ideals of Dedekind domains #

source
theorem prime.exists_mem_finprod_dvd {α : Type u_1} {N : Type u_2} [comm_monoid_with_zero N] {f : α → N} {p : N} (hp : prime p) (hf : (function.mul_support f).finite) :
p ∣ ∏ᶠ (i : α), f i → (∃ (a : α), p ∣ f a)

If a prime p divides a finprod, then it must divide one of its factors.

source
@[protected, instance]
def ufi_ts {R : Type u_3} {K : Type u_4} [comm_ring R] [field K] [algebra R K] :
topological_space (fractional_ideal R⁰ K)ˣ

The discrete topology on the units of the fractional ideals.

Equations
source
@[protected, instance]
def ufi_tg {R : Type u_3} {K : Type u_4} [comm_ring R] [field K] [algebra R K] :
topological_group (fractional_ideal R⁰ K)ˣ

The units of the fractional ideals with the discrete topology are a topological group.

source
@[protected, instance]
def ufi_us {R : Type u_3} {K : Type u_4} [comm_ring R] [field K] [algebra R K] :
uniform_space (fractional_ideal R⁰ K)ˣ
Equations
source
@[protected, instance]
def ufi_ug {R : Type u_3} {K : Type u_4} [comm_ring R] [field K] [algebra R K] :
uniform_group (fractional_ideal R⁰ K)ˣ
source
theorem fractional_ideal.ideal_factor_ne_zero {R : Type u_3} {K : Type u_4} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] {I : fractional_ideal R⁰ K} (hI : I ≠ 0) {a : R} {J : ideal R} (haJ : I = (fractional_ideal.span_singleton R⁰ (⇑(algebra_map R K) a)⁻¹) * ↑J) :
J ≠ 0

If I is a nonzero fractional ideal, a ∈ R, and J is an ideal of R such that I = a⁻¹J, then J is nonzero.

source
theorem fractional_ideal.constant_factor_ne_zero {R : Type u_3} {K : Type u_4} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] {I : fractional_ideal R⁰ K} (hI : I ≠ 0) {a : R} {J : ideal R} (haJ : I = (fractional_ideal.span_singleton R⁰ (⇑(algebra_map R K) a)⁻¹) * ↑J) :
ideal.span {a} ≠ 0

If I is a nonzero fractional ideal, a ∈ R, and J is an ideal of R such that I = a⁻¹J, then a is nonzero.

source
theorem ideal.finite_factors {R : Type u_3} [comm_ring R] [is_domain R] [is_dedekind_domain R] {I : ideal R} (hI : I ≠ 0) :
{v : maximal_spectrum R | v.as_ideal ∣ I}.finite

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

source
theorem finite_factors {R : Type u_3} [comm_ring R] [is_domain R] [is_dedekind_domain R] (d : R) (hd : ideal.span {d} ≠ 0) :
{v : maximal_spectrum R | v.as_ideal ∣ ideal.span {d}}.finite

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

source
theorem associates.finite_factors {R : Type u_3} [comm_ring R] [is_domain R] [is_dedekind_domain R] (I : ideal R) (hI : I ≠ 0) :
∀ᶠ (v : maximal_spectrum R) in filter.cofinite, ↑((associates.mk v.as_ideal).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.

source
theorem ideal.finite_mul_support {R : Type u_3} [comm_ring R] [is_domain R] [is_dedekind_domain R] {I : ideal R} (hI : I ≠ 0) :
(function.mul_support (λ (v : maximal_spectrum R), v.as_ideal ^ (associates.mk v.as_ideal).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.

source
theorem ideal.finite_mul_support_coe {R : Type u_3} {K : Type u_4} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] {I : ideal R} (hI : I ≠ 0) :
(function.mul_support (λ (v : maximal_spectrum R), ↑(v.as_ideal) ^ ↑((associates.mk v.as_ideal).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).

source
theorem ideal.finite_mul_support_inv {R : Type u_3} {K : Type u_4} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] {I : ideal R} (hI : I ≠ 0) :
(function.mul_support (λ (v : maximal_spectrum R), ↑(v.as_ideal) ^ -↑((associates.mk v.as_ideal).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.

source
theorem ideal.finprod_not_dvd {R : Type u_3} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) (I : ideal R) (hI : I ≠ 0) :
¬v.as_ideal ^ ((associates.mk v.as_ideal).count (associates.mk I).factors + 1) ∣ ∏ᶠ (v : maximal_spectrum R), v.as_ideal ^ (associates.mk v.as_ideal).count (associates.mk I).factors

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_3} [comm_ring R] [is_domain R] [is_dedekind_domain R] (I : ideal R) :
associates.mk (∏ᶠ (v : maximal_spectrum R), v.as_ideal ^ (associates.mk v.as_ideal).count (associates.mk I).factors) ≠ 0
source
theorem ideal.finprod_count {R : Type u_3} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) (I : ideal R) (hI : I ≠ 0) :
(associates.mk v.as_ideal).count (associates.mk (∏ᶠ (v : maximal_spectrum R), v.as_ideal ^ (associates.mk v.as_ideal).count (associates.mk I).factors)).factors = (associates.mk v.as_ideal).count (associates.mk I).factors

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

source
theorem ideal.factorization {R : Type u_3} [comm_ring R] [is_domain R] [is_dedekind_domain R] (I : ideal R) (hI : I ≠ 0) :
∏ᶠ (v : maximal_spectrum R), v.as_ideal ^ (associates.mk v.as_ideal).count (associates.mk I).factors = I

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

source
theorem ideal.factorization_coe {R : Type u_3} {K : Type u_4} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (I : ideal R) (hI : I ≠ 0) :
∏ᶠ (v : maximal_spectrum R), ↑(v.as_ideal) ^ ↑((associates.mk v.as_ideal).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.

source
theorem fractional_ideal.factorization {R : Type u_3} {K : Type u_4} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (I : fractional_ideal R⁰ K) (hI : I ≠ 0) {a : R} {J : ideal R} (haJ : I = (fractional_ideal.span_singleton R⁰ (⇑(algebra_map R K) a)⁻¹) * ↑J) :
∏ᶠ (v : maximal_spectrum R), ↑(v.as_ideal) ^ (↑((associates.mk v.as_ideal).count (associates.mk J).factors) - ↑((associates.mk v.as_ideal).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)).

source
theorem fractional_ideal.factorization_principal {R : Type u_3} {K : Type u_4} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (I : fractional_ideal R⁰ K) (hI : I ≠ 0) (k : K) (hk : I = fractional_ideal.span_singleton R⁰ k) :
∏ᶠ (v : maximal_spectrum R), ↑(v.as_ideal) ^ (↑((associates.mk v.as_ideal).count (associates.mk (ideal.span {classical.some _})).factors) - ↑((associates.mk v.as_ideal).count (associates.mk (ideal.span {↑(classical.some _)})).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)).

source
noncomputable def fractional_ideal.count {R : Type u_3} (K : Type u_4) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) (I : fractional_ideal R⁰ K) :
ℤ

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
source
theorem fractional_ideal.count_well_defined {R : Type u_3} (K : Type u_4) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) {I : fractional_ideal R⁰ K} (hI : I ≠ 0) {a : R} {J : ideal R} (h_aJ : I = (fractional_ideal.span_singleton R⁰ (⇑(algebra_map R K) a)⁻¹) * ↑J) :
fractional_ideal.count K v I = ↑((associates.mk v.as_ideal).count (associates.mk J).factors) - ↑((associates.mk v.as_ideal).count (associates.mk (ideal.span {a})).factors)

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

source
theorem fractional_ideal.count_mul {R : Type u_3} (K : Type u_4) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) {I I' : fractional_ideal R⁰ K} (hI : I ≠ 0) (hI' : I' ≠ 0) :
fractional_ideal.count K v (I * I') = fractional_ideal.count K v I + fractional_ideal.count K v I'

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

source
theorem fractional_ideal.count_mul' {R : Type u_3} (K : Type u_4) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) (I I' : fractional_ideal R⁰ K) :
fractional_ideal.count K v (I * I') = ite (I ≠ 0 ∧ I' ≠ 0) (fractional_ideal.count K v I + fractional_ideal.count K v I') 0

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.

source
theorem fractional_ideal.count_zero {R : Type u_3} (K : Type u_4) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) :
fractional_ideal.count K v 0 = 0

val_v(0) = 0.

source
theorem fractional_ideal.count_one {R : Type u_3} (K : Type u_4) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) :
fractional_ideal.count K v 1 = 0

val_v(1) = 0.

source
theorem fractional_ideal.count_pow {R : Type u_3} (K : Type u_4) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) (n : ℕ) (I : fractional_ideal R⁰ K) :
fractional_ideal.count K v (I ^ n) = (↑n) * fractional_ideal.count K v I

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

source
theorem fractional_ideal.count_self {R : Type u_3} (K : Type u_4) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) :
fractional_ideal.count K v ↑(v.as_ideal) = 1

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

source
theorem fractional_ideal.count_pow_self {R : Type u_3} (K : Type u_4) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) (n : ℕ) :
fractional_ideal.count K v (↑(v.as_ideal) ^ n) = ↑n

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

source
theorem fractional_ideal.count_inv {R : Type u_3} (K : Type u_4) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) (n : ℤ) (I : fractional_ideal R⁰ K) :
fractional_ideal.count K v (I ^ -n) = -fractional_ideal.count K v (I ^ n)

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

source
theorem fractional_ideal.count_zpow {R : Type u_3} (K : Type u_4) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) (n : ℤ) (I : fractional_ideal R⁰ K) :
fractional_ideal.count K v (I ^ n) = n * fractional_ideal.count K v I

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

source
theorem fractional_ideal.count_zpow_self {R : Type u_3} (K : Type u_4) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) (n : ℤ) :
fractional_ideal.count K v (↑(v.as_ideal) ^ n) = n

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

source
theorem fractional_ideal.count_maximal_coprime {R : Type u_3} (K : Type u_4) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (v w : maximal_spectrum R) (hw : w ≠ v) :
fractional_ideal.count K v ↑(w.as_ideal) = 0

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

source
theorem fractional_ideal.count_finprod_coprime {R : Type u_3} (K : Type u_4) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) (exps : maximal_spectrum R → ℤ) :
fractional_ideal.count K v (∏ᶠ (w : maximal_spectrum R) (H : w ≠ v), ↑(w.as_ideal) ^ exps w) = 0

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

source
theorem fractional_ideal.count_finprod {R : Type u_3} (K : Type u_4) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (v : maximal_spectrum R) (exps : maximal_spectrum R → ℤ) (h_exps : ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, exps v = 0) :
fractional_ideal.count K v (∏ᶠ (v : maximal_spectrum R), ↑(v.as_ideal) ^ exps v) = exps v

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

source
theorem fractional_ideal.finite_factors {R : Type u_3} {K : Type u_4} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] {I : fractional_ideal R⁰ K} (hI : I ≠ 0) {a : R} {J : ideal R} (haJ : I = (fractional_ideal.span_singleton R⁰ (⇑(algebra_map R K) a)⁻¹) * ↑J) :
∀ᶠ (v : maximal_spectrum R) in filter.cofinite, ↑((associates.mk v.as_ideal).count (associates.mk J).factors) - ↑((associates.mk v.as_ideal).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.