Zulip Chat Archive

Stream: maths

Topic: Order reversing iso


view this post on Zulip Yakov Pechersky (Jan 08 2021 at 02:37):

Do we have a α ≃ order_dual α? Or the idea of a reversing order_iso?

view this post on Zulip Bryan Gin-ge Chen (Jan 08 2021 at 02:41):

docs#order_dual.to_dual has type α ≃ order_dual α.

view this post on Zulip Yakov Pechersky (Jan 08 2021 at 02:49):

But is there a proof that that takes \bot to \top?

view this post on Zulip Reid Barton (Jan 08 2021 at 02:49):

Probably rfl?

view this post on Zulip Yakov Pechersky (Jan 08 2021 at 03:12):

I guess my question is, how is it that the \bot portion of the following works, but not the \top? And am I just misusing order_dual here?

import data.fin
import order.order_dual

variable {n : }

open fin

@[simp] lemma bot_eq_zero : ( : fin (n + 1)) = 0 := rfl

@[simp] lemma top_eq_last : ( : fin (n + 1)) = last n := rfl

lemma dual_bot_eq_top {α : Type*} [bounded_lattice α] (x : α) (y : order_dual α)
  (hx : x = ) (hy : y = ) : order_dual.to_dual x = y :=
by { rw [hx, hy], refl }

/-- The isomorphism reversing the order on `fin n`. -/
def invert_iso : fin n  (fin n) := order_dual.to_dual

lemma invert_iso_zero : invert_iso (0 : fin (n + 1)) = last n :=
begin
  cases n,
  { refl },
  { rw invert_iso,
    rw dual_bot_eq_top,
    { exact bot_eq_zero },
    { symmetry,
      convert top_eq_last,
      sorry } }
end

view this post on Zulip Reid Barton (Jan 08 2021 at 03:26):

invert_iso is the identity so the lemma is false for n > 0

view this post on Zulip Reid Barton (Jan 08 2021 at 03:26):

of course most orders are not order isomorphic to their opposite orders

view this post on Zulip Reid Barton (Jan 08 2021 at 03:28):

order_dual.to_dual is just equiv.refl

view this post on Zulip Yakov Pechersky (Jan 08 2021 at 03:31):

Right, ok, makes sense. But since we have an order_iso, shouldn't we be able to use that to generate the reversing one? Or does that require an explicit construction?

view this post on Zulip Reid Barton (Jan 08 2021 at 03:33):

It needs a construction, it's entirely specific to fin

view this post on Zulip Reid Barton (Jan 08 2021 at 03:33):

or at least to finite total orders (which are all essentially fin)

view this post on Zulip Mario Carneiro (Jan 08 2021 at 03:37):

I don't think we have an order_iso on fin n

view this post on Zulip Mario Carneiro (Jan 08 2021 at 03:38):

I could imagine having a typeclass for symmetric orders, although I have no idea how important they are

view this post on Zulip Mario Carneiro (Jan 08 2021 at 03:40):

(also such an isomorphism is very often not unique even when it exists, as in int)

view this post on Zulip Yakov Pechersky (Jan 08 2021 at 05:07):

We have docs#fin.order_iso_unique

view this post on Zulip Yakov Pechersky (Jan 08 2021 at 05:07):

And of course, that order_iso is fin.cast rfl

view this post on Zulip Thomas Browning (Jan 08 2021 at 05:09):

When stating the Galois correspondence, we wrote it as a ≃ order_dual b

view this post on Zulip Thomas Browning (Jan 08 2021 at 05:09):

(we couldn't find a better option)

view this post on Zulip Yakov Pechersky (Jan 08 2021 at 05:10):

data/zmod/basic defines a has_neg on fin n and I am thinking it should be moved into a data/fin and a special locale

view this post on Zulip Mario Carneiro (Jan 08 2021 at 05:10):

@Yakov Pechersky I mean an order_iso between fin and it's dual

view this post on Zulip Mario Carneiro (Jan 08 2021 at 05:11):

which should be \lam i : fin (n+1), n - i

view this post on Zulip Mario Carneiro (Jan 08 2021 at 05:11):

and the empty function on fin 0

view this post on Zulip Yakov Pechersky (Jan 08 2021 at 05:11):

And was hoping to just use some neat way of flipping the order_iso. Yeah it's just that -- not sure why the zmod defn goes all the way through nat_mod on int coercions

view this post on Zulip Mario Carneiro (Jan 08 2021 at 05:12):

Note that zmod negation is not correct, because -0 = 0

view this post on Zulip Mario Carneiro (Jan 08 2021 at 05:12):

I mean it's correct as negation but not as the order dual isomorphism

view this post on Zulip Mario Carneiro (Jan 08 2021 at 05:14):

I don't think it would be a good idea to register this function as has_neg (fin n) because it doesn't match the zmod negation or make sense with addition

view this post on Zulip Yakov Pechersky (Jan 08 2021 at 05:17):

Is there a different comm_ring possible on fin (n + 1) other than the one defined in data/basic/zmod?

view this post on Zulip Aaron Anderson (Jan 08 2021 at 05:39):

Mario Carneiro said:

I could imagine having a typeclass for symmetric orders, although I have no idea how important they are

Basically boolean algebras where compl is surjective?

view this post on Zulip Mario Carneiro (Jan 08 2021 at 19:30):

@Aaron Anderson A boolean algebra would be an example of a "symmetric preorder", but there are many more examples. A boolean algebra needs a meet and join operation, but here we only need an order anti-automorphism

view this post on Zulip Mario Carneiro (Jan 08 2021 at 19:31):

(FYI compl is surjective in a boolean algebra because ~~a = a)

view this post on Zulip Reid Barton (Jan 08 2021 at 19:33):

I think fin n is not a boolean algebra for n >= 3, for example


Last updated: May 18 2021 at 06:15 UTC