Should zero ring be finite-dimensional?

Stream: mathlib4

[Wang Jingting]

In PR #21041, we were trying to port @Andrew Yang 's lean3 repository about dimension theory, and we encountered the following problem while opening the PR to mathlib, so we thought it's probably better to go on zulip and ask for people's suggestions.

We were trying to translate the concept of FiniteRingKrullDim, which refers to a ring having finite krull dimension. Andrew Yang pointed out in his review comment to the PR that we should be using FiniteDimensionalOrder directly, but we noticed that this would probably make the zero ring not finite-dimensional, since FiniteDimensionalOrder α doesn't hold when α is empty.

So my question is that, should we make the zero ring to be not finite-dimensional? Or, should we refactor the definition of FiniteDimensionalOrder?

Note: The definition of FiniteDimensionalOrder is Rel.FiniteDimensional with respect to the < relation, and the definition of Rel.FiniteDimensional is that there exists a longest RelSeries (which doesn't allow empty series)

[Andrew Yang]

My response on the PR:

Hmmm. I think it is probably fine. If we later need a "finitedimensionalorder-or-empty" typeclass we can add it later. Or arguably FiniteDimensionalOrder is just wrong and we should fix that.

And I think @Christian Merten agrees.

[Christian Merten]

I think we should change FiniteDimensionalOrder to allow IsEmpty and assume Nonempty when it is actually needed.

[Junyan Xu]

It seems we need to introduce Rel.krullDim which is Order.krullDim with LTSeries replaced by RelSeries. (In)FiniteDimensionalOrder should then be defined in terms of krullDim.

[Wang Jingting]

Thanks for everyone's suggestions!