Preorder from function iteration

Stream: Is there code for X?

[Daniel Weber]

For any function f : a -> a we can define a preorder by a ≤ b <-> exists n, f^[n] a = b. This is also a successor order with succ = f. Is this in Mathlib?

[Yaël Dillies]

Pretty sure this is not, no. It might exist in category theory?

[Kim Morrison]

(Don't think so.)

[Daniel Weber]

What would be a good location for this definition?

[Yaël Dillies]

I think it should be somewhere in Algebra.Group.Action, by defining n • a = f^[n] a. Does that fit the bill for your application?

[Daniel Weber]

How do I get an order from that? In my current application I want to apply docs#AntisymmRel.setoid to it and then look at docs#Finpartition.ofSetoid, and I have another use planned where I make a docs#SuccOrder from it.

[Yaël Dillies]

AntisymmRel.setoid is just looking at the orbits of f, right? The SuccOrder part I'm not sure

[Daniel Weber]

Oh, looking at docs#MulAction.orbit does seem like it might be nicer. Is there a way to get a docs#Finpartition of those?

[Daniel Weber]

I want the SuccOrder to make a tree from a function mapping each node to its parent

[Daniel Weber]

Actually, it's only orbits for a permutation, not for a general function