## Stream: new members

### Topic: order_iso woes

#### Bryan Gin-ge Chen (Oct 10 2018 at 01:55):

I'm trying to generalize this function (there's a typo, that should be a def not a lemma; nonetheless it works...). I want to prove that an order_isogives rise to a galois_insertion but I'm stuck on what seems to me to be simple:

import order.galois_connection order.order_iso

namespace order_iso
variables {β : Type*} {γ : Type*} [preorder β] [preorder γ]
{r : β → β → Prop} {s : γ → γ → Prop} (oi : order_iso r s)

set_option pp.implicit true

theorem to_galois_connection :
galois_connection (oi.to_fun) (oi.inv_fun) :=
by unfold galois_connection;
exact λ {b g}, calc (oi.to_fun b) ≤ g ↔
(oi.to_fun b) ≤ (oi.to_fun (oi.inv_fun g)) : by rw oi.right_inv
... ↔ b ≤ (oi.inv_fun g) : by { -- rw oi.ord
have : r b (oi.inv_fun g) ↔
s (oi.to_fun b) (oi.to_fun (oi.inv_fun g)) := (@order_iso.ord β γ r s oi b (oi.inv_fun g)),
change oi.to_fun b ≤ oi.to_fun (oi.inv_fun g) ↔ b ≤ oi.inv_fun g,
sorry }

protected def to_galois_insertion [preorder β] [preorder γ] : @galois_insertion β γ _ _
(oi.to_fun) (oi.inv_fun) :=
{ choice := λ b h, oi.to_fun b,
gc := to_galois_connection oi,
le_l_u := λ g, le_of_eq (oi.right_inv g).symm,
choice_eq := λ b h, rfl }

end order_iso


In the tactic state near where I gave up, the only difference I see between the goal and this is that the goal uses ≤ and this uses r and s.

#### Kevin Buzzard (Oct 10 2018 at 06:22):

This is a job for @Kenny Lau

#### Mario Carneiro (Oct 10 2018 at 06:25):

You should be able to use function coercion instead of to_fun and inv_fun everywhere

#### Kenny Lau (Oct 10 2018 at 07:56):

This is ridiculous.

#### Kenny Lau (Oct 10 2018 at 07:56):

variables {β : Type*} {γ : Type*} [preorder β] [preorder γ]
{r : β → β → Prop} {s : γ → γ → Prop} (oi : order_iso r s)


#### Kenny Lau (Oct 10 2018 at 07:56):

game: spot the error

no error?

#### Kenny Lau (Oct 10 2018 at 08:01):

even Mario missed it

#### Kenny Lau (Oct 10 2018 at 08:01):

the correct declaration should be

variables {β : Type*} {γ : Type*} [preorder β] [preorder γ]
(oi : @order_iso β γ (≤) (≤))


#### Johan Commelin (Oct 10 2018 at 08:04):

In particular, this means that order_iso is not what we want it to be.

#### Kenny Lau (Oct 10 2018 at 08:04):

import order.galois_connection order.order_iso

namespace order_iso
variables {β : Type*} {γ : Type*} [preorder β] [preorder γ]
(oi : @order_iso β γ (≤) (≤))

theorem to_galois_connection : galois_connection oi oi.symm :=
λ b g, by rw [ord' oi, apply_inverse_apply]

protected def to_galois_insertion :
@galois_insertion β γ _ _ oi oi.symm :=
{ choice := λ b h, oi b,
gc := to_galois_connection oi,
le_l_u := λ g, le_of_eq (oi.right_inv g).symm,
choice_eq := λ b h, rfl }

end order_iso


#### Kenny Lau (Oct 10 2018 at 08:05):

@Mario Carneiro how many of this error do you think are in mathlib?

#### Mario Carneiro (Oct 10 2018 at 08:06):

Oh, I missed the context

#### Mario Carneiro (Oct 10 2018 at 08:06):

I thought you meant those variables don't typecheck

#### Mario Carneiro (Oct 10 2018 at 08:07):

are you saying that this is in mathlib?

#### Mario Carneiro (Oct 10 2018 at 08:08):

I guess there is a tension here between order_iso, which works with explicit relations, and galois_connection, which works with types with a preorder instance

#### Kenny Lau (Oct 10 2018 at 08:09):

I'm saying that there are errors like this in mathlib

#### Mario Carneiro (Oct 10 2018 at 08:09):

I'm sure there are, but someone has to notice them first

#### Mario Carneiro (Oct 10 2018 at 08:09):

if no one notices them then they aren't doing anyone harm

#### Johan Commelin (Oct 10 2018 at 08:10):

if no one notices them then they aren't doing anyone harm

Except that you might think you have formalised something, but it turns out to be something else.

#### Mario Carneiro (Oct 10 2018 at 08:10):

that's where the fun is

#### Kevin Buzzard (Oct 10 2018 at 09:20):

@Kenny Lau , now all the people who bothered to click and investigate are in on the joke, can you paste one line of explanation for those of us that are so busy preparing 1st year lectures that we don't even understand the issue at hand here and would hence prefer it if your comments were less cryptic?

#### Kenny Lau (Oct 10 2018 at 10:07):

@Kevin Buzzard basically there are two orders on each type when there should only be one order

#### Bryan Gin-ge Chen (Oct 10 2018 at 13:40):

Thanks Kenny! I'm glad it turned out to be something simple.

Last updated: May 12 2021 at 22:15 UTC