# Zulip Chat Archive

## Stream: new members

### Topic: Subtypes for provably equal sets

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

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

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

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

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

#### 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 α := α`

.

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

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

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

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

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

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

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