Should fields be Dedekind domains?

Stream: maths

[María Inés de Frutos Fernández]

Mathlib's definition of Dedekind domain includes fields. I know that if I want to restrict to the case of Krull dimension 1 (in which a prime ideal is maximal if and only if is nonzero), I can just add a ¬ is_field R hypothesis, but I was wondering if it would make sense to include this in the definition of Dedekind domain.
Both conventions are used, so I would like to know what other people think about this (@Anne Baanen?).

[Adam Topaz]

https://en.wikipedia.org/wiki/Dedekind_domain seems to agree that fields should be included.

[Adam Topaz]

Let me check what Neukirch has to say.

[María Inés de Frutos Fernández]

I think Neukirch includes fields.

[Adam Topaz]

Indeed!
Screenshot-2022-02-10-at-13-04-15-Neukirch1999_Book_AlgebraicNumberTheory-pdf.png

[Adam Topaz]

As far as I am concerned, that's sufficient evidence that fields should be included, but I don't actually have any strong opinions about this.

[Eric Rodriguez]

this discussion is mentioned in the implementation notes: https://leanprover-community.github.io/mathlib_docs/ring_theory/dedekind_domain.html#implementation-notes

[Anne Baanen]

In the end, we (@Sander Dahmen, @Filippo A. E. Nuccio, @Ashvni Narayanan and I) decided to allow fields to be DDs, because it's easier to include ¬ is_field in the hypotheses than remove it from the is_dedekind_domain structure. In fact, the initial definition excluded fields, and we changed that later

[María Inés de Frutos Fernández]

I see, thanks!

[Kevin Buzzard]

Wikipedia says that there are two conventions. I asked someone in our department and they immediately expressed the wonderful viewpoint that in their opinion they didn't think that fields should be PIDs! I can completely see their point! It's developing a theory of geometric objects of dimension <= 1 and then continuously having to say "...and not 0" the moment one gets going. Note that the definition of DVR (the local analogy of a Dedekind domain) does seem to exclude fields by convention. The question is analogous to whether 1 should be a prime -- it's an annoyance at the beginning having to exclude it but then you find that the meatier theorems don't work with it. It's also like whether the definition of filter should be bourbaki's or ours. Perhaps there's no good answer. Part of me wants to vote for fields being pre-Dedekind-domains but not Dedekind domains. However because "I'm not a field" is so easy to say in mathlib perhaps we just leave things as they are.

Note that I don't buy "the literature says this" as a defence though -- the literature is pretty adamant that our definition of filter is incorrect and that didn't stop us.

[Antoine Chambert-Loir]

If fields are not Dedekind rings, then the lemma that says that localizations of Dedekind rings are Dedekind rings will need to be adjusted.

[Antoine Chambert-Loir]

(Aside : I find very funny in the theory of algebraic number fields and their rings of integers that people usually say “prime ideal” when they mean “maximal ideal”!)

[María Inés de Frutos Fernández]

If the definition changed we would also need to check that the ring of integers of a global field is not a field, but this should be in mathlib in any case (I've opened #11956 for the number field case).