lattice with antiautomorphism

Stream: maths

[Kevin Buzzard]

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]

There is lattice.copy, and all its cousins.

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Chris Hughes]

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

[Kevin Buzzard]

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]

Galois connection: that is an interesting idea!

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

I think we need the other way round here

[Mario Carneiro]

oh yes you are right

[Kevin Buzzard]

But this doesn't solve the problem right?

[Kevin Buzzard]

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

[Chris Hughes]

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

[Chris Hughes]

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

[Kevin Buzzard]

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]

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

[Chris Hughes]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

Interesting!