Subtypes for provably equal sets

Stream: new members

[Heather Macbeth]

I would like to identify the subtypes coming from two sets which I can prove are equal:

import order.filter.at_top_bot
variables {α : Type*} [decidable_linear_order α]

open set filter

-- works
example {a b : α} : @Ioo (order_dual α) _ b a = @Ioo α _ a b := dual_Ioo

-- fails
example {a b : α} : @at_bot (Ioo a b) _ = @at_top (@Ioo (order_dual α) _ b a) _ := sorry

I get the following error: "type mismatch at application at_bot = at_top, term at_top has type filter ↥(Ioo b a) but is expected to have type filter ↥(Ioo a b)".

This makes sense, but how do I fix it? (Is this similar to the questions @Peter Nelson was asking the other day?)

[Kevin Buzzard]

You can prove the sets are equal, but equality of types is an unpleasant notion. One way of "fixing" it would be to give a name to the "identity" map between the types, and then compare one filter with the pullback of the other.

[Heather Macbeth]

Thanks! This typechecks, is it what you had in mind?

import order.filter.at_top_bot
variables {α : Type*} [decidable_linear_order α]

open set filter

def order_id (a b : α) : @Ioo (order_dual α) _ b a → @Ioo α _ a b :=
λ x, ⟨(x : order_dual α), begin
  have : @Ioo (order_dual α) _ b a = @Ioo α _ a b := dual_Ioo,
  rw ← this,
  exact x.2,
end⟩

example {a b : α} :
  comap (order_id a b) (@at_bot (@Ioo α _ a b) _) = @at_top (@Ioo (order_dual α) _ b a) _ :=
sorry

[Kevin Buzzard]

Yes! Here's my definition of order_id:

variables (a b : α)

def X := @Ioo α _ a b
def Y := @Ioo (order_dual α) _ b a

def to_dual : α → order_dual α := id -- do we have this map?

def f : X a b → Y a b := λ x, ⟨to_dual x.1, x.2.2, x.2.1⟩

[Heather Macbeth]

Looks great. Have to go teach now, but I look forward to filling in my sorry using this trick.

[Kevin Buzzard]

In Lean we have groups and add_groups, and sometimes this is great and sometimes it's not great. There is this to_additive story, which moves from one situation to the other: if (G : Type) [group G] then additive G is the add_group with group law + which is defined to be G's *. But the definition of additive G is just additive G := G. Similarly if A is an add_group then multiplicative A is the group. There are named maps called things like additive.of_multiplicative or something, which move you between these two structures -- this is why I defined to_dual. However some proofs in mathlib completely abuse the fact that these maps from G to additive G are just the identity function. This might work fine for groups, but you're doing the dual order and here what is a bit scary is that you will now have < on alpha and a different < on order_dual alpha and if you are not principled about these things then it will be easy to get confused. It is not hard to get Lean to accept "theoretically ill-defined" terms, e.g. of the form "x < y" where x : alpha and y : order_dual alpha, and then you can't guess what < will mean (and in the days before widgets this was a royal pain). So I guess I would recommend the principled approach, using to_dual rather than "abusing" the fact that order_dual α := α.

[Kevin Buzzard]

I should say however that this idea of defining to_dual is my own crazy notion and it's not already in mathlib which might mean that it's for some reason a bad idea.

[Reid Barton]

For opposite categories (which are basically the same thing) we have docs#opposite which is an even more locked down version of this. Your to_dual is called op

[Kevin Buzzard]

@[irreducible]
def opposite : Sort u → Sort u :=
λ (α : Sort u), α

Because it's irreducible, it's much easier to be principled about these things. I made with_zero and with_one irreducible recently because it stopped the simplifier simplifying x : with_zero X to x : option X, something which is sometimes a great idea but sometimes not so great (it's not the correct path to go down if you want to actually use properties of zero which none doesn't have).

[Heather Macbeth]

Reid, was your comment intended as something that is ready-to-go on current mathlib, or something that would be nice to add? I just tried taking it literally, by trying to write

import order.filter.at_top_bot
variables {α : Type*} [decidable_linear_order α]

open opposite

example : (order_dual α) → α := @unop α

but it seems that αᵒᵖ and order_dual α are not the same thing on current mathlib (I get "type mismatch, term unop has type αᵒᵖ → α but is expected to have type order_dual α → α", unsurprisingly)

[Reid Barton]

Right, opposite and order_dual are not the same (though perhaps the opposite for categories should unmerge somehow with the opposite for *, and merge with order_dual instead).

[Heather Macbeth]

Do you happen to know if there is an analogue of the map op in the order_dual situation? I checked the library but didn't see it.

[Reid Barton]

I don't know--my guess is if you didn't find it then it doesn't exist.