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 #

FractionalIdeal.count : 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.

Main results #

Ideal.finite_factors : Only finitely many maximal ideals of R divide a given nonzero ideal.
Ideal.finprod_heightOneSpectrum_factorization : The ideal I equals the finprod ∏_v v^(val_v(I)), where val_v(I) denotes the multiplicity of v in the factorization of I and v runs over the maximal ideals of R.
FractionalIdeal.finprod_heightOneSpectrum_factorization : 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)).
- FractionalIdeal.finprod_heightOneSpectrum_factorization' : If I is a nonzero fractional ideal, then I is equal to the product ∏_v v^(val_v(I)).
FractionalIdeal.finprod_heightOneSpectrum_factorization_principal : For a nonzero k = r/s ∈ K, the fractional ideal (k) is equal to the product ∏_v v^(val_v(r) - val_v(s)).
FractionalIdeal.finite_factors : If I ≠ 0, then val_v(I) = 0 for all but finitely many maximal ideals of R.
IsDedekindDomain.exists_sup_span_eq: For every ideals 0 < I ≤ J, there exists a such that J = I + ⟨a⟩.

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 #

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

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

Equations

v.maxPowDividing I = v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors

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

def FractionalIdeal.count {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) :

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.

theorem FractionalIdeal.count_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) :

count K v 0 = 0

val_v(0) = 0.

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

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 = spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * ↑J) :

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.

theorem FractionalIdeal.count_mul {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 I' : FractionalIdeal (nonZeroDivisors R) K} (hI : I ≠ 0) (hI' : I' ≠ 0) :

count K v (I * I') = count K v I + count K v I'

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

theorem FractionalIdeal.count_mul' {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 I' : FractionalIdeal (nonZeroDivisors R) K) [Decidable (I ≠ 0 ∧ I' ≠ 0)] :

count K v (I * I') = if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 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.

theorem FractionalIdeal.count_one {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) :

count K v 1 = 0

val_v(1) = 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 : ∀ i ∈ s, I i ≠ 0) :

count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)

theorem FractionalIdeal.count_pow {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 : ℕ) (I : FractionalIdeal (nonZeroDivisors R) K) :

count K v (I ^ n) = ↑n * count K v I

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

theorem FractionalIdeal.count_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) :

count K v ↑v.asIdeal = 1

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 : ℕ) :

count K v (↑v.asIdeal ^ n) = ↑n

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

theorem FractionalIdeal.count_neg_zpow {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 : ℤ) (I : FractionalIdeal (nonZeroDivisors R) K) :

count K v (I ^ (-n)) = -count K v (I ^ n)

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

theorem FractionalIdeal.count_inv {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) :

count K v I⁻¹ = -count K v I

theorem FractionalIdeal.count_zpow {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 : ℤ) (I : FractionalIdeal (nonZeroDivisors R) K) :

count K v (I ^ n) = n * count K v I

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 : ℤ) :

count K v (↑v.asIdeal ^ n) = n

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

theorem FractionalIdeal.count_maximal_coprime {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {w : IsDedekindDomain.HeightOneSpectrum R} (hw : w ≠ v) :

count K v ↑w.asIdeal = 0

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

theorem FractionalIdeal.count_maximal {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (v w : IsDedekindDomain.HeightOneSpectrum R) [Decidable (w = v)] :

count K v ↑w.asIdeal = if w = v then 1 else 0

theorem FractionalIdeal.count_finprod_coprime {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 → ℤ) :

count K v (∏ᶠ (w : IsDedekindDomain.HeightOneSpectrum R) (_ : w ≠ v), ↑w.asIdeal ^ exps w) = 0

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

theorem FractionalIdeal.count_finsuppProd {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 →₀ ℤ) :

count K v (exps.prod fun (x1 : IsDedekindDomain.HeightOneSpectrum R) (x2 : ℤ) => ↑x1.asIdeal ^ x2) = exps v

@[deprecated FractionalIdeal.count_finsuppProd (since := "2025-04-06")]

theorem FractionalIdeal.count_finsupp_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) (exps : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ) :

count K v (exps.prod fun (x1 : IsDedekindDomain.HeightOneSpectrum R) (x2 : ℤ) => ↑x1.asIdeal ^ x2) = exps v

Alias of FractionalIdeal.count_finsuppProd.

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

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

count K v ↑J = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)

theorem FractionalIdeal.count_coe_nonneg {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) :

0 ≤ count K v ↑J

theorem FractionalIdeal.count_mono {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 J : FractionalIdeal (nonZeroDivisors R) K} (hI : I ≠ 0) (h : I ≤ J) :

count K v J ≤ count K v I

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

∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ count K v I = I

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 = 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 , count K v I = 0

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

theorem IsDedekindDomain.exists_sup_span_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I J : Ideal R} (hIJ : I ≤ J) (hI : I ≠ 0) :

∃ (a : R), I ⊔ Ideal.span {a} = J

In a Dedekind domain, for every ideals 0 < I ≤ J there exists a such that J = I + ⟨a⟩. TODO: Show that this property uniquely characterizes dedekind domains.

theorem IsDedekindDomain.exists_eq_span_pair {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} {x : R} (hxI : x ∈ I) (hx : x ≠ 0) :

∃ (y : R), I = Ideal.span {x, y}

In a Dedekind domain, any ideal is spanned by two elements, where one of the element could be any fixed non-zero element in the ideal.

theorem IsDedekindDomain.exists_add_spanSingleton_mul_eq {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal (nonZeroDivisors R) K} (hac : a ≤ c) (ha : a ≠ 0) (hb : b ≠ 0) :

∃ (x : K), a + FractionalIdeal.spanSingleton (nonZeroDivisors R) x * b = c

noncomputable def FractionalIdeal.divMod {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (c b a : FractionalIdeal (nonZeroDivisors R) K) :

K

c.divMod b a (i.e. c / b mod a) is an arbitrary x such that c = bx + a. This is zero if the above is not possible, i.e. when a = 0 or b = 0 or ¬ a ≤ c.

Equations

c.divMod b a = if h : a ≤ c ∧ a ≠ 0 ∧ b ≠ 0 then ⋯.choose else 0

theorem FractionalIdeal.divMod_spec {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal (nonZeroDivisors R) K} (hac : a ≤ c) (ha : a ≠ 0) (hb : b ≠ 0) :

a + spanSingleton (nonZeroDivisors R) (c.divMod b a) * b = c

@[simp]

theorem FractionalIdeal.divMod_zero_left {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I J : FractionalIdeal (nonZeroDivisors R) K} :

I.divMod 0 J = 0

@[simp]

theorem FractionalIdeal.divMod_zero_right {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I J : FractionalIdeal (nonZeroDivisors R) K} :

I.divMod J 0 = 0

@[simp]

theorem FractionalIdeal.zero_divMod {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {I J : FractionalIdeal (nonZeroDivisors R) K} :

divMod 0 I J = 0

theorem FractionalIdeal.divMod_zero_of_not_le {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal (nonZeroDivisors R) K} (hac : ¬a ≤ c) :

c.divMod b a = 0

noncomputable def FractionalIdeal.quotientEquiv {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (I J I' J' : FractionalIdeal (nonZeroDivisors R) K) (H : I * J' = I' * J) (h : J ≤ I) (h' : J' ≤ I') (hJ' : J' ≠ 0) (hI : I ≠ 0) :

(↥↑I ⧸ Submodule.comap (↑I).subtype ↑J) ≃ₗ[R] ↥↑I' ⧸ Submodule.comap (↑I').subtype ↑J'

Let I J I' J' be nonzero fractional ideals in a dedekind domain with J ≤ I and J' ≤ I'. If I/J = I'/J' in the group of fractional ideals (i.e. I * J' = I' * J), then I/J ≃ I'/J' as quotient R-modules.

Equations

One or more equations did not get rendered due to their size.