Dedekind domains #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the notion of a Dedekind domain (or Dedekind ring), as a Noetherian integrally closed commutative ring of Krull dimension at most one.

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.

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.

References #

Tags #

dedekind domain, dedekind ring

source

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

ring.dimension_le_one R = ∀ (p : ideal R), p ≠ ⊥ → p.is_prime → p.is_maximal

source

theorem ring.dimension_le_one.principal_ideal_ring (A : Type u_2) [comm_ring A] [is_domain A] [is_principal_ideal_ring A] :

ring.dimension_le_one A

source

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] [algebra R A] [algebra R B] [algebra B A] [is_scalar_tower R B A] [is_integral_closure B R A] (h : ring.dimension_le_one R) :

ring.dimension_le_one B

source

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] [algebra R A] (h : ring.dimension_le_one R) :

ring.dimension_le_one ↥(integral_closure R A)

source

theorem ring.dimension_le_one.not_lt_lt {R : Type u_1} [comm_ring R] (h : ring.dimension_le_one R) (p₀ p₁ p₂ : ideal R) [hp₁ : p₁.is_prime] [hp₂ : p₂.is_prime] :

¬(p₀ < p₁ ∧ p₁ < p₂)

source

theorem ring.dimension_le_one.eq_bot_of_lt {R : Type u_1} [comm_ring R] (h : ring.dimension_le_one R) (p P : ideal R) [hp : p.is_prime] [hP : P.is_prime] (hpP : p < P) :

p = ⊥

source

@[class]

structure is_dedekind_domain (A : Type u_2) [comm_ring A] [is_domain A] :

Prop

is_noetherian_ring : is_noetherian_ring A
dimension_le_one : ring.dimension_le_one A
is_integrally_closed : is_integrally_closed A

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 of this typeclass

source

theorem is_dedekind_domain_iff (A : Type u_2) [comm_ring A] [is_domain A] (K : Type u_1) [field K] [algebra A K] [is_fraction_ring A K] :

is_dedekind_domain A ↔ is_noetherian_ring A ∧ ring.dimension_le_one A ∧ ∀ {x : K}, is_integral A x → (∃ (y : A), ⇑(algebra_map 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.

source

@[protected, instance]

def is_principal_ideal_ring.is_dedekind_domain (A : Type u_2) [comm_ring A] [is_domain A] [is_principal_ideal_ring A] :

is_dedekind_domain A