## Stream: Is there code for X?

### Topic: Lattice Homomorphisms?

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

#### Aaron Anderson (Sep 13 2020 at 18:52):

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

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

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

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

#### Johan Commelin (Sep 14 2020 at 08:38):

Note that there is in fact preorder_hom

#### Johan Commelin (Sep 14 2020 at 08:38):

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

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

#### Scott Morrison (Mar 13 2021 at 22:21):

Yes please, I'd like them too!

#### Scott Morrison (Mar 13 2021 at 22:21):

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

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

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

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

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

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

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

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

#### Kevin Buzzard (Mar 14 2021 at 08:49):

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

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

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