# Zulip Chat Archive

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

gives 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

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

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

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

Isn't this exactly related to https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/stacks.20project.20.2F.20schemes/near/123090992

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