Order reversing iso

Stream: maths

[Yakov Pechersky]

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

[Bryan Gin-ge Chen]

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

[Yakov Pechersky]

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

[Reid Barton]

Probably rfl?

[Yakov Pechersky]

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]

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

[Reid Barton]

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

[Reid Barton]

order_dual.to_dual is just equiv.refl

[Yakov Pechersky]

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]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yakov Pechersky]

We have docs#fin.order_iso_unique

[Yakov Pechersky]

And of course, that order_iso is fin.cast rfl

[Thomas Browning]

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

[Thomas Browning]

(we couldn't find a better option)

[Yakov Pechersky]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

and the empty function on fin 0

[Yakov Pechersky]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Aaron Anderson]

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]

@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]

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

[Reid Barton]

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