Length of longest chain

Stream: Is there code for X?

[Andrew Yang]

Is there any results regarding the length of a the longest ascending chain in an order? One that presumably takes values in $\mathbb{N} \cup \{\infty\}$.

I would like to define the Krull dimension of rings and topological spaces, and also height of primes, codimensions of subspaces, etc.

[Junyan Xu]

I guess you can work with docs#is_max_chain and just prove every max chain has the same cardinality, etc.?

[Junyan Xu]

When the chain is finite, I think we'd like to know it can be arranged into a list in ascending order. Can we use some development from docs#composition_series ?

[Junyan Xu]

I suspect it's easier to work with docs#list.chain has_lt.lt, then we can talk about length of the list instead of cardinality. "maximal length" just means having max length among all chains. However it seems we don't have a predicate on it saying the chain is maximal (i.e. nothing can be inserted while keeping it a chain). The max length is infinity precisely when there is no list that is a max length chain.

[Violeta Hernández]

Part of the problem with having API for "length of longest chain" is that the output type is far from obvious, particularly regarding infinite chains

[Violeta Hernández]

A quite natural output type is enat, but if you're working with finite structures, you'll probably want ℕ instead, and if you're working with well-founded orders, you'll want ordinal instead, and there's a case to be made for cardinal too.

[Violeta Hernández]

I agree with Junyan in that you might be better off working with is_max_chain directly and adding the necessary lemmas that suit your needs

[Andrew Yang]

I was planning on considering the sup (in enat) of all the lengths of finite strictly ascending chains. I think this is what @Junyan Xu is talking about as well?

[Junyan Xu]

enat didn't come to my mind before Violeta mentioned it, but it seems the right way to go, yes.