# Dedekind rings and domains #

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

## Main definitions #

- `IsDedekindRing` defines a Dedekind ring as a commutative ring that is Noetherian, integrally closed in its field of fractions and has Krull dimension at most one. `isDedekindRing_iff` shows that this does not depend on the choice of field of fractions.
- `IsDedekindDomain` defines a Dedekind domain as a Dedekind ring that is a domain.

## 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.

`IsDedekindRing` and `IsDedekindDomain` form a cycle in the typeclass hierarchy: `IsDedekindRing R + IsDomain R` imply `IsDedekindDomain R`, which implies `IsDedekindRing R`. This should be safe since the start and end point is the literal same expression, which the tabled typeclass synthesis algorithm can deal with.

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

## References #

- [D. Marcus, Number Fields][marcus1977number]
- [J.W.S. Cassels, A. Fröhlich, Algebraic Number Theory][cassels1967algebraic]
- [J. Neukirch, Algebraic Number Theory][Neukirch1992]

## Tags #

dedekind domain, dedekind ring

source
class Ring.DimensionLEOne (R : Type u_1) [CommRing R] :
Prop

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

- maximalOfPrime {p : Ideal R} : p ≠ ⊥ → p.IsPrime → p.IsMaximal

Instances

source
theorem Ideal.IsPrime.isMaximal {R : Type u_4} [CommRing R] [Ring.DimensionLEOne R] {p : Ideal R} (h : p.IsPrime) (hp : p ≠ ⊥) :
p.IsMaximal
source
instance Ring.DimensionLEOne.principal_ideal_ring (A : Type u_2) [CommRing A] [IsDomain A] [IsPrincipalIdealRing A] :
DimensionLEOne A
source
theorem Ring.DimensionLEOne.isIntegralClosure (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] (B : Type u_4) [CommRing B] [IsDomain B] [Nontrivial R] [Algebra R A] [Algebra R B] [Algebra B A] [IsScalarTower R B A] [IsIntegralClosure B R A] [DimensionLEOne R] :
DimensionLEOne B
source
instance Ring.DimensionLEOne.integralClosure (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Nontrivial R] [IsDomain A] [Algebra R A] [DimensionLEOne R] :
DimensionLEOne ↥(_root_.integralClosure R A)
source
theorem Ring.DimensionLEOne.not_lt_lt {R : Type u_1} [CommRing R] [DimensionLEOne R] (p₀ p₁ p₂ : Ideal R) [hp₁ : p₁.IsPrime] [hp₂ : p₂.IsPrime] :
¬(p₀ < p₁ ∧ p₁ < p₂)
source
theorem Ring.DimensionLEOne.eq_bot_of_lt {R : Type u_1} [CommRing R] [DimensionLEOne R] (p P : Ideal R) [p.IsPrime] [P.IsPrime] (hpP : p < P) :
p = ⊥
source
class IsDedekindRing (A : Type u_2) [CommRing A] extends IsNoetherian A A, Ring.DimensionLEOne A, IsIntegralClosure A A (FractionRing A) :
Prop

A Dedekind ring is a commutative ring that is Noetherian, integrally closed, and has Krull dimension at most one.

This is exactly `IsDedekindDomain` minus the `IsDomain` hypothesis.

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

- noetherian (s : Submodule A A) : s.FG
- maximalOfPrime {p : Ideal A} : p ≠ ⊥ → p.IsPrime → p.IsMaximal
- algebraMap_injective : Function.Injective ⇑(algebraMap A (FractionRing A))
- isIntegral_iff {x : FractionRing A} : IsIntegral A x ↔ ∃ (y : A), (algebraMap A (FractionRing A)) y = x

Instances

source
theorem isDedekindRing_iff (A : Type u_2) [CommRing A] (K : Type u_4) [CommRing K] [Algebra A K] [IsFractionRing A K] :
IsDedekindRing A ↔ IsNoetherianRing A ∧ Ring.DimensionLEOne A ∧ ∀ {x : K}, IsIntegral A x → ∃ (y : A), (algebraMap A K) y = x

An integral domain is a Dedekind domain if 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
class IsDedekindDomain (A : Type u_2) [CommRing A] extends IsDomain A, IsDedekindRing A :
Prop

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 [Neukirch1992].

This is exactly `IsDedekindRing` plus the `IsDomain` hypothesis.

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

This is the default implementation, but there are equivalent definitions, `IsDedekindDomainDvr` and `IsDedekindDomainInv`.

- mul_left_cancel_of_ne_zero {a : A} : a ≠ 0 → IsLeftRegular a
- mul_right_cancel_of_ne_zero {a : A} : a ≠ 0 → IsRightRegular a
- exists_pair_ne : ∃ (x : A) (y : A), x ≠ y
- noetherian (s : Submodule A A) : s.FG
- maximalOfPrime {p : Ideal A} : p ≠ ⊥ → p.IsPrime → p.IsMaximal
- algebraMap_injective : Function.Injective ⇑(algebraMap A (FractionRing A))
- isIntegral_iff {x : FractionRing A} : IsIntegral A x ↔ ∃ (y : A), (algebraMap A (FractionRing A)) y = x

Instances

source
instance instIsDedekindDomainOfIsDomainOfIsDedekindRing (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindRing A] :
IsDedekindDomain A

Make a Dedekind domain from a Dedekind ring given that it is a domain.

`IsDedekindRing` and `IsDedekindDomain` form a cycle in the typeclass hierarchy: `IsDedekindRing R + IsDomain R` imply `IsDedekindDomain R`, which implies `IsDedekindRing R`. This should be safe since the start and end point is the literal same expression, which the tabled typeclass synthesis algorithm can deal with.

source
theorem isDedekindDomain_iff (A : Type u_2) [CommRing A] (K : Type u_4) [CommRing K] [Algebra A K] [IsFractionRing A K] :
IsDedekindDomain A ↔ IsDomain A ∧ IsNoetherianRing A ∧ Ring.DimensionLEOne A ∧ ∀ {x : K}, IsIntegral A x → ∃ (y : A), (algebraMap 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
@[instance 100]
instance IsPrincipalIdealRing.isDedekindDomain (A : Type u_2) [CommRing A] [IsDomain A] [IsPrincipalIdealRing A] :
IsDedekindDomain A
source
theorem IsLocalRing.primesOver_eq {R : Type u_1} (A : Type u_2) [CommRing R] [CommRing A] [IsLocalRing A] [IsDedekindDomain A] [Algebra R A] [FaithfulSMul R A] [Module.Finite R A] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) :
p.primesOver A = {maximalIdeal A}