Finite posets

Stream: Is there code for X?

[Jukka Kohonen]

Howdy. I have a question that is a mixture of "is there code" and "I don't even know how to do it". I would like to construct a (large) number of finite posets by their Hasse diagrams (covering relations), and then work with them like proving "this one is modular", "these are all possible posets on 7 elements" etc. How should I go about this? To start with, is there code that would take a cover relation and give me a poset (PartialOrder)? What would be a good "carrier type" for such finite posets? If I have 7 elements, Fin 7 would seem natural...?

[Yaël Dillies]

Don't use Fin 7! It already carries an order which will conflict with whatever you're trying to do. I would suggest you define your own inductive type for each finite order you care about (or find a family of finite orders it belongs to and define it instead). For locally finite orders (docs#LocallyFiniteOrder), a ≤ b iff there exists a sequence of elements each covering the next starting from a and ending at b. Namely, a < b ↔ TransGen (· ⋖ ·) a b (and a ≤ b ↔ ReflTransGen (· ⋖ ·) a b ↔ TransGen (· ⩿ ·) a b).

[Yaël Dillies]

I've been meaning to add this result but I had no need for it so it was very low priority for me. Feel free to open a PR for it and ask for my review!

[Yaël Dillies]

To create a (locally finite) preorder from a covering relation, you should use docs#ReflTransGen.

[Yaël Dillies]

I don't think it will be super easy to prove you get a preorder, though. The problem is that your covering relation needs to be acyclic, and this is not super easy to check.

[Jukka Kohonen]

Thanks for the advice! I'll try along those lines.