preorder

Stream: general

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

I think it was lower and upper?

[Johan Commelin]

But also left and underlying...

[Johannes Hölzl]

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]

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]

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.