Zulip Chat Archive

Stream: new members

Topic: Subtypes for provably equal sets


view this post on Zulip Heather Macbeth (Sep 04 2020 at 16:30):

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

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 16:38):

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.

view this post on Zulip Heather Macbeth (Sep 04 2020 at 16:45):

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

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 16:45):

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

view this post on Zulip Heather Macbeth (Sep 04 2020 at 16:47):

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

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 16:53):

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 α := α.

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 17:04):

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.

view this post on Zulip Reid Barton (Sep 04 2020 at 17:07):

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

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 17:09):

@[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).

view this post on Zulip Heather Macbeth (Sep 04 2020 at 19:05):

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)

view this post on Zulip Reid Barton (Sep 04 2020 at 19:10):

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).

view this post on Zulip Heather Macbeth (Sep 04 2020 at 19:18):

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.

view this post on Zulip Reid Barton (Sep 04 2020 at 19:44):

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


Last updated: May 14 2021 at 07:19 UTC