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
u in the Galois connection stuff?
r I would understand...
Kevin Buzzard (Sep 03 2018 at 10:26):
r:(scoped f, supr f) := r mean?
Johan Commelin (Sep 03 2018 at 10:28):
I think it was
Johan Commelin (Sep 03 2018 at 10:29):
Johannes Hölzl (Sep 03 2018 at 10:41):
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.
(⨆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