## Stream: maths

### Topic: Order reversing iso

#### Yakov Pechersky (Jan 08 2021 at 02:37):

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

#### Bryan Gin-ge Chen (Jan 08 2021 at 02:41):

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

#### Yakov Pechersky (Jan 08 2021 at 02:49):

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

#### Reid Barton (Jan 08 2021 at 02:49):

Probably rfl?

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


#### Reid Barton (Jan 08 2021 at 03:26):

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

#### Reid Barton (Jan 08 2021 at 03:26):

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

#### Reid Barton (Jan 08 2021 at 03:28):

order_dual.to_dual is just equiv.refl

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

#### Reid Barton (Jan 08 2021 at 03:33):

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

#### Reid Barton (Jan 08 2021 at 03:33):

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

#### Mario Carneiro (Jan 08 2021 at 03:37):

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

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

#### Mario Carneiro (Jan 08 2021 at 03:40):

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

#### Yakov Pechersky (Jan 08 2021 at 05:07):

We have docs#fin.order_iso_unique

#### Yakov Pechersky (Jan 08 2021 at 05:07):

And of course, that order_iso is fin.cast rfl

#### Thomas Browning (Jan 08 2021 at 05:09):

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

#### Thomas Browning (Jan 08 2021 at 05:09):

(we couldn't find a better option)

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

#### Mario Carneiro (Jan 08 2021 at 05:10):

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

#### Mario Carneiro (Jan 08 2021 at 05:11):

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

#### Mario Carneiro (Jan 08 2021 at 05:11):

and the empty function on fin 0

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

#### Mario Carneiro (Jan 08 2021 at 05:12):

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

#### Mario Carneiro (Jan 08 2021 at 05:12):

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

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

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

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

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

#### Mario Carneiro (Jan 08 2021 at 19:31):

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

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