## Stream: general

### Topic: preorder

#### 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?

#### 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...

#### Kevin Buzzard (Sep 03 2018 at 10:26):

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

#### Johan Commelin (Sep 03 2018 at 10:28):

I think it was lower and upper?

#### Johan Commelin (Sep 03 2018 at 10:29):

But also left and underlying...

#### 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)

#### 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

#### 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