Documentation

Mathlib.RingTheory.DedekindDomain.Basic

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 #

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 #

Tags #

dedekind domain, dedekind ring

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

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

  • maximalOfPrime : ∀ {p : Ideal R}, p p.IsPrimep.IsMaximal
Instances
    theorem Ring.DimensionLEOne.maximalOfPrime {R : Type u_1} [CommRing R] [self : Ring.DimensionLEOne R] {p : Ideal R} :
    p p.IsPrimep.IsMaximal
    theorem Ideal.IsPrime.isMaximal {R : Type u_4} [CommRing R] [Ring.DimensionLEOne R] {p : Ideal R} (h : p.IsPrime) (hp : p ) :
    p.IsMaximal
    theorem Ring.DimensionLEOne.not_lt_lt {R : Type u_1} [CommRing R] [Ring.DimensionLEOne R] (p₀ : Ideal R) (p₁ : Ideal R) (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 : Ideal R) (P : Ideal R) [p.IsPrime] [P.IsPrime] (hpP : p < P) :
    p =

    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.

      Instances
        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 , IsDedekindRing :

        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, is_dedekind_domain_dvr and is_dedekind_domain_inv. TODO: Prove that these are actually equivalent definitions.

          Instances

            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]
            Equations
            • =