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
• J.W.S. Cassels, A. Frölich, Algebraic Number Theory
• J. Neukirch, Algebraic Number Theory

Tags

dedekind domain, dedekind ring

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

theorem Ideal.IsPrime.isMaximal {R : Type u_4} [CommRing R] [Ring.DimensionLEOne R] {p : Ideal R} (h : p.IsPrime) (hp : p ≠ ⊥) : p.IsMaximal

instance Ring.DimensionLEOne.principal_ideal_ring (A : Type u_2) [CommRing A] [IsDomain A] [IsPrincipalIdealRing A] : Ring.DimensionLEOne A

Equations

• ⋯ = ⋯

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] [Ring.DimensionLEOne R] : Ring.DimensionLEOne B

instance Ring.DimensionLEOne.integralClosure (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Nontrivial R] [IsDomain A] [Algebra R A] [Ring.DimensionLEOne R] : Ring.DimensionLEOne ↥(integralClosure R A)

Equations

• ⋯ = ⋯

theorem Ring.DimensionLEOne.not_lt_lt {R : Type u_1} [CommRing R] [Ring.DimensionLEOne R] (p₀ p₁ p₂ : Ideal R) [hp₁ : p₁.IsPrime] [hp₂ : p₂.IsPrime] : ¬(p₀ < p₁ ∧ p₁ < p₂)

theorem Ring.DimensionLEOne.eq_bot_of_lt {R : Type u_1} [CommRing R] [Ring.DimensionLEOne R] (p P : Ideal R) [p.IsPrime] [P.IsPrime] (hpP : p < P) : p = ⊥

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

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.

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

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 b c : A}, a ≠ 0 → a * b = a * c → b = c
• mul_right_cancel_of_ne_zero : ∀ {a b c : A}, b ≠ 0 → a * b = c * b → a = c
• 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

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.

Equations

• ⋯ = ⋯

theorem isDedekindDomain_iff (A : Type u_2) [CommRing A] (K : Type u_4) [Field 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.

@[instance 100]

instance IsPrincipalIdealRing.isDedekindDomain (A : Type u_2) [CommRing A] [IsDomain A] [IsPrincipalIdealRing A] : IsDedekindDomain A

Equations

• ⋯ = ⋯