Dual of is_filtered_or_empty_of_directed_order

Stream: general

[Yaël Dillies]

@Adam Topaz, @Kyle Miller, what is the dual lemma to

@[priority 100]
instance is_filtered_or_empty_of_directed_order
  (α : Type u) [directed_order α] : is_filtered_or_empty α :=
{ cocone_objs := λ X Y, let ⟨Z,h1,h2⟩ := directed_order.directed X Y in
    ⟨Z, hom_of_le h1, hom_of_le h2, trivial⟩,
  cocone_maps := λ X Y f g, ⟨Y, 𝟙 _, by simp⟩ }

you were hinting at? I'm in a position to prove it at branch#directed_mixin.

[Yaël Dillies]

Mostly, I don't know where you want the duals/opposites to be inserted.

[Adam Topaz]

is_cofiltered_of_empty_of_codirected_order ?

[Adam Topaz]

(sorry)

[Yaël Dillies]

Oh, is_cofiltered is a thing!

[Yaël Dillies]

Sorry, category theory newbie :sweat_smile:

[Adam Topaz]

At some point, I (and some other people) tried dualizing these results with bad results: #7980
I hope the mixin approach will resolve these issues -- I guess we'll see!

[Yaël Dillies]

Directed orders are barely used (less than 40 times) and they don't neatly fit in the hierarchy. Further, the mixin is Prop-valued. So I think it's all benef!

[Yaël Dillies]

Yeah, the full history is #7163, #7980, #9200 I think.

[Adam Topaz]

Looks like a graveyard of abandoned PRs...

[David Wärn]

What's the point of this lemma? It seems to encourage using 'wrong' definitions. The 'correct' definition of directed order should include nonempty α (then every finset has an upper bound, not only nonempty finsets), just like is_filtered does

[Adam Topaz]

Are you suggesting that the definition docs#directed_order should be changed?

[Yaël Dillies]

directed_order α wasn't including nonempty α, so I'm playing it conservative. My point with #11238 is really to turn from an extends to a mixin.

[Yaël Dillies]

If you really want is_directed α to include nonempty α, we can consider this in a followup PR. But I'm already noting that this would break away from the other unbundled relation classes.

[David Wärn]

Ok, I guess my question is orthogonal to this PR. I don't know if the definition of directed_order needs to change (you can still use it as [directed_order A] [nonempty A]), but it could maybe be renamed to 'predirected' in line with is_preconnected.

[Yaël Dillies]

Yes, this sounds more reasonable already :smile:

[Yaël Dillies]

This change is really doomed. There is random stuff breaking...

[Yaël Dillies]

Which pair of lemmas do you prefer?

lemma exists_ge_ge [has_le α] [is_directed α (≤)] (a b : α) : ∃ c, a ≤ c ∧ b ≤ c :=
lemma exists_le_le [has_le α] [is_directed α (swap (≤))] (a b : α) : ∃ c, c ≤ a ∧ c ≤ b :=
-- or
lemma exists_ge_ge [has_le α] [is_directed α (≤)] (a b : α) : ∃ c, a ≤ c ∧ b ≤ c :=
lemma exists_le_le [has_le α] [is_directed α (≥)] (a b : α) : ∃ c, c ≤ a ∧ c ≤ b :=