Zulip Chat Archive

Stream: maths

Topic: lattice with antiautomorphism


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 28 2020 at 17:36):

There is lattice.copy, and all its cousins.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 28 2020 at 17:55):

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

view this post on Zulip Chris Hughes (Mar 28 2020 at 17:55):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 17:56):

Galois connection: that is an interesting idea!

view this post on Zulip 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

view this post on Zulip 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)?

view this post on Zulip 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)

view this post on Zulip Chris Hughes (Mar 28 2020 at 22:35):

I think we need the other way round here

view this post on Zulip Mario Carneiro (Mar 28 2020 at 22:36):

oh yes you are right

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 00:04):

But this doesn't solve the problem right?

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 00:05):

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

view this post on Zulip Chris Hughes (Mar 29 2020 at 00:12):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Chris Hughes (Mar 29 2020 at 00:22):

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

view this post on Zulip Chris Hughes (Mar 29 2020 at 00:22):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 00:56):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 29 2020 at 01:04):

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

view this post on Zulip Mario Carneiro (Mar 29 2020 at 01:04):

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

view this post on Zulip Mario Carneiro (Mar 29 2020 at 01:05):

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

view this post on Zulip Mario Carneiro (Mar 29 2020 at 01:06):

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

view this post on Zulip 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) _

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 31 2020 at 13:09):

Interesting!


Last updated: May 12 2021 at 08:14 UTC