What do you want to do with this? I've thought about the height of an order myself and came to the conclusion that we would want it to be ℕ-valued.

@YaelDillies I would like to define heights of primes, Krull dimensions of rings, codimensions of irreducible closed subsets etc. (cf This Zulip thread)

What is the reason behind the conclusion? I don't have a good way to deal with the unbounded case when it is ℕ-valued.

If we want a nat-valued height, perhaps we should define it on a type with well-founded <? Relevant refactor: #15023.

I think < being well-founded does not guarantee that the global height would be finite. It only guarantees that the height of all the elements are finite.

Oh of course. But the nice thing is that all elements have a finite height iff < is well-founded, so this is the most general class you could define this in.

Actually, more generally, we should have a height function on is_well_founded. I'll add that as yet another to-do in the aforementioned refactor.

Can't you just use grade_min_order ℕ α or grade_bounded_order enat α and talk about grade ℕ ⊤/grade enat ⊤? Are some of the examples above not graded? That is, can maximal chains between two elements have different lengths?

Not really. Not every topological space (or ring) is catenary.

Oh wait, I totally lied to you. Well founded orders don't necessarily have a nat-valued height function: consider enat. They do have an ordinal-valued height function though. That should be worked on separately, and maybe these two APIs can be linked at some point.

Expanding on that previous thought: my relevant refactor introduces an is_well_founded typeclass. We could use it to define a height function taking an [is_well_founded α r] argument, similar to our current ordinal.type and ordinal.typein (in fact, ordinal.typein is just a special case of this).

This isn't really relevant to this PR though, I'm just thinking out loud.

@erdOne @vihdzp Do I understand correctly that the consensus is that this PR is basically ready to go. Connections to other concepts will be done in future work?

I think yes?

I'm not sure this is the right way to do things. It certainly is a bit weird if you're interested in studying finite orders. Maybe a literature dive would help here.

I could golf a bit further with your changes, so I integrated them. I'm quite happy with the current state of things although some golfing should still be possible.

maintainer merge

🚀 Pull request has been placed on the maintainer queue by alreadydone.

CI fails because the implicitness of the function in pairwise_of_fn changed, apparently.

Please open a corresponding mathlib4 PR (even an empty one).

Riccardo, it's already here: leanprover-community/mathlib4#1762

My bad, too many teaching hours these days.

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests