Dedekind ring

Stream: mathlib4

[Andrew Yang]

We have the following in mathlib, but this looks very suspicious to me

/-- 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. -/
class IsDedekindRing
  extends IsNoetherian A A, DimensionLEOne A, IsIntegralClosure A A (FractionRing A) : Prop

Are arbitrary artinian rings supposed to be dedekind rings?

Furthermore, Ring.DimensionLEOne is a deceiving name too because its implementation is

/-- A ring `R` has Krull dimension at most one if all nonzero prime ideals are maximal. -/
class Ring.DimensionLEOne : Prop where
  (maximalOfPrime : ∀ {p : Ideal R}, p ≠ ⊥ → p.IsPrime → p.IsMaximal)

which is very wrong for non-domains.

Hence, under our definitions IsDedekindRing R ↔ IsDedekindDomain R ∨ IsArtinianRing R.
I cannot find a good reference on non-domain dedekind rings to say for sure, but I really don't think this is what we were trying to describe with this typeclass.

So, what's the fix here (of both IsDedekindRing and Ring.DimensionLEOne)?

[Johan Commelin]

Maybe Ring.DimensionLEOne stems from before we had krullDim?

[Andrew Yang]

Yeah I think so. But the question is then: Is it saying what it wants to say with the wrong name, or should the definition be changed, or maybe just add a IsDomain R and pretend everything is fine?

[Johan Commelin]

I feel like the predicate is a useful one. So maybe we need a better name.

[Kevin Buzzard]

For DimensionLEOne your point is that $\mathbb{Z}[X]/(X^2)$ has dimension 1 but not DimensionLEOne, so this should definitely be fixed. I'm not sure what a good definition is -- maybe "P <= Q <= R implies P=Q or Q=R" (for prime ideals)? for Dedekind rings my instinct is that this is a mathlibism, do people really talk about Dedekind rings which aren't Dedekind domains in the literature?

[Kevin Buzzard]

Whatever the intention of DedekindRing was, it's hard to imagine that it has been correctly implemented. For example $\mathbb{Z}\times\mathbb{Z}$ doesn't look like it's going to be a Dedekind ring because it doesn't have DimensionLEOne.

[Kevin Buzzard]

I'm guessing that the idea was "smooth affine possibly-not-connected curve"?

[Kevin Buzzard]

So this seems to be the relevant thread. Seems like the initial motivation was just that because we already have IsDomain it was annoying to have to write IsDedekindDomain as well, so the idea was to split it off. It's not clear to me that there were any planned applications of IsDedekindRing beyond domains.

[Antoine Chambert-Loir]

in Bosch, Lutkebohmert, Raynaud, they work with more general Dedekind rings than domains. On the other hand, their local rings are either fields or dvr.

[Antoine Chambert-Loir]

I just checked. I was slightly wrong: they talk about Dedekind schemes, which are defined as Noetherian, normal schemes of dimension at most 1. I could find 6 occurrences of the expression Dedekind ring in their book, and 2 occurrences of Dedekind domain; in all cases, they write something like “over a field or a Dedekind [domain|ring]”, which seems to imply that Dedekind rings are not fields.

[Junyan Xu]

To fix docs#Ring.DimensionLEOne we might say any prime is either maximal or minimal, using docs#minimalPrimes. We might introduce DimensionLEZero simultaneously.

[Antoine Chambert-Loir]

I just checked the definition in Bourbaki for whom a Dedekind ring is a Krull ring of which all nonzero prime ideals are maximal. (A Krull ring is an integral domain which is defined by a set of discrete valuations on its field of fractions) With their definition, a field is a Dedekind ring.

[Andrew Yang]

The context is precisely me trying to introduce such a dim = 0 typeclass and running to a naming conflict with docs#Ideal.IsPrime.isMaximal

[Junyan Xu]

docs#Ideal.IsPrime.isMaximal (lowercase i after the last dot)

[Andrew Yang]

(and the PR is #20108; almost done)

[Antoine Chambert-Loir]

Regarding dimension: we have an ordered set, the set of prime ideals, and the dimension is that of this ordered set. So I believe that the dimension_le_oneshould just be an abbreviation to a similar predicate on ordered sets. Given the difficulty of deciding the value of the dimension of an infinite dimensional thing (0 or infinity?), the above suggestion of @Junyan Xu would be perfect.

[Antoine Chambert-Loir]

(It could easily be generalized to dimension_le_nat…)

[Junyan Xu]

Mathlib has the theory for general ordered sets docs#Order.krullDim, and it takes value in natural numbers as well as $\pm\infty$. The specialization to comm. rings is docs#ringKrullDim. Andrew's PR proves RingKrullDimZero R ↔ ringKrullDim R = 0 assuming Nontrivial, and it should also be true that RingKrullDimZero R ↔ ringKrullDim R ≤ 0 without that assumption, so DimensionLEZero is probably a more appropriate name and it aligns with DimensionLEOne.

[Andrew Yang]

I think I'll pause that PR for now because I like Antoine's suggestion more.

[Junyan Xu]

So you're going to refactor DimensionLEOne? That might be a good idea. I've heard people are introducing ProjectiveDimensionLE too.

[Junyan Xu]

Stacks' proof of Noetherian + zero-dim -> Artinian is a bit complicated but would be much easier using (Akizuki's commutative version of) Hopkins--Levitzki, because it's easy to show a Noetherian ring of zero dimension is semiprimary. (It's essentially the same proof.)

[Andrew Yang]

I have that proof here #20096. I did it 3 years ago in lean3 so I don't remember what proof I followed though.