chore(order/{rel_iso, directed}): monotone functions and rel_homs are directed #7163
Conversation
eric-wieser
commented
Apr 11, 2021
eric-wieser
commented
eric-wieser
added
the
awaiting-review
eric-wieser
changed the title
src/order/directed.lean
Outdated
| instance semilattice_sup.to_directed_order (α) [semilattice_sup α] : directed_order α := | ||
| ⟨λ i j, ⟨i ⊔ j, le_sup_left, le_sup_right⟩⟩ | ||
|
|
||
| /-- A monotone function on a directed order (aka a sup-semilattice) is directed. -/ |
There was a problem hiding this comment.
I think this description is a little misleading in that it says directed orders are also known as sup-semilattices: perhaps better phrasing would be "on a directed order (in particular a sup-semilattice) is".
There was a problem hiding this comment.
I guess I was trying to hand-wave over the asymmetry with the _inf version below. I'm not really convinced directed_order is useful, since it's really just semilattice_sup with a non-computable sup
There was a problem hiding this comment.
Directed orders are very useful! And they're very different from just semilattice_sup: in particular in a directed order there's no guarantee that the given element is a supremum of the two given elements (ie sup_le might not hold), see eg here.
There was a problem hiding this comment.
Well, I'd argue they can't be that useful because mathlib has no instances of them that aren't linear orders so far!
There was a problem hiding this comment.
But thanks for clearing that up, I was missing the requirement for uniqueness.
src/order/directed.lean
Outdated
| /-- A `preorder` is a `directed_order` if for any two elements `i`, `j` | ||
| there is an element `k` such that `i ≤ k` and `j ≤ k`. -/ | ||
| class directed_order (α : Type u) extends preorder α := | ||
| (directed : ∀ i j : α, ∃ k, i ≤ k ∧ j ≤ k) | ||
|
|
||
| /-- A `preorder` is a `anti_directed_order` if for any two elements `i`, `j` | ||
| there is an element `k` such that `k ≤ i` and `k ≤ j`. -/ | ||
| class anti_directed_order (α : Type u) extends preorder α := | ||
| (directed : ∀ i j : α, ∃ k, k ≤ i ∧ k ≤ j) |
There was a problem hiding this comment.
@b-mehta, does this terminology seem ok to you? "upward-directed" and "downward-directed" are another option for the two names, or perhaps even sup_directed and inf_directed?
There was a problem hiding this comment.
I think your alternatives are slightly nicer but there's nothing wrong with the original - perhaps ask on Zulip? As long as the names aren't misleading I'm probably pretty happy with whatever you pick.
github-actions
bot
added
the
merge-conflict
…d-monotone # Conflicts: # src/order/directed.lean
eric-wieser
force-pushed
the
eric-wieser/directed-monotone
branch
from
8c9c842
to
5dd08f0
Compare
github-actions
bot
removed
the
merge-conflict
Vierkantor
added
awaiting-author
|
I'm not sure I can - I think they're caused by the introduction of the new typeclasses. |
github-actions
bot
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
github-actions
bot
added
the
merge-conflict
|
For obscure reasons, inserting As future work, we might want to add |
