Lattice Homomorphisms?

Stream: Is there code for X?

[Reed Mullanix]

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

[Aaron Anderson]

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

[Aaron Anderson]

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]

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]

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

[Johan Commelin]

Note that there is in fact preorder_hom

[Johan Commelin]

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

[Bryan Gin-ge Chen]

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

Yes please, I'd like them too!

[Scott Morrison]

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

[Bryan Gin-ge Chen]

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

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

[Eric Wieser]

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]

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]

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]

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]

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]

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

[Aaron Anderson]

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]

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