Zulip Chat Archive
Stream: Is there code for X?
Topic: Minimal elements and descending chains
Yaël Dillies (Jan 04 2022 at 16:40):
Is there any way to talk about the minimal elements of a set in an order and do we have the proof that if the set has no descending chain every element is greater than a minimal element?
Eric Rodriguez (Jan 04 2022 at 16:42):
file#src/order/well_founded_set?
Yaël Dillies (Jan 04 2022 at 16:42):
Pretty certain we don't have that as pure order theory (except for docs#set.is_wf and around), but I'm sure you ring people will have done it on your own
Eric Rodriguez (Jan 04 2022 at 16:43):
specifically maybe docs#set.well_founded_on_iff_no_descending_seq
Yaël Dillies (Jan 04 2022 at 16:44):
I know about all of that, but it doesn't talk about minimal elements.
Eric Rodriguez (Jan 04 2022 at 16:45):
docs#set.is_wf.min? or am I missing something dumb again... you'll know more about the order theory
Yaël Dillies (Jan 04 2022 at 16:45):
Nah, this is for a linear order.
Yaël Dillies (Jan 04 2022 at 16:48):
I'm actually interested in cowellfoundedness, not wellfoundedness. And my end statement is that a downward closed set of finsets of maximal elements of size n contains finsets of all lower sizes under each finset.
Yaël Dillies (Jan 04 2022 at 16:49):
The size bit is generally true in a ranked/graded order, and I expect the "I'm less than some maximal element" is true generally.
Yaël Dillies (Jan 04 2022 at 16:50):
@Violeta Hernández, you might have ideas.
Floris van Doorn (Jan 04 2022 at 16:50):
For the first question do you mean docs#is_least? EDIT: oh wait, you asked for minimal, but that might still suffice if you're working in a linear order.
I don't think the second question is there, but it shouldn't be too hard with docs#zorn.zorn_partial_order (on docs#order_dual) + a lemma that states that for a linear order is_least coincides with being minimal.
Reid Barton (Jan 04 2022 at 16:55):
Yaël Dillies said:
Nah, this is for a linear order.
What is?
Yaël Dillies (Jan 04 2022 at 16:56):
Oh yeah of course. I wanted the set of minimal elements, but is_least will do EDIT: No, it doesn't. However I don't see how Zorn helps here. Zorn doesn't know about the ascending/descending chain condition.
Yaël Dillies (Jan 04 2022 at 16:57):
Ah, maybe if I apply set.is_wf.min to a subset of my original set?
Floris van Doorn (Jan 04 2022 at 16:59):
Oh I see, there is indeed a gap between your formulation and Zorn... You could still use Zorn: if there is no infinite descending chain, then every chain is finite so has a lower bound, so by Zorn you get a minimal element. Probably there is a more direct proof though.
Yaël Dillies (Jan 04 2022 at 17:02):
Also, is there really no dual to docs#set.is_wf? I foresee that doing through order_dual might be a bit painful.
Yaël Dillies (Jan 04 2022 at 17:07):
Btw, I already defined maximal elements as docs#is_antichain.mk. Maybe it deserves a better name...
Floris van Doorn (Jan 04 2022 at 17:11):
That definitely deserves a better name, since you could equally well have taken the minimal elements :-)
Yaël Dillies (Jan 04 2022 at 17:11):
Okay, I will make a new file with definitions maxima and minima and a little API!
Yaël Dillies (Jan 04 2022 at 17:12):
Maybe we can then refactor order.zorn to use it?
Yaël Dillies (Jan 04 2022 at 17:14):
I can also add them to order.bounds. Any preference?
Floris van Doorn (Jan 04 2022 at 17:17):
If you formulate them using the ≤ relation, order.bounds seems like the right place to put it. Otherwise, not so much.
Yaël Dillies (Jan 04 2022 at 17:18):
Given that is_antichain works for any relation, it would be nice if minima and maxima did too.
Reid Barton (Jan 04 2022 at 17:19):
This might be overly pedantic, but maxima is the plural of maximum which (in what I consider to be the standard usage) is not the word you want--you are interested in maximal elements. (Same for minima.)
Reid Barton (Jan 04 2022 at 17:20):
e.g. http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/maximal+element
Yaël Dillies (Jan 04 2022 at 17:22):
So maximals and minimals? (I want them as a set to talk about union and stuff)
Reid Barton (Jan 04 2022 at 17:22):
Maximal and minimal elements aren't really bounds, you might create a new file, and cross-reference it from order.bounds
Yaël Dillies (Jan 05 2022 at 18:23):
Violeta Hernández (Jan 06 2022 at 03:13):
Yaël Dillies said:
Violeta Hernández, you might have ideas.
I proved something similar in the polytope branch
Violeta Hernández (Jan 06 2022 at 03:13):
Specifically, what I proved is that a graded order with top grade n has elements of all grades from 0 to n
Violeta Hernández (Jan 06 2022 at 03:13):
...but you probably already knew that, haha
Yaël Dillies (Jan 06 2022 at 09:40):
Yeah, I'm thinking this is almost what I want!
Yaël Dillies (Jan 06 2022 at 09:42):
The general case is an arbitrary interval of the order, rather than all elements. I assume it's not too hard to adapt your proof?
Last updated: Dec 20 2023 at 11:08 UTC