mathlib3 documentation

ring_theory.dedekind_domain.factorization

Factorization of ideals of Dedekind domains #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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
noncomputable def is_dedekind_domain.height_one_spectrum.max_pow_dividing {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) (I : ideal R) :
ideal R

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

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

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

source
theorem associates.finite_factors {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] {I : ideal R} (hI : I ≠ 0) :
∀ᶠ (v : is_dedekind_domain.height_one_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_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] {I : ideal R} (hI : I ≠ 0) :
(function.mul_support (λ (v : is_dedekind_domain.height_one_spectrum R), v.max_pow_dividing 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.

source
theorem ideal.finite_mul_support_coe {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] {K : Type u_2} [field K] [algebra R K] [is_fraction_ring R K] {I : ideal R} (hI : I ≠ 0) :
(function.mul_support (λ (v : is_dedekind_domain.height_one_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_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] {K : Type u_2} [field K] [algebra R K] [is_fraction_ring R K] {I : ideal R} (hI : I ≠ 0) :
(function.mul_support (λ (v : is_dedekind_domain.height_one_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_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) (I : ideal R) (hI : I ≠ 0) :
¬v.as_ideal ^ ((associates.mk v.as_ideal).count (associates.mk I).factors + 1) ∣ finprod (λ (v : is_dedekind_domain.height_one_spectrum R), v.max_pow_dividing 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} [comm_ring R] [is_domain R] [is_dedekind_domain R] (I : ideal R) :
associates.mk (finprod (λ (v : is_dedekind_domain.height_one_spectrum R), v.max_pow_dividing I)) ≠ 0
source
theorem ideal.finprod_count {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) (I : ideal R) (hI : I ≠ 0) :
(associates.mk v.as_ideal).count (associates.mk (finprod (λ (v : is_dedekind_domain.height_one_spectrum R), v.max_pow_dividing I))).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.finprod_height_one_spectrum_factorization {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (I : ideal R) (hI : I ≠ 0) :
finprod (λ (v : is_dedekind_domain.height_one_spectrum R), v.max_pow_dividing I) = I

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

source
theorem ideal.finprod_height_one_spectrum_factorization_coe {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] {K : Type u_2} [field K] [algebra R K] [is_fraction_ring R K] (I : ideal R) (hI : I ≠ 0) :
finprod (λ (v : is_dedekind_domain.height_one_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.