Modular Lattice

Stream: maths

[Aaron Anderson]

I'd like to define modular lattices (to talk about modules), and I'd like to know whether modular-ness should be a mixin. So far, everything to do with lattices (including the distrib_lattice property) includes a new lattice structure, except for the mixin I defined, is_simple_lattice.

[Aaron Anderson]

I’m thinking yes, it should be a mixin, unless there’s some more complicated notion of completely modular lattice, analogous to complete_distrib_lattice

[Aaron Anderson]

It appears there is such a notion, and it does look pretty fiddly... https://encyclopediaofmath.org/wiki/Complete_Dedekind_lattice

[Matt Insall]

Modular lattices form a variety, so you can define them using a set of equations. In fact, the book on universal algebra by Burris and Sankappannavar (among others) shows a single equation that characterizes all modular lattices. I'm new to lean, so I'm not sure what is a "mixin", and I don't know what you mean by a "new lattice structure", but my intuitive idea of what you mean is that you may be concerned about the language for these structures. To me the most natural language for lattices is the same as for modular lattices, just like for distributive lattices, so I tend to think "no". If I'm misunderstanding your question, please let me know, as I would like to learn more about this particular part of lean, since I have worked in lattice theory.

[Kevin Buzzard]

"mixin" is a technical thing we use in Lean in order to add axioms to structures in some cases. For example a commutative ring is an additive group and a multiplicative monoid together with some relation between + and *, namely distributivity. In Lean 3 there is a crazy object called a distrib which is just an object with a + and a * satisfying _only_ distributivity, and it's used in the definition of a ring.

[Bryan Gin-ge Chen]

Aaron's modular lattice PR: #5564. Comments and additional reviews welcome, particularly if you know the math!

[Aaron Anderson]

Bryan Gin-ge Chen said:

Aaron's modular lattice PR: #5564. Comments and additional reviews welcome, particularly if you know the math!

Thanks for linking

[Aaron Anderson]

Matt Insall said:

Modular lattices form a variety, so you can define them using a set of equations. In fact, the book on universal algebra by Burris and Sankappannavar (among others) shows a single equation that characterizes all modular lattices. I'm new to lean, so I'm not sure what is a "mixin", and I don't know what you mean by a "new lattice structure", but my intuitive idea of what you mean is that you may be concerned about the language for these structures. To me the most natural language for lattices is the same as for modular lattices, just like for distributive lattices, so I tend to think "no". If I'm misunderstanding your question, please let me know, as I would like to learn more about this particular part of lean, since I have worked in lattice theory.

Either way, it's going to start with the regular language for lattices. The question is whether the actual Lean code for introducing a modular lattice will look like [lattice α] [is_modular_lattice α] (the mixin, this is the version in my PR) or [modular_lattice α] (a whole other name, but still defines all the usual lattice operations on α.)

[Aaron Anderson]

It's probably worth mentioning that my PR on modular lattices is depending on another PR of mine on order theory, #5493 (although this is probably near the end of its reviewing process).

[Matt Insall]

Aaron, like I said I'm new to lean, and being not a programmer, I'm more comfortable with natural language instead of code, but from the little bit I gathered here, introducing something using "mixin" means that the resulting structure is an expansion of the original, or equivalently, that the original is a reduct of the result. That's not the case for modular lattices, so I don't see why using "mixin" would be efficient. Another way I could have said what I said before is that modular lattices form a subvariety of the variety of lattices.

On the other hand, bounded lattices do not form a subvariety of the variety of lattices, so in order to specify them, the philosophically nore cogent approach to introducing those lattices would to me include using "mixin", if I'm understanding that correctly, because a "lattice that has an element greater than all the others and has an element that is less than all of the others" is categorically distinct from a "bounded lattice", whose specification language needs two constant terms (one for the top element and another for the bottom element) not in the language for lattices, in order to see that bounded lattices form a variety, even though they don't form a subvariety of the variety of lattices.

I may be barking up the wrong tree here, but even in the informal literature, the notions this that I discuss above lead to confusion if not dealt with carefully.