Zulip Chat Archive

Stream: maths

Topic: Heights of posets


Andrew Yang (Jul 18 2022 at 11:07):

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 (Jul 18 2022 at 14:35):

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

Bhavik Mehta (Jul 19 2022 at 18:15):

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 (Jul 19 2022 at 18:17):

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

Andrew Yang (Jul 19 2022 at 19:53):

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 (Jul 19 2022 at 22:25):

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...


Last updated: Dec 20 2023 at 11:08 UTC