Characterizations of Dedekind domains

TheoremDedekind domains as the Noetherian domains where to contain is to divide#✓fully proved

An integral domain \(A\) is a Dedekind domain if and only if \(A\) is Noetherian and, for all ideals \(I\) and \(J\) of \(A\), \(I\) divides \(J\) if and only if \(J \subseteq I\).

theorem isDedekindDomain_iff_contain_isDivide :
    IsDedekindDomain A ↔
      IsNoetherianRing A ∧ ∀ I J : Ideal A, I ∣ J ↔ J ≤ I
Sources
  • ATLAS NumberTheoryI Theorem 3.23, conditions (1) and (5).
Used by 1
Used byEquivalent characterizations of Dedekind domains

TheoremDedekind domains via principal products#✓fully proved

An integral domain \(A\) is a Dedekind domain if and only if for every nonzero ideal \(I\) of \(A\) there is an ideal \(J\) of \(A\) such that \(IJ\) is a nonzero principal ideal.

theorem isDedekindDomain_iff_principalProduct :
    IsDedekindDomain A ↔
      ∀ I : Ideal A, I ≠ ⊥ →
        ∃ J : Ideal A, (I * J).IsPrincipal ∧ I * J ≠ ⊥
Sources
  • ATLAS NumberTheoryI Theorem 3.23(6), corrected: the recorded condition omits both nonzero qualifiers, which makes it vacuous (take \(J = 0\)).
Used by 1
Used byEquivalent characterizations of Dedekind domains

TheoremEquivalent characterizations of Dedekind domains#✓fully proved

For an integral domain \(A\), the following are equivalent: (1) \(A\) is a Dedekind domain; (2) \(A\) is Noetherian and, for all ideals \(I\) and \(J\) of \(A\), \(I\) divides \(J\) if and only if \(J \subseteq I\); (3) for every nonzero ideal \(I\) of \(A\) there is an ideal \(J\) of \(A\) such that \(IJ\) is a nonzero principal ideal.

theorem isDedekindDomain_tfae_contain_isDivide_principalProduct :
    List.TFAE
      [IsDedekindDomain A,
       IsNoetherianRing A ∧ ∀ I J : Ideal A, I ∣ J ↔ J ≤ I,
       ∀ I : Ideal A, I ≠ ⊥ →
         ∃ J : Ideal A, (I * J).IsPrincipal ∧ I * J ≠ ⊥]
Sources
  • ATLAS NumberTheoryI Theorem 3.23, conditions (1), (5) and (6), with (6) corrected by the two nonzero qualifiers.
Uses 2
Proof usesDedekind domains as the Noetherian domains where to contain is to divide · Dedekind domains via principal products

TheoremDedekind domains are the integrally closed Noetherian domains of dimension at most one#✓fully proved

Let \(A\) be a Noetherian integral domain. Then \(A\) is integrally closed and has Krull dimension at most one if and only if \(A\) is a Dedekind domain.

theorem integrallyClosed_dimensionLEOne_iff_isDedekindDomain
    (A : Type*) [CommRing A] [IsDomain A] [IsNoetherianRing A] :
    (IsIntegrallyClosed A ∧ Ring.DimensionLEOne A) ↔ IsDedekindDomain A
Sources
  • ATLAS NumberTheoryI Definition 2.10, characterization form.
Used by 1
Used byDVR localizations in a Noetherian domain

TheoremDVR localizations in a Noetherian domain#✓fully proved

Let \(A\) be a Noetherian integral domain. Then the localizations \(A_P\) at all nonzero prime ideals \(P\) of \(A\) are discrete valuation rings if and only if \(A\) is integrally closed and has Krull dimension at most one.

theorem isDiscreteValuationRing_localization_atPrime_iff_integrallyClosed_dimensionLEOne
    (A : Type*) [CommRing A] [IsDomain A] [IsNoetherianRing A] :
    (∀ (P : Ideal A), P ≠ ⊥ → ∀ (_h : P.IsPrime),
      IsDiscreteValuationRing (Localization.AtPrime P)) ↔
    (IsIntegrallyClosed A ∧ Ring.DimensionLEOne A)
Sources
  • ATLAS NumberTheoryI Proposition 2.9.
Uses 1
Proof usesDedekind domains are the integrally closed Noetherian domains of dimension at most one

TheoremQuotients of Dedekind domains by nonzero ideals are principal ideal rings#✓fully proved

Every quotient of a Dedekind domain by a nonzero ideal is a principal ideal ring.

theorem IsDedekindDomain.isPrincipalIdealRing_quotient {A : Type*} [CommRing A]
    [IsDedekindDomain A] (I : Ideal A) (hI : I ≠ ⊥) : IsPrincipalIdealRing (A ⧸ I)

TheoremDomains with principal quotients are Noetherian#✓fully proved

Let \(A\) be an integral domain such that for every nonzero ideal \(I\) of \(A\) the quotient ring \(A/I\) is a principal ideal ring. Then \(A\) is a Noetherian ring.

For a nonzero ideal \(I\), pick a nonzero \(a \in I\); the image of \(I\) in the principal ideal ring \(A/(a)\) is principal, and lifting a generator to some \(b \in I\) shows \(I = (a, b)\), so \(I\) is finitely generated.

theorem isNoetherianRing_of_forall_isPrincipalIdealRing_quotient {A : Type*}
    [CommRing A] [IsDomain A]
    (h : ∀ I : Ideal A, I ≠ ⊥ → IsPrincipalIdealRing (A ⧸ I)) :
    IsNoetherianRing A
Used by 2
Used byDedekind domains from principal quotients · Principal quotients give discrete valuation rings at nonzero primes

TheoremPrincipal quotients give discrete valuation rings at nonzero primes#✓fully proved

Let \(A\) be an integral domain such that for every nonzero ideal \(I\) of \(A\) the quotient ring \(A/I\) is a principal ideal ring. Then for every nonzero prime ideal \(P\) of \(A\), the localization \(A_P\) is a discrete valuation ring.

The image of \(P\) in \(A/P^2\) is principal, generated by the image of some \(\pi \in P\), so \(P \subseteq (\pi) + P^2\). Hence the maximal ideal \(\mathfrak{m}\) of \(A_P\) satisfies \(\mathfrak{m} \subseteq (\pi) + \mathfrak{m}^2\), and Nakayama's lemma gives \(\mathfrak{m} = (\pi)\).

theorem isDiscreteValuationRing_localization_atPrime_of_forall_isPrincipalIdealRing_quotient
    {A : Type*} [CommRing A] [IsDomain A]
    (h : ∀ I : Ideal A, I ≠ ⊥ → IsPrincipalIdealRing (A ⧸ I))
    (P : Ideal A) (hPne : P ≠ ⊥) (hPpr : P.IsPrime) :
    IsDiscreteValuationRing (Localization.AtPrime P)
Uses 1 · Used by 1
Proof usesDomains with principal quotients are Noetherian
Used byDedekind domains from principal quotients

TheoremDedekind domains from principal quotients#✓fully proved

Let \(A\) be an integral domain such that for every nonzero ideal \(I\) of \(A\) the quotient ring \(A/I\) is a principal ideal ring. Then \(A\) is a Dedekind domain.

theorem isDedekindDomain_of_forall_isPrincipalIdealRing_quotient {A : Type*}
    [CommRing A] [IsDomain A]
    (h : ∀ I : Ideal A, I ≠ ⊥ → IsPrincipalIdealRing (A ⧸ I)) :
    IsDedekindDomain A
Sources
  • converse of ATLAS NumberTheoryI, Corollary 3.18, derived independently.
Uses 2 · Used by 1
Proof usesPrincipal quotients give discrete valuation rings at nonzero primes · Domains with principal quotients are Noetherian
Used byDedekind domains from two generators with one prescribed

TheoremTwo generators with one prescribed give principal quotients#✓fully proved

Let \(A\) be an integral domain such that for every nonzero ideal \(I\) of \(A\) and every nonzero \(a \in I\) there is \(b \in A\) with \(I = (a, b)\). Then for every nonzero ideal \(I\) of \(A\), the quotient ring \(A/I\) is a principal ideal ring.

For a nonzero ideal \(I\), an ideal \(J\) of \(A/I\) has preimage \(J'\) in \(A\) containing \(I\); pick a nonzero \(a \in I\), write \(J' = (a, b)\), and the image of \(b\) generates \(J\) since the image of \(a\) is zero.

theorem isPrincipalIdealRing_quotient_of_forall_exists_span_pair {A : Type*}
    [CommRing A] [IsDomain A]
    (h : ∀ (I : Ideal A) (a : A), I ≠ ⊥ → a ≠ 0 → a ∈ I →
      ∃ b : A, I = Ideal.span {a, b}) :
    ∀ I : Ideal A, I ≠ ⊥ → IsPrincipalIdealRing (A ⧸ I)
Used by 1
Used byDedekind domains from two generators with one prescribed

TheoremDedekind domains from two generators with one prescribed#✓fully proved

Let \(A\) be an integral domain such that for every nonzero ideal \(I\) of \(A\) and every nonzero \(a \in I\) there is \(b \in A\) with \(I = (a, b)\). Then \(A\) is a Dedekind domain.

theorem isDedekindDomain_of_forall_exists_span_pair {A : Type*}
    [CommRing A] [IsDomain A]
    (h : ∀ (I : Ideal A) (a : A), I ≠ ⊥ → a ≠ 0 → a ∈ I →
      ∃ b : A, I = Ideal.span {a, b}) :
    IsDedekindDomain A
Sources
  • converse of ATLAS NumberTheoryI, Theorem 3.22, derived independently.
Uses 2
Proof usesDedekind domains from principal quotients · Two generators with one prescribed give principal quotients
11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.