[Merged by Bors] - feat(order/height): The height of a poset

[erdOne]

---

Match leanprover-community/mathlib4#1762

[vihdzp]

General comments + a few ramblings you can probably ignore

[YaelDillies]

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.

[erdOne]

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

[vihdzp]

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

[erdOne]

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.

[vihdzp]

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.

[vihdzp]

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.

[YaelDillies]

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?

[erdOne]

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

[vihdzp]

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.

[vihdzp]

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.

[jcommelin]

@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?

[erdOne]

I think yes?

[YaelDillies]

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.

[YaelDillies]

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.

[alreadydone]

maintainer merge

[github-actions]

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

[alreadydone]

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

[riccardobrasca]

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

[YaelDillies]

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

[riccardobrasca]

My bad, too many teaching hours these days.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

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