# Zulip Chat Archive

## Stream: maths

### Topic: lattice with antiautomorphism

#### Kevin Buzzard (Mar 28 2020 at 17:20):

In this piece of code there's a lattice where inf is much easier to work with than sup. I defined inf and proved all the theorems to make a `semilattice_inf_bot`

. I now wanted a `semilattice_sup_top`

and I claim that I should be able to get it for free by applying an `inv`

function to everything, e.g. `E ⊔ F = (F⁻¹ ⊓ E⁻¹)⁻¹`

and so on (maybe I don't want this to be the definition of sup, but I want to prove this theorem about sup, and once I've proved it and that the inverse of top is bot, I want everything else for free). What is happening here? Is this some kind of `to_additive`

on steroids?

#### Johan Commelin (Mar 28 2020 at 17:36):

There is `lattice.copy`

, and all its cousins.

#### Johan Commelin (Mar 28 2020 at 17:37):

That allows you to take a lattice structure with ugly definitions, and replace them with good definitions, but maintain all the proofs.

#### Kevin Buzzard (Mar 28 2020 at 17:54):

What's happening here is that I prove all the theorems about inf and top, but I don't want to prove any of the theorems about sup and bot because they all follow from the theorems about inf and top when I apply the involution.

#### Johan Commelin (Mar 28 2020 at 17:55):

Maybe not all the machinery for transporting half of the structure across that involution is there.

#### Chris Hughes (Mar 28 2020 at 17:55):

Can you do a galois connection with the dual to get `semilattice_sup_top`

somehow?

#### Kevin Buzzard (Mar 28 2020 at 17:56):

However I was forced to prove them because I didn't know any automation which would do them, and asking `simp`

to do it is I think too tall an order. You apply le_of_inv_ge_inv or eq_of_inv_eq_inv to everything and then apply the corresponding "dual" lemma, with the occasional inv_inv thrown in

#### Kevin Buzzard (Mar 28 2020 at 17:56):

Galois connection: that is an interesting idea!

#### Kevin Buzzard (Mar 28 2020 at 18:42):

I think I simply need that if `L ≃ M`

is <=-reversing then I can transfer an inf_bot on L to a sup_top on M

#### Mario Carneiro (Mar 28 2020 at 22:35):

Do we have the theorem that says that `semilattice_inf_bot X -> semilattice_sup_top (dual X)`

?

#### Mario Carneiro (Mar 28 2020 at 22:35):

If so, you should be able to apply it and then use `change`

to fix up all the operations (the inverse function is not necessary)

#### Chris Hughes (Mar 28 2020 at 22:35):

I think we need the other way round here

#### Mario Carneiro (Mar 28 2020 at 22:36):

oh yes you are right

#### Kevin Buzzard (Mar 29 2020 at 00:04):

But this doesn't solve the problem right?

#### Kevin Buzzard (Mar 29 2020 at 00:05):

I now need to transport the typeclass along the isomorphism between the lattice and its dual

#### Chris Hughes (Mar 29 2020 at 00:12):

Yeah, you have to do that. But you can do that once in great generality.

#### Chris Hughes (Mar 29 2020 at 00:13):

So you haven't saved yourself much work, but you've saved the next person some work.

#### Kevin Buzzard (Mar 29 2020 at 00:16):

But I thought we're supposed to doing this with the transfer tactic which didn't get written yet? I'm supposed to be giving a talk on this on Wednesday

#### Chris Hughes (Mar 29 2020 at 00:22):

I'm not sure the transfer tactic will do that.

#### Chris Hughes (Mar 29 2020 at 00:22):

This doesn't feel like that, because the structures are different.

#### Kevin Buzzard (Mar 29 2020 at 00:55):

I mean after getting the suptop on the dual of L from the infbot on L, I then need to get a suptop on L from the suptop on the dual of L by transporting it along the isomorphism I have between L and its dual given by inv

#### Kevin Buzzard (Mar 29 2020 at 00:56):

In my situation I have an isomorphism inv between L and its dual

#### Kevin Buzzard (Mar 29 2020 at 00:58):

So I want to do only half the work for proving L is a bounded lattice. Other than the partial order it seems to be that the inf top structure and the sup bot structure are completely disjoint and dual in some way

#### Chris Hughes (Mar 29 2020 at 01:02):

But that's a theorem that isn't inside the realm of transfer I think. Even though it's an easy tedious theorem. The fact that `sup`

is dual to `inf`

and so on.

#### Mario Carneiro (Mar 29 2020 at 01:04):

I'm confused. The transfer tactic is not needed here

#### Mario Carneiro (Mar 29 2020 at 01:04):

There is a theorem, proven once, that `semilattice_sup_top X -> semilattice_inf_bot (dual X)`

#### Mario Carneiro (Mar 29 2020 at 01:05):

there is no automation involved in this theorem, you just unfold and apply the projections

#### Mario Carneiro (Mar 29 2020 at 01:06):

This is analogous to the theorem `group G -> add_group (additive G)`

#### Mario Carneiro (Mar 29 2020 at 01:07):

Once that is set up, a statement like `\forall x y : X, x \cap y = y \cap x`

can be proven by `@sup_comm (dual X) _`

#### Kevin Buzzard (Mar 29 2020 at 01:10):

In my situation I have an inf_bot on L. I want a sup_top on L. The theorem above, proven once, will give me a sup_top on dual(L). Now how do I get the sup_top on L? Answer: use `inv`

, the isomorphism between L and dual(L). But now I need transfer, right? What am I missing?

#### Scott Morrison (Mar 31 2020 at 13:00):

@Kevin Buzzard, sorry this answer is two days late, but we are on the verge of having this. From the `transport`

branch, for which there is an open PR #2251:

-- We verify that `transport` can move a `semiring` across an equivalence. -- Note that we've never even mentioned the idea of addition or multiplication to `transport`. def semiring.map {α : Type} [semiring α] {β : Type} (e : α ≃ β) : semiring β := by transport. -- Indeed, it can equally well move a `semilattice_sup_top`. def sup_top.map {α : Type} [semilattice_sup_top α] {β : Type} (e : α ≃ β) : semilattice_sup_top β := by transport.

#### Kevin Buzzard (Mar 31 2020 at 13:09):

Interesting!

Last updated: May 12 2021 at 08:14 UTC