Should `IsDedekindDomain` extend `IsDomain`?

Stream: general

[Anne Baanen]

Right now to assume a Dedekind domain we write variable {R : Type _} [CommRing R] [IsDomain R] [IsDedekindDomain R] since docs#IsDedekindDomain takes docs#IsDomain as a parameter. Should we use extends instead so we only write variable {R : Type _} [CommRing R] [IsDedekindDomain R]? (Are there any useful "Dedekind rings" that are IsDedekindDomain but not IsDomain?)

[Johan Commelin]

I don't know of any examples. Note that "integrally closed" already assumes the ring to be a domain.

[Johan Commelin]

That assumption could maybe be dropped. But I'm not yet convinced that it is useful to diverge from the standard maths setup here.

[Anne Baanen]

I mean:

class IsDedekindDomain (A : Type _) [CommRing A] extends IsDomain A where
  isNoetherianRing : IsNoetherianRing A
  dimensionLEOne : DimensionLEOne A
  isIntegrallyClosed : IsIntegrallyClosed A

instead of the current situation

class IsDedekindDomain (A : Type _) [CommRing A] [IsDomain A] : Prop where
  isNoetherianRing : IsNoetherianRing A
  dimensionLEOne : DimensionLEOne A
  isIntegrallyClosed : IsIntegrallyClosed A

[Riccardo Brasca]

I agree with this. I don't think mathematically there any interesting examples of Dedekind "domains" that are not domains (as the name suggest).

[Anne Baanen]

Or perhaps:

class IsDedekindDomain (A : Type _) [CommRing A]
    extends IsDomain A, IsNoetherianRing A, IsIntegrallyClosed A where
  dimensionLEOne : DimensionLEOne A

[Anne Baanen]

And we might even want to turn DimensionLEOne into a class so IsDedekindDomain can be defined without any of its own fields.

[Damiano Testa]

I would also agree. It seems that the only potential gain in not assuming IsDomain is that you allow products of Dedekind domains to be Dedekind domains. Does allowing products possibly simplify some arguments?

In my mind, being a Dedekind domains is a property checked locally, so the "global" IsDomain is not really needed and not really harmful either!

[Johan Commelin]

So should IsIntegrallyClosed also extend IsDomain? I don't really have an idea/pref...

[Riccardo Brasca]

Ah, it's even worse: currently you cannot drop IsDomain I think (because it is required by IsIntegrallyClosed.

[Johan Commelin]

But is it really?

[Riccardo Brasca]

I mean that you have to write [IsDomain R] [IsDedekindDomain R]

[Johan Commelin]

Wouldn't it pick up the instance that is extended?

[Johan Commelin]

I think we can technically just drop that assumption from the defn of IsIntegrallyClosed.

[Johan Commelin]

Let me test

[Riccardo Brasca]

This

import Mathlib.RingTheory.DedekindDomain.Basic

example {R : Type} [CommRing R] [IsDedekindDomain R] : True := trivial

gives an error

[Anne Baanen]

Riccardo Brasca said:

This

import Mathlib.RingTheory.DedekindDomain.Basic

example {R : Type} [CommRing R] [IsDedekindDomain R] : True := trivial

gives an error

Indeed, this is what I want to change :)

[Riccardo Brasca]

Then I agree even more than before, you are not even changing the mathematics (in the sense that already now a Dedekind domain is a domain)

[Johan Commelin]

Johan Commelin said:

I think we can technically just drop that assumption from the defn of IsIntegrallyClosed.

class IsIntegrallyClosed (R : Type _) [CommRing R] : Prop where
  /-- All integral elements of `Frac(R)` are also elements of `R`. -/
  algebraMap_eq_of_integral :
    ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, algebraMap R (FractionRing R) y = x

typechecks

[Johan Commelin]

Would this more general definition be helpful? Does it mean that products of integrally closed things would be integrally closed?

[Riccardo Brasca]

At least Domain is not in the name of IsIntegrallyClosed...

[Damiano Testa]

Am I right that there are two overlapping issues here?

Anne wanted to simply reorganize assumptions, so that Dedekind domains stay domains, but the assumptions is extended. The discussion got partially hijacked into the question of whether even assuming that Dedekind domains should be domains at all.

[Johan Commelin]

Is the FractionRing of $\mathbb{Z} \times \mathbb{Z}$ isomorphic to $\mathbb{Q} \times \mathbb{Q}$?

[Damiano Testa]

My personal view is that it might make some arguments easier to not have to carry around the domain hypothesis, though the name Dedekind domain should be reserved for something that is a domain!

[Damiano Testa]

Johan Commelin said:

Is the FractionRing of $\mathbb{Z} \times \mathbb{Z}$ isomorphic to $\mathbb{Q} \times \mathbb{Q}$?

I think so. If I remember correctly, the "total fraction ring" of a product is the product of the total fraction rings. Things get more subtle for connected schemes.

[Johan Commelin]

In that case, I'm inclined to drop IsDomain from IsIntegrallyClosed and rename IsDedekindDomain to IsDedekindRing.

[Damiano Testa]

Johan, the first example of Wikipedia mentions products: it should be what I said.

[Johan Commelin]

Perfect!

[Johan Commelin]

We should probably mention "total ring of fractions" in the docstring of FractionRing.

[Johan Commelin]

I don't think I've heard of that concept before.

[Damiano Testa]

There is a paper of Kleiman on the total ring of fractions, clearing up issues that had arisen.

[Johan Commelin]

That paper is already mentioned here:

Mathlib/FieldTheory/RatFunc.lean
90:* [Kleiman, *Misconceptions about $K_X$*][kleiman1979]
91:* https://freedommathdance.blogspot.com/2012/11/misconceptions-about-kx.html

[Johan Commelin]

#5827 adds "total fraction ring" to the docstring

[Anne Baanen]

Should I open a PR now to make the proposed changes, or wait for the port to be officially over?

[Scott Morrison]

Certainly you can open the PR now. The question is only whether to mark it after-port.

[Anne Baanen]

I went ahead and opened #5833 (turn DimensionLEOne into a class) and #5834 (make IsDedekindDomain extend all the hypotheses). Next two will be forgetting IsDomain in IsIntegrallyClosed and IsDedekindDomain.

[Kevin Buzzard]

Do you think that a Dedekind domain without the domain hypothesis should be called a Dedekind ring instead?

[Johan Commelin]

That's what I've been using as a working assumption so far :wink: