Zulip Chat Archive

Stream: new members

Topic: order_iso woes


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 06:22):

This is a job for @Kenny Lau

view this post on Zulip Mario Carneiro (Oct 10 2018 at 06:25):

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

view this post on Zulip Kenny Lau (Oct 10 2018 at 07:56):

This is ridiculous.

view this post on Zulip Kenny Lau (Oct 10 2018 at 07:56):

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

view this post on Zulip Kenny Lau (Oct 10 2018 at 07:56):

game: spot the error

view this post on Zulip Mario Carneiro (Oct 10 2018 at 07:58):

no error?

view this post on Zulip Kenny Lau (Oct 10 2018 at 08:01):

even Mario missed it

view this post on Zulip Kenny Lau (Oct 10 2018 at 08:01):

the correct declaration should be

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 08:04):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 10 2018 at 08:05):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 08:06):

Oh, I missed the context

view this post on Zulip Mario Carneiro (Oct 10 2018 at 08:06):

I thought you meant those variables don't typecheck

view this post on Zulip Mario Carneiro (Oct 10 2018 at 08:07):

are you saying that this is in mathlib?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 10 2018 at 08:09):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 08:09):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 08:09):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 10 2018 at 08:10):

that's where the fun is

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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