# Zulip Chat Archive

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