Zulip Chat Archive

Stream: general

Topic: preorder


view this post on Zulip Kevin Buzzard (Sep 03 2018 at 09:45):

class preorder (α : Type u) extends has_le α, has_lt α :=
(le_refl :  a : α, a  a)
(le_trans :  a b c : α, a  b  b  c  a  c)
(lt := λ a b, a  b  ¬ b  a)
(lt_iff_le_not_le :  a b : α, a < b  (a  b  ¬ b  a) . order_laws_tac)

I just want to check I've got this right. The lt field does not even seem to document its type, but given that we have an example of how to fill it in, we can infer the type. The lt_iff_le_not_le field demands that lt a b is logically equivalent to (a ≤ b ∧ ¬ b ≤ a), so from a mathematician's point of view it may as well be defined to be λ a b, a ≤ b ∧ ¬ b ≤ a. However from a computer scientist's point of view they might want some other algorithm for computing < and then a theorem saying it's equivalent. The order_laws_tac thing -- this is some tactic, which presumably is a beefed-up version of exact iff.refl. Mathematicians could hence simply completely ignore the last two fields when getting a feel as to what a preorder is (I am more used to partial orders). A preorder is just a category whose objects are terms of alpha and for which there is at most one morphism between any two objects; it's weaker than a partial order because there can be objects which are isomorphic but not equal. A Galois connection is no more and no less than a pair of adjoint functors between two such categories. Have I got all this straight?

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 10:21):

Why are the maps called l and u in the Galois connection stuff? l and r I would understand...

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 10:26):

What does notation binders , r:(scoped f, supr f) := r mean?

view this post on Zulip Johan Commelin (Sep 03 2018 at 10:28):

I think it was lower and upper?

view this post on Zulip Johan Commelin (Sep 03 2018 at 10:29):

But also left and underlying...

view this post on Zulip Johannes Hölzl (Sep 03 2018 at 10:41):

Yes l for lower, and u for upper. But left and underlying is also nice
I don't understand the notation-syntax myself. This specific case sets up to behave like a lambda, and put a supr around it.
I.e. (⨆a, f a) := supr (λa, f a)

view this post on Zulip Johannes Hölzl (Sep 03 2018 at 10:42):

That we want to overwrite < is not necessary due to more efficient computation, but sometimes also easier proofs. For example for nat it is defined to be a < b := nat.succ a <= b

view this post on Zulip Reid Barton (Sep 03 2018 at 11:22):

Kevin what you say is right. Also worth noting is that every preorder has a canonical equivalence (in the category theory sense) to a poset, so there's not much harm in treating posets and preorders as the same thing.


Last updated: May 17 2021 at 21:12 UTC