Modular Lattices #
This file defines Modular Lattices, a kind of lattice useful in algebra. For examples, look to the subobject lattices of abelian groups, submodules, and ideals, or consider any distributive lattice.
Main Definitions #
is_modular_latticedefines a modular lattice to be one such that
x ≤ z → (x ⊔ y) ⊓ z ≤ x ⊔ (y ⊓ z)
inf_Icc_order_iso_Icc_supgives an order isomorphism between the intervals
[a ⊓ b, a]and
[b, a ⊔ b]. This corresponds to the diamond (or second) isomorphism theorems of algebra.
Main Results #
is_modular_lattice_iff_inf_sup_inf_assoc: Modularity is equivalent to the
(x ⊓ z) ⊔ (y ⊓ z) = ((x ⊓ z) ⊔ y) ⊓ z
distrib_lattice.is_modular_lattice: Distributive lattices are modular.
To do #
- Relate atoms and coatoms in modular lattices
A modular lattice is one with a limited associativity between
The diamond isomorphism between the intervals
[a ⊓ b, a] and
[b, a ⊔ b]