Heights of posets

Stream: maths

[Andrew Yang]

The PR #15026 defines the height of a poset as the supremum (in enat) of the lengths of finite strictly increasing sequences. I have never studied any order theory, and I just want a way to do mathematically trivial calculations regarding heights of prime ideals, lengths of module etc. However, @Yaël Dillies thinks that the current approach is weird, so I was wondering if there is a standard or a more general/sophisticated way to deal with these objects in order theory?

There were some previous discussions here.

[Violeta Hernández]

I think the approach is fine, though it shouldn't be the only approach we eventually implement.

[Bhavik Mehta]

The approach looks sensible to me - certainly on paper I'd expect to see extended naturals for this quantity. It's not too clear to me what's weird about this approach - or rather, what the advantage of specialising to finite orders is. Is the definition you currently have useful for your applications?

[Bhavik Mehta]

Here's one example of extended naturals being used in literature: https://stacks.math.columbia.edu/tag/02I0

[Andrew Yang]

I think this will be useful for my applications, but I also agree that the things in mathlib should be done in the right generality, and I have no experience in order theory to judge. Hopefully Yaël could elaborate more on the caveats of this approach?

[Kevin Buzzard]

When one is applying these ideas to ring theory enat should be fine. Typically if one is talking about chains of prime ideals one is in a situation where all chains are finite length (because one is not interested in the idea otherwise) so one possibility is doing enat and another possibility is that we assume Noetherian and then do everything in nat...