mathlib documentation

order.modular_lattice

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 #

Main Results #

To do #

@[class]
structure is_modular_lattice (α : Type u_2) [lattice α] :
Prop
  • sup_inf_le_assoc_of_le : ∀ {x : α} (y : α) {z : α}, x z(x y) z x y z

A modular lattice is one with a limited associativity between and .

Instances
theorem sup_inf_assoc_of_le {α : Type u_1} [lattice α] [is_modular_lattice α] {x : α} (y : α) {z : α} (h : x z) :
(x y) z = x y z
theorem is_modular_lattice.inf_sup_inf_assoc {α : Type u_1} [lattice α] [is_modular_lattice α] {x y z : α} :
x z y z = (x z y) z
theorem inf_sup_assoc_of_le {α : Type u_1} [lattice α] [is_modular_lattice α] {x : α} (y : α) {z : α} (h : z x) :
x y z = x (y z)
theorem is_modular_lattice.sup_inf_sup_assoc {α : Type u_1} [lattice α] [is_modular_lattice α] {x y z : α} :
(x z) (y z) = (x z) y z
def inf_Icc_order_iso_Icc_sup {α : Type u_1} [lattice α] [is_modular_lattice α] (a b : α) :
(set.Icc (a b) a) ≃o (set.Icc b (a b))

The diamond isomorphism between the intervals [a ⊓ b, a] and [b, a ⊔ b]

Equations
def is_compl.Iic_order_iso_Ici {α : Type u_1} [bounded_lattice α] [is_modular_lattice α] {a b : α} (h : is_compl a b) :

The diamond isomorphism between the intervals set.Iic a and set.Ici b.

Equations
theorem is_modular_lattice_iff_inf_sup_inf_assoc {α : Type u_1} [lattice α] :
is_modular_lattice α ∀ (x y z : α), x z y z = (x z y) z
theorem disjoint.disjoint_sup_right_of_disjoint_sup_left {α : Type u_1} [bounded_lattice α] [is_modular_lattice α] {a b c : α} (h : disjoint a b) (hsup : disjoint (a b) c) :
disjoint a (b c)
theorem disjoint.disjoint_sup_left_of_disjoint_sup_right {α : Type u_1} [bounded_lattice α] [is_modular_lattice α] {a b c : α} (h : disjoint b c) (hsup : disjoint a (b c)) :
disjoint (a b) c