downward-closedness under a general relation

Stream: Is there code for X?

[Junyan Xu]

Mathlib currently have docs#is_lower_set and docs#is_upper_set, which are both special cases of the predicate ∀ {a' a}, r a' a → p a → p a' that says the set (or predicate) p is downward closed under r, for r = (≤) and r = (≥) respectively.

This downward-closedness predicate doesn't seem to exist in mathlib, so in acc.of_downward_closed, the condition that the image of f is downward closed under r is written out explicitly. More recently, in my surreal multiplication work, I use the fact being numeric is downward closed under is_option, and I showed if p is downward closed under r, then λ s, ∀ a ∈ s, p a is downward closed under cut_expand r, and I also basically showed that p is also downward closed under trans_gen r. All of this seems in favor of introducing the downward-closedness predicate (maybe we should just call it relation.closed without "downward"), but refactoring and golfing stuff around is_lower_set/is_upperset (which I guess relied on order_dual to dualize?) would be beyond my capacity. I think (from #12189) maybe @Yaël Dillies would be interested in this? Thanks in advance for your consideration.

[Yaël Dillies]

I am happy to golf is_upper_set and is_lower_set, but there is not much to gain because no proof takes more than a line already.

[Yaël Dillies]

Also, if you do want to introduce relation.closed, I think file#order/upper_lower is indeed a good place for it.

[Violeta Hernández]

I'm not quite sure what benefit such a predicate would have, other than increased readability. That said, I don't oppose it.

[Junyan Xu]

Actually the condition dc in docs#acc.of_downward_closed (that the image of a function is downward closed) also appears in docs#initial_seg.

[Junyan Xu]

I'm not that familiar with initial_seg; are there anything general about downward-closedness that could be proven and used to golf proofs about initial_seg?

[Yaël Dillies]

I'm not quite sure what initial_seg is useful for, but I need initial segments of the colexicographical order for Kruskal-Katona (#2770).

[Yaël Dillies]

Note that initial segments are the same as (open?) lower sets only in linear orders. This is causing me trouble in the colexicographical order because it's not linear (or rather colex is linear, but colex + same size isn't).

[Junyan Xu]

How is it so? The only difference between docs#is_lower_set and the condition in your is_init_seg_of_colex seems to be the difference between le and lt, but docs#le_iff_lt_or_eq is available for partial orders, not necessarily linear.

[Junyan Xu]

I'm not quite sure what initial_seg is useful for, but I need initial segments of the colexicographical order for Kruskal-Katona (#2770).

Given any two ordinals, one of them embeds as an initial segment in the other, and docs#initial_seg is the data structure for such embeddings. Violeta has more experience working with the ordinal library than me; if he doesn't see a benefit then probably there's also no benefit from the downward-closedness predicate there (other than readability).

[Junyan Xu]

So for partial orders, being downward closed under (<) or (≤) are both equivalent to docs#is_lower_set, but for preorders, downward closedness under (<) is a weaker condition.

[Junyan Xu]

I am a bit ambivalent about the names; I don't want to use "downward" because a general relation can't be said to have a lower and an upper direction; rather it's closed towards the left (from the right argument to the left argument), but maybe we should just say "closed" and consider the right to left direction as a convention.

If dot notation is available, I'd like to write s.closed_under r or r.preserves s. Unfortuantely dot notation is only available to set and not functions like predicates or relations, so for e.g. a predicate p we could only possibly write relation.closed p r.

[Bhavik Mehta]

Yaël Dillies said:

Note that initial segments are the same as (open?) lower sets only in linear orders. This is causing me trouble in the colexicographical order because it's not linear (or rather colex is linear, but colex + same size isn't).

colex + same size is linear, in fact this was a key part in the original proofs of #2770. To put it simply, the relation relevant there is the colex relation restricted to sets which are all the same size, and since the whole ordering is linear clearly any restriction must also be

[Violeta Hernández]

As far as I understand, initial_seg is just an auxiliary definition that's used to prove basic properties on ordinal ordering and nothing else

[Violeta Hernández]

e.g. an ordinal is less-equal to another when there's an initial ordering from one to the other

[Violeta Hernández]

I think initial_seg is more useful due to being a structure instead of a predicate. Compare equiv to function.bijective (except the former is a bit harder to write down manually)

[Eric Wieser]

Regarding the original message; you can spell this concept as (r ⇒ swap (→)) p p

[Eric Wieser]

(docs#relator.lift_fun)

[Yaël Dillies]

Bhavik Mehta said:

Yaël Dillies said:

Note that initial segments are the same as (open?) lower sets only in linear orders. This is causing me trouble in the colexicographical order because it's not linear (or rather colex is linear, but colex + same size isn't).

colex + same size is linear

No, that's my point. colex + same size isn't linear, but colex restricted to same size is. In the first case, sets of different sizes are incomparable. In the second, all sets have the same size so we do inherit linearity.

[Violeta Hernández]

You know, after seeing your code, I support this idea

[Violeta Hernández]

The explicitly written down condition for downwards closedness isn't immediate to understand

[Violeta Hernández]

Also, dot notation!

[Violeta Hernández]

Update on this: after actually trying to work with initial segments, I realized they were the real deal and not just an auxiliary definition

[Violeta Hernández]

I opened #15328 to move these definitions to their own file