Zulip Chat Archive

Stream: Is there code for X?

Topic: Lattice Homomorphisms?


view this post on Zulip Reed Mullanix (Sep 13 2020 at 15:44):

I'm working on some point-free topology, and was struggling to find a notion of a lattice homomorphism anywhere.

view this post on Zulip Aaron Anderson (Sep 13 2020 at 18:52):

The file order/rel_iso.lean has everything relevant that we have

view this post on Zulip Aaron Anderson (Sep 13 2020 at 18:55):

In short, we have order embeddings and order isomorphisms, and we know how those relate to lattices, and a general relation homomorphism that generalizes monotone maps, but we don’t have a dedicated type for maps that may not be embeddings/isos but do preserve all lattice operations.

view this post on Zulip Aaron Anderson (Sep 13 2020 at 19:02):

I don’t know your background, but if you’re looking for a place to start/first PR, studying that file and writing a definition of lattice homomorphism seems to me like a decent place to start

view this post on Zulip Reed Mullanix (Sep 13 2020 at 20:10):

I'll probably pester you all with some more silly questions, but I'll give that a go later today :)

view this post on Zulip Johan Commelin (Sep 14 2020 at 08:38):

Note that there is in fact preorder_hom

view this post on Zulip Johan Commelin (Sep 14 2020 at 08:38):

@Reed Mullanix @Aaron Anderson see order/preorder_hom.lean

view this post on Zulip Bryan Gin-ge Chen (Mar 13 2021 at 15:02):

@Reed Mullanix did you ever make any progress with lattice homomorphisms? I think we'll be wanting them soon, as @Noam Atar has been defining properties of order ideals.

view this post on Zulip Scott Morrison (Mar 13 2021 at 22:21):

Yes please, I'd like them too!

view this post on Zulip Scott Morrison (Mar 13 2021 at 22:21):

Do we have bundled sublattices? (Like subsemiring and friends.) They would be nice too.

view this post on Zulip Bryan Gin-ge Chen (Mar 13 2021 at 22:51):

@Scott Morrison No, we don't have those either yet. Imitating the algebraic hierarchy around subsemiring, ring_hom, etc. would be a good way to start, right?

view this post on Zulip Scott Morrison (Mar 13 2021 at 22:58):

Yes. On the other hand it's starting to look pretty creaky to have to do this by hand again.

view this post on Zulip Eric Wieser (Mar 14 2021 at 00:06):

I think mathlib is in dire need of a "subobject" generator that takes a list of "closure under" axioms and builds the 200 or so lines of boilerplate

view this post on Zulip Eric Wieser (Mar 14 2021 at 00:07):

I know one of @Kevin Buzzard's students was going to start looking at sets closed under +, -, and smul that contain 0 recently - which is basically submodule but extending subgroup instead of submonoid and without a ring assumption that makes the - irrelevant. The number of the subobjects that can exist is exponential in the number of operators, which feels really bad.

view this post on Zulip Aaron Anderson (Mar 14 2021 at 03:56):

A lot of the API can come from the fact that closure is a Galois Insertion representing a finitary closure operator, I think this might get us a lot of the way there

view this post on Zulip Bryan Gin-ge Chen (Mar 14 2021 at 05:52):

Aaron Anderson said:

A lot of the API can come from the fact that closure is a Galois Insertion representing a finitary closure operator, I think this might get us a lot of the way there

I'd love to see how this works, if you wouldn't mind sketching some of this out.

view this post on Zulip Kevin Buzzard (Mar 14 2021 at 08:37):

That's normally the quickest way to get to the sublattice I think. Here this would involve defining the G-invariant-subgroup-closure of either a subgroup or a G-invariant subset (note that the definition of G-invariant subgroup is just to switch on the old structure command and then extend sub_mul_action and subgroup, so the game seems to be that you have to make it back to one of the things you extended). You can either do it with an inductive prop or prove closed under arbitrary intersections first and use this. Then you prove enough about it to be able to use the theorem which pulls back complete lattice structures along Galois insertions. Then I still want "kernel and range of a G-module map are G-submodules" and a map and comap which are also a Galois connection

view this post on Zulip Kevin Buzzard (Mar 14 2021 at 08:49):

It's all a great exercise for a beginner by the way

view this post on Zulip Aaron Anderson (Mar 14 2021 at 16:25):

Or we could define lattices as substructures of lattices in a given first-order language, and just prove that boilerplate once more for substructures

view this post on Zulip Bhavik Mehta (Apr 30 2021 at 14:50):

Is there any progress on this? I'd like to try getting to things like Stone duality for profinite sets, so some notions of lattice homomorphisms would be helpful


Last updated: May 17 2021 at 16:26 UTC