# mathlibdocumentation

ring_theory.dedekind_domain

# Dedekind domains #

This file defines the notion of a Dedekind domain (or Dedekind ring), giving three equivalent definitions (TODO: and shows that they are equivalent).

## Main definitions #

• is_dedekind_domain defines a Dedekind domain as a commutative ring that is Noetherian, integrally closed in its field of fractions and has Krull dimension at most one. is_dedekind_domain_iff shows that this does not depend on the choice of field of fractions.
• is_dedekind_domain_dvr alternatively defines a Dedekind domain as an integral domain that is Noetherian, and the localization at every nonzero prime ideal is a DVR.
• is_dedekind_domain_inv alternatively defines a Dedekind domain as an integral domain where every nonzero fractional ideal is invertible.
• is_dedekind_domain_inv_iff shows that this does note depend on the choice of field of fractions.

## Implementation notes #

The definitions that involve a field of fractions choose a canonical field of fractions, but are independent of that choice. The ..._iff lemmas express this independence.

Often, definitions assume that Dedekind domains are not fields. We found it more practical to add a (h : ¬ is_field A) assumption whenever this is explicitly needed.

## Tags #

dedekind domain, dedekind ring

def ring.dimension_le_one (R : Type u_1) [comm_ring R] :
Prop

A ring R has Krull dimension at most one if all nonzero prime ideals are maximal.

Equations
theorem ring.dimension_le_one.is_integral_closure (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] (B : Type u_3) [comm_ring B] [is_domain B] [nontrivial R] [ A] [ B] [ A] [ A] [ A] (h : ring.dimension_le_one R) :
theorem ring.dimension_le_one.integral_closure (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [nontrivial R] [is_domain A] [ A] (h : ring.dimension_le_one R) :
@[class]
structure is_dedekind_domain (A : Type u_2) [comm_ring A] [is_domain A] :
Prop
• is_noetherian_ring :
• dimension_le_one :
• is_integrally_closed :

A Dedekind domain is an integral domain that is Noetherian, integrally closed, and has Krull dimension at most one.

This is definition 3.2 of [Neu99].

The integral closure condition is independent of the choice of field of fractions: use is_dedekind_domain_iff to prove is_dedekind_domain for a given fraction_map.

This is the default implementation, but there are equivalent definitions, is_dedekind_domain_dvr and is_dedekind_domain_inv. TODO: Prove that these are actually equivalent definitions.

Instances
theorem is_dedekind_domain_iff (A : Type u_2) [comm_ring A] [is_domain A] (K : Type u_1) [field K] [ K] [ K] :
∀ {x : K}, x(∃ (y : A), K) y = x)

An integral domain is a Dedekind domain iff and only if it is Noetherian, has dimension ≤ 1, and is integrally closed in a given fraction field. In particular, this definition does not depend on the choice of this fraction field.

@[protected, instance]
structure is_dedekind_domain_dvr (A : Type u_2) [comm_ring A] [is_domain A] :
Prop
• is_noetherian_ring :
• is_dvr_at_nonzero_prime : ∀ (P : ideal A), P ∀ (ᾰ : P.is_prime),

A Dedekind domain is an integral domain that is Noetherian, and the localization at every nonzero prime is a discrete valuation ring.

This is equivalent to is_dedekind_domain. TODO: prove the equivalence.

@[protected, instance]
noncomputable def fractional_ideal.has_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] :
Equations
• = {inv := λ (I : K), 1 / I}
theorem fractional_ideal.inv_eq (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {I : K} :
I⁻¹ = 1 / I
theorem fractional_ideal.inv_zero' (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] :
0⁻¹ = 0
theorem fractional_ideal.inv_nonzero (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {J : K} (h : J 0) :
J⁻¹ = 1 / J, _⟩
theorem fractional_ideal.coe_inv_of_nonzero (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {J : K} (h : J 0) :
theorem fractional_ideal.mem_inv_iff {K : Type u_3} [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {I : K} (hI : I 0) {x : K} :
x I⁻¹ ∀ (y : K), y Ix * y 1
theorem fractional_ideal.inv_anti_mono {K : Type u_3} [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {I J : K} (hI : I 0) (hJ : J 0) (hIJ : I J) :
theorem fractional_ideal.le_self_mul_inv {K : Type u_3} [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {I : K} (hI : I 1) :
I I * I⁻¹
theorem fractional_ideal.coe_ideal_le_self_mul_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] (I : ideal R₁) :
theorem fractional_ideal.right_inverse_eq (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] (I J : K) (h : I * J = 1) :
J = I⁻¹

I⁻¹ is the inverse of I if I has an inverse.

theorem fractional_ideal.mul_inv_cancel_iff (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {I : K} :
I * I⁻¹ = 1 ∃ (J : K), I * J = 1
theorem fractional_ideal.mul_inv_cancel_iff_is_unit (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {I : K} :
I * I⁻¹ = 1
@[simp]
theorem fractional_ideal.map_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] {K' : Type u_5} [field K'] [algebra R₁ K'] [ K'] (I : K) (h : K ≃ₐ[R₁] K') :
@[simp]
theorem fractional_ideal.span_singleton_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] (x : K) :
theorem fractional_ideal.mul_generator_self_inv (K : Type u_3) [field K] {R₁ : Type u_1} [comm_ring R₁] [algebra R₁ K] [ K] (I : K) [I.is_principal] (h : I 0) :
theorem fractional_ideal.invertible_of_principal (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] (I : K) [I.is_principal] (h : I 0) :
I * I⁻¹ = 1
theorem fractional_ideal.invertible_iff_generator_nonzero (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] (I : K) [I.is_principal] :
I * I⁻¹ = 1
theorem fractional_ideal.is_principal_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] (I : K) [I.is_principal] (h : I 0) :
@[simp]
theorem fractional_ideal.one_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [ K] :
1⁻¹ = 1
def is_dedekind_domain_inv (A : Type u_2) [comm_ring A] [is_domain A] :
Prop

A Dedekind domain is an integral domain such that every fractional ideal has an inverse.

This is equivalent to is_dedekind_domain. In particular we provide a fractional_ideal.comm_group_with_zero instance, assuming is_dedekind_domain A, which implies is_dedekind_domain_inv. For integral ideals, is_dedekind_domain(_inv) implies only ideal.comm_cancel_monoid_with_zero.

Equations
theorem is_dedekind_domain_inv_iff {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] :
∀ (I : , I I * I⁻¹ = 1
theorem fractional_ideal.adjoin_integral_eq_one_of_is_unit {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] (x : K) (hx : x) (hI : is_unit ) :
theorem is_dedekind_domain_inv.mul_inv_eq_one {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] (h : is_dedekind_domain_inv A) {I : K} (hI : I 0) :
I * I⁻¹ = 1
theorem is_dedekind_domain_inv.inv_mul_eq_one {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] (h : is_dedekind_domain_inv A) {I : K} (hI : I 0) :
I⁻¹ * I = 1
@[protected]
theorem is_dedekind_domain_inv.is_unit {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] (h : is_dedekind_domain_inv A) {I : K} (hI : I 0) :

Showing one side of the equivalence between the definitions is_dedekind_domain_inv and is_dedekind_domain of Dedekind domains.

theorem exists_multiset_prod_cons_le_and_prod_not_le {A : Type u_2} [comm_ring A] [is_domain A] (hNF : ¬) {I M : ideal A} (hI0 : I ) (hIM : I M) [hM : M.is_maximal] :
∃ (Z : ,

Specialization of exists_prime_spectrum_prod_le_and_ne_bot_of_domain to Dedekind domains: Let I : ideal A be a nonzero ideal, where A is a Dedekind domain that is not a field. Then exists_prime_spectrum_prod_le_and_ne_bot_of_domain states we can find a product of prime ideals that is contained within I. This lemma extends that result by making the product minimal: let M be a maximal ideal that contains I, then the product including M is contained within I and the product excluding M is not contained within I.

theorem fractional_ideal.exists_not_mem_one_of_ne_bot {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] (hNF : ¬) {I : ideal A} (hI0 : I ) (hI1 : I ) :
∃ (x : K), x (I)⁻¹ x 1
theorem fractional_ideal.one_mem_inv_coe_ideal {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {I : ideal A} (hI : I ) :
theorem fractional_ideal.mul_inv_cancel_of_le_one {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] [h : is_dedekind_domain A] {I : ideal A} (hI0 : I ) (hI : ((I) * (I)⁻¹)⁻¹ 1) :
(I) * (I)⁻¹ = 1
theorem fractional_ideal.coe_ideal_mul_inv {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] [h : is_dedekind_domain A] (I : ideal A) (hI0 : I ) :
(I) * (I)⁻¹ = 1

Nonzero integral ideals in a Dedekind domain are invertible.

We will use this to show that nonzero fractional ideals are invertible, and finally conclude that fractional ideals in a Dedekind domain form a group with zero.

@[protected]
theorem fractional_ideal.mul_inv_cancel {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {I : K} (hne : I 0) :
I * I⁻¹ = 1

Nonzero fractional ideals in a Dedekind domain are units.

This is also available as _root_.mul_inv_cancel, using the comm_group_with_zero instance defined below.

theorem fractional_ideal.mul_right_le_iff {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {J : K} (hJ : J 0) {I I' : K} :
I * J I' * J I I'
theorem fractional_ideal.mul_left_le_iff {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {J : K} (hJ : J 0) {I I' : K} :
J * I J * I' I I'
theorem fractional_ideal.mul_right_strict_mono {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {I : K} (hI : I 0) :
strict_mono (λ (_x : fractional_ideal A K), _x * I)
theorem fractional_ideal.mul_left_strict_mono {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {I : K} (hI : I 0) :
@[protected]
theorem fractional_ideal.div_eq_mul_inv {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] (I J : K) :
I / J = I * J⁻¹

This is also available as _root_.div_eq_mul_inv, using the comm_group_with_zero instance defined below.

is_dedekind_domain and is_dedekind_domain_inv are equivalent ways to express that an integral domain is a Dedekind domain.

@[protected, instance]
noncomputable def fractional_ideal.comm_group_with_zero {A : Type u_2} (K : Type u_3) [comm_ring A] [field K] [is_domain A] [ K] [ K] :
Equations
@[protected, instance]
noncomputable def ideal.comm_cancel_monoid_with_zero {A : Type u_2} [comm_ring A] [is_domain A]  :
Equations
• ideal.comm_cancel_monoid_with_zero = ideal.comm_cancel_monoid_with_zero._proof_2 ideal.comm_cancel_monoid_with_zero._proof_3 ideal.comm_cancel_monoid_with_zero._proof_4 ideal.comm_cancel_monoid_with_zero._proof_5
theorem ideal.dvd_iff_le {A : Type u_2} [comm_ring A] [is_domain A] {I J : ideal A} :
I J J I

For ideals in a Dedekind domain, to divide is to contain.

theorem ideal.dvd_not_unit_iff_lt {A : Type u_2} [comm_ring A] [is_domain A] {I J : ideal A} :
J J < I
@[protected, instance]
def ideal.wf_dvd_monoid {A : Type u_2} [comm_ring A] [is_domain A]  :
@[protected, instance]
def ideal.unique_factorization_monoid {A : Type u_2} [comm_ring A] [is_domain A]  :
@[protected, instance]
noncomputable def ideal.normalization_monoid {A : Type u_2} [comm_ring A] [is_domain A]  :
Equations
@[simp]
theorem ideal.dvd_span_singleton {A : Type u_2} [comm_ring A] [is_domain A] {I : ideal A} {x : A} :
I ideal.span {x} x I
theorem ideal.is_prime_of_prime {A : Type u_2} [comm_ring A] [is_domain A] {P : ideal A} (h : prime P) :
theorem ideal.prime_of_is_prime {A : Type u_2} [comm_ring A] [is_domain A] {P : ideal A} (hP : P ) (h : P.is_prime) :
theorem ideal.prime_iff_is_prime {A : Type u_2} [comm_ring A] [is_domain A] {P : ideal A} (hP : P ) :

In a Dedekind domain, the (nonzero) prime elements of the monoid with zero ideal A are exactly the prime ideals.

### is_integral_closure section #

We show that an integral closure of a Dedekind domain in a finite separable field extension is again a Dedekind domain. This implies the ring of integers of a number field is a Dedekind domain.

theorem is_integral_closure.range_le_span_dual_basis {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {L : Type u_4} [field L] (C : Type u_5) [comm_ring C] [ L] [ L] [ L] [ L] [ L] [ L] [ C] [ L] [ L] {ι : Type u_1} [fintype ι] [decidable_eq ι] (b : K L) (hb_int : ∀ (i : ι), (b i))  :
theorem integral_closure_le_span_dual_basis {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {L : Type u_4} [field L] [ L] [ L] [ L] [ L] [ L] {ι : Type u_1} [fintype ι] [decidable_eq ι] (b : K L) (hb_int : ∀ (i : ι), (b i))  :
theorem exists_integral_multiples (A : Type u_2) (K : Type u_3) [comm_ring A] [field K] [is_domain A] [ K] [ K] {L : Type u_4} [field L] [ L] [ L] [ L] [ L] (s : finset L) :
∃ (y : A) (H : y 0), ∀ (x : L), x s (y x)

Send a set of x'es in a finite extension L of the fraction field of R to (y : R) • x ∈ integral_closure R L.

theorem finite_dimensional.exists_is_basis_integral (A : Type u_2) (K : Type u_3) [comm_ring A] [field K] [is_domain A] [ K] [ K] (L : Type u_4) [field L] [ L] [ L] [ L] [ L] :
∃ (s : finset L) (b : K L), ∀ (x : s), (b x)

If L is a finite extension of K = Frac(A), then L has a basis over A consisting of integral elements.

theorem is_integral_closure.is_noetherian_ring (A : Type u_2) (K : Type u_3) [comm_ring A] [field K] [is_domain A] [ K] [ K] (L : Type u_4) [field L] (C : Type u_5) [comm_ring C] [ L] [ L] [ L] [ L] [ L] [ L] [ C] [ L] [ L]  :
theorem integral_closure.is_noetherian_ring {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] (L : Type u_4) [field L] [ L] [ L] [ L] [ L] [ L]  :
theorem is_integral_closure.is_dedekind_domain (A : Type u_2) (K : Type u_3) [comm_ring A] [field K] [is_domain A] [ K] [ K] (L : Type u_4) [field L] (C : Type u_5) [comm_ring C] [ L] [ L] [ L] [ L] [ L] [ L] [ C] [ L] [ L] [is_domain C] [h : is_dedekind_domain A] :
theorem integral_closure.is_dedekind_domain (A : Type u_2) (K : Type u_3) [comm_ring A] [field K] [is_domain A] [ K] [ K] (L : Type u_4) [field L] [ L] [ L] [ L] [ L] [ L] [h : is_dedekind_domain A] :
@[protected, instance]
def integral_closure.is_dedekind_domain_fraction_ring (A : Type u_2) [comm_ring A] [is_domain A] (L : Type u_4) [field L] [ L] [ L] [ L] [ L] [ L]  :
theorem prod_normalized_factors_eq_self {T : Type u_4} [comm_ring T] [is_domain T] {I : ideal T} (hI : I ) :
theorem normalized_factors_prod {T : Type u_4} [comm_ring T] [is_domain T] {α : multiset (ideal T)} (h : ∀ (p : ideal T), p α) :
theorem count_le_of_ideal_ge {T : Type u_4} [comm_ring T] [is_domain T] {I J : ideal T} (h : I J) (hI : I ) (K : ideal T) :
theorem sup_eq_prod_inf_factors {T : Type u_4} [comm_ring T] [is_domain T] (I J : ideal T) (hI : I ) (hJ : J ) :