RelSeries vs List.chain vs Order.height

Stream: mathlib4

[Yury G. Kudryashov]

It looks like we have (at least) two ways to describe (almost) the same notion:

• docs#Set.chainHeight defined in terms of docs#List.chain';
• docs#krullDim and docs#height, defined in terms of docs#RelSeries

The only difference I see is that the latter definition returns an element of WithBot (WithTop Nat), so that it's bot, not 0 for an empty type. However, for a nonempty type it's always at least 1, so I don't see why do we need WithBot here.

Let me tag the authors @Andrew Yang and @Jujian Zhang. I failed to tag Fangming Li.

[Yury G. Kudryashov]

Note: I don't use this part of the library, so it's possible that I miss some other subtle difference in definitions. However, I'm confident that we should unify approaches to these 2 definitions.

[Jujian Zhang]

The dimension of a trivial ring should be negative infinity. For example, the dimension of product of two variety should be the sum of their dimensions. In this case if one of the variety is trivial, their product is also trivial. Then the dimension of a trivial variety needs to be negative infinity.

[Jujian Zhang]

It’s kind of like the degree of the zero polynomial should be negative infinity.

[Jujian Zhang]

Another example is that a field has krull dimension zero, which intuitively should be larger than krull dimension of a trivial ring.

[Kevin Buzzard]

It's like the dimension of the empty manifold being negative infinity, the dimension of R^n or the n-sphere S_n (as a manifold) is n, and the dimension of an infinite-dimensional Banach space (as a Banach manifold) is +infinity.

[Yury G. Kudryashov]

When you talk about dimensions of fields etc, which type with a Preorder do you associate to them?

[Jujian Zhang]

For fields (and rings in general), the RelSeries will be a series of prime ideals ordered by inclusion.

[Yury G. Kudryashov]

Also, am I right that the only way for krullDim α to be -∞ is for α to be empty? If yes, then it should be stated in the docstring.

[Yury G. Kudryashov]

BTW, am I right that docs#height and docs#Set.chainHeight are off by 1?

[Jujian Zhang]

In finite cases, I think so.

[Jujian Zhang]

One possible way to unify is perhaps to define a pred function from WithTop \Nat to WithBot (WithTop \Nat) by sending 0 to negative infinity, and define krull dimension to be pred of chain height?

[Yury G. Kudryashov]

BTW, why not use something like this?

def myHeight (s : Set α) : ENat := ⨆ (t ⊆ s) (ht : IsChain (⋅ < ⋅) t), Set.encard t

[Yury G. Kudryashov]

Jujian Zhang said:

One possible way to unify is perhaps to define a pred function from WithTop \Nat to WithBot (WithTop \Nat) by sending 0 to negative infinity, and define krull dimension to be pred of chain height?

It's just Order.pred (a : WithBot ENat)