feat(Order/KrullDimension): add some basic lemmas about krull dimension of a preorder

[jjaassoonn]

trafficstars

• krull dimension, height, coheight interacting with functions
• order dual

These will be specialized to ring theoretic krull dimension later

---

• [ ] depends on:#11730

[jjaassoonn]

What's your use case for KrullDimOfRel?

I have no other use of KrullDimOfRel other than specializing it into KrullDim. But I thought I could add it for the sake of generality.

[YaelDillies]

Then let's turn it into a note instead. I doubt people will ever need it.

[YaelDillies]

No sorry I meant "let's remove the definition and add a note about how we could have it but don't because nobody needs it".

[jjaassoonn]

No sorry I meant "let's remove the definition and add a note about how we could have it but don't because nobody needs it".

Thanks for the clarification and sorry for the misunderstanding. Only after I removed krullDimOfRel, I realized that it might be useful afterall, because a composition series is a relation series of \covby, anyway, If it turns out to be useful, I will open another PR and revert the change I guess.