Dedekind domain definitions

Stream: Is there code for X?

[Jiang Jiedong]

Hi everyone,

In Stacks Project, a Dedekind domain $R$ is a domain such that every nonzero ideal has a unique (up to permutation) prime ideal multiplicative decomposition, see Definition 034W. This implies that $R$ Noetherian, and it is equivalent to other definitions (like local DVR and the mathlib one).

Q1. Is the Stacks' definition the same as requiring [IsDomain R] and [UniqueFactorizationMonoid (Ideal R)]?

Q2. Do we have this precise definition in Mathlib? Or do we have a theorem saying this definition implies IsDedekindDomain?

[Kenny Lau]

@Jiang Jiedong but how would you ever prove that a domain has unique factorisation of ideals?

[Kenny Lau]

note that the other direction (which is the more useful one) is Ideal.uniqueFactorizationMonoid:

instance Ideal.uniqueFactorizationMonoid {A : Type u_2} [CommRing A] [IsDedekindDomain A] :
    UniqueFactorizationMonoid (Ideal A)

[Jiang Jiedong]

Kenny Lau said:

Jiang Jiedong but how would you ever prove that a domain has unique factorisation of ideals?

This direction is not so useful indeed. But it could be an interesting formalization exercise.

[Kenny Lau]

@Jiang Jiedong go ahead

[Andrew Yang]

Here are some more equivalent characterizations that might be fun to do
Let $R$ be a domain (that is not a field), then TFAE

• $R$ is noetherian, integrally closed of dim 1
• $R$ is noetherian with DVR stalks
• $R$ is noetherian and every nonzero primary ideal is a power of a maximal ideal
• UniqueFactorizationMonoid (Ideal R)
• Semifield (FractionalIdeal R⁰ (FractionRing R))
• $R$ is a CDR (i.e. docs#Ideal.dvd_iff_le)
• $R/I$ is a PIR for all $I \ne 0$ (i.e. docs#IsDedekindDomain.exists_sup_span_eq).

The fact that each one implies the next (and last => first) should all be easy.

[Yakov Pechersky]

We have docs#IsDedekindDomainDvr

[Yongle Hu]

I think maybe it is docs#IsDedekindDomainInv, which is proven to be equivalent to docs#IsDedekindDomain by docs#IisDedekindDomain_iff_isDedekindDomainInv.

[Junyan Xu]

That looks like Semifield (FractionalIdeal R⁰ (FractionRing R))

[Yongle Hu]

My bad. But deriving Semifield (FractionalIdeal R⁰ (FractionRing R)) from UniqueFactorizationMonoid (Ideal R) maybe not very hard?