Modular Lattices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines (semi)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.

Typeclasses #

We define (semi)modularity typeclasses as Prop-valued mixins.

is_weak_upper_modular_lattice: Weakly upper modular lattices. Lattice where a ⊔ b covers a and b if a and b both cover a ⊓ b.
is_weak_lower_modular_lattice: Weakly lower modular lattices. Lattice where a and b cover a ⊓ b if a ⊔ b covers both a and b
is_upper_modular_lattice: Upper modular lattices. Lattices where a ⊔ b covers a if b covers a ⊓ b.
is_lower_modular_lattice: Lower modular lattices. Lattices where a covers a ⊓ b if a ⊔ b covers b.

is_modular_lattice: Modular lattices. Lattices where a ≤ c → (a ⊔ b) ⊓ c = a ⊔ (b ⊓ c). We only require an inequality because the other direction holds in all lattices.

Main Definitions #

inf_Icc_order_iso_Icc_sup gives 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 inf_sup_inf_assoc: (x ⊓ z) ⊔ (y ⊓ z) = ((x ⊓ z) ⊔ y) ⊓ z
distrib_lattice.is_modular_lattice: Distributive lattices are modular.

References #

Manfred Stern, Semimodular lattices. {Theory} and applications
[Wikipedia, Modular Lattice][https://en.wikipedia.org/wiki/Modular_lattice]

TODO #

Relate atoms and coatoms in modular lattices

source

@[class]

structure is_weak_upper_modular_lattice (α : Type u_2) [lattice α] :

Prop

covby_sup_of_inf_covby_covby : ∀ {a b : α}, a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b

A weakly upper modular lattice is a lattice where a ⊔ b covers a and b if a and b both cover a ⊓ b.

Instances of this typeclass

source

@[class]

structure is_weak_lower_modular_lattice (α : Type u_2) [lattice α] :

Prop

inf_covby_of_covby_covby_sup : ∀ {a b : α}, a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a

A weakly lower modular lattice is a lattice where a and b cover a ⊓ b if a ⊔ b covers both a and b.

Instances of this typeclass

source

@[class]

structure is_upper_modular_lattice (α : Type u_2) [lattice α] :

Prop

covby_sup_of_inf_covby : ∀ {a b : α}, a ⊓ b ⋖ a → b ⋖ a ⊔ b

An upper modular lattice, aka semimodular lattice, is a lattice where a ⊔ b covers a and b if either a or b covers a ⊓ b.

Instances of this typeclass

source

@[class]

structure is_lower_modular_lattice (α : Type u_2) [lattice α] :

Prop

inf_covby_of_covby_sup : ∀ {a b : α}, a ⋖ a ⊔ b → a ⊓ b ⋖ b

A lower modular lattice is a lattice where a and b both cover a ⊓ b if a ⊔ b covers either a or b.

Instances of this typeclass

source

@[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 of this typeclass

source

theorem covby_sup_of_inf_covby_of_inf_covby_left {α : Type u_1} [lattice α] [is_weak_upper_modular_lattice α] {a b : α} :

a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b

source

theorem covby_sup_of_inf_covby_of_inf_covby_right {α : Type u_1} [lattice α] [is_weak_upper_modular_lattice α] {a b : α} :

a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b

source

theorem covby.sup_of_inf_of_inf_left {α : Type u_1} [lattice α] [is_weak_upper_modular_lattice α] {a b : α} :

a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b

Alias of covby_sup_of_inf_covby_of_inf_covby_left.

source

theorem covby.sup_of_inf_of_inf_right {α : Type u_1} [lattice α] [is_weak_upper_modular_lattice α] {a b : α} :

a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b

Alias of covby_sup_of_inf_covby_of_inf_covby_right.

source

@[protected, instance]

def order_dual.is_weak_lower_modular_lattice {α : Type u_1} [lattice α] [is_weak_upper_modular_lattice α] :

is_weak_lower_modular_lattice αᵒᵈ

source

theorem inf_covby_of_covby_sup_of_covby_sup_left {α : Type u_1} [lattice α] [is_weak_lower_modular_lattice α] {a b : α} :

a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a

source

theorem inf_covby_of_covby_sup_of_covby_sup_right {α : Type u_1} [lattice α] [is_weak_lower_modular_lattice α] {a b : α} :

a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b

source

theorem covby.inf_of_sup_of_sup_left {α : Type u_1} [lattice α] [is_weak_lower_modular_lattice α] {a b : α} :

a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a

Alias of inf_covby_of_covby_sup_of_covby_sup_left.

source

theorem covby.inf_of_sup_of_sup_right {α : Type u_1} [lattice α] [is_weak_lower_modular_lattice α] {a b : α} :

a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b

Alias of inf_covby_of_covby_sup_of_covby_sup_right.

source

@[protected, instance]

def order_dual.is_weak_upper_modular_lattice {α : Type u_1} [lattice α] [is_weak_lower_modular_lattice α] :

is_weak_upper_modular_lattice αᵒᵈ

source

theorem covby_sup_of_inf_covby_left {α : Type u_1} [lattice α] [is_upper_modular_lattice α] {a b : α} :

a ⊓ b ⋖ a → b ⋖ a ⊔ b

source

theorem covby_sup_of_inf_covby_right {α : Type u_1} [lattice α] [is_upper_modular_lattice α] {a b : α} :

a ⊓ b ⋖ b → a ⋖ a ⊔ b

source

theorem covby.sup_of_inf_left {α : Type u_1} [lattice α] [is_upper_modular_lattice α] {a b : α} :

a ⊓ b ⋖ a → b ⋖ a ⊔ b

Alias of covby_sup_of_inf_covby_left.

source

theorem covby.sup_of_inf_right {α : Type u_1} [lattice α] [is_upper_modular_lattice α] {a b : α} :

a ⊓ b ⋖ b → a ⋖ a ⊔ b

Alias of covby_sup_of_inf_covby_right.

source

@[protected, instance]

def is_upper_modular_lattice.to_is_weak_upper_modular_lattice {α : Type u_1} [lattice α] [is_upper_modular_lattice α] :

is_weak_upper_modular_lattice α

source

@[protected, instance]

def order_dual.is_lower_modular_lattice {α : Type u_1} [lattice α] [is_upper_modular_lattice α] :

is_lower_modular_lattice αᵒᵈ

source

theorem inf_covby_of_covby_sup_left {α : Type u_1} [lattice α] [is_lower_modular_lattice α] {a b : α} :

a ⋖ a ⊔ b → a ⊓ b ⋖ b

source

theorem inf_covby_of_covby_sup_right {α : Type u_1} [lattice α] [is_lower_modular_lattice α] {a b : α} :

b ⋖ a ⊔ b → a ⊓ b ⋖ a

source

theorem covby.inf_of_sup_left {α : Type u_1} [lattice α] [is_lower_modular_lattice α] {a b : α} :

a ⋖ a ⊔ b → a ⊓ b ⋖ b

Alias of inf_covby_of_covby_sup_left.

source

theorem covby.inf_of_sup_right {α : Type u_1} [lattice α] [is_lower_modular_lattice α] {a b : α} :

b ⋖ a ⊔ b → a ⊓ b ⋖ a

Alias of inf_covby_of_covby_sup_right.

source

@[protected, instance]

def is_lower_modular_lattice.to_is_weak_lower_modular_lattice {α : Type u_1} [lattice α] [is_lower_modular_lattice α] :

is_weak_lower_modular_lattice α

source

@[protected, instance]

def order_dual.is_upper_modular_lattice {α : Type u_1} [lattice α] [is_lower_modular_lattice α] :

is_upper_modular_lattice αᵒᵈ

source

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

source

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

source

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)

source

@[protected, instance]

def order_dual.is_modular_lattice {α : Type u_1} [lattice α] [is_modular_lattice α] :

is_modular_lattice αᵒᵈ

source

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

source

theorem eq_of_le_of_inf_le_of_sup_le {α : Type u_1} [lattice α] [is_modular_lattice α] {x y z : α} (hxy : x ≤ y) (hinf : y ⊓ z ≤ x ⊓ z) (hsup : y ⊔ z ≤ x ⊔ z) :

x = y

source

theorem sup_lt_sup_of_lt_of_inf_le_inf {α : Type u_1} [lattice α] [is_modular_lattice α] {x y z : α} (hxy : x < y) (hinf : y ⊓ z ≤ x ⊓ z) :

x ⊔ z < y ⊔ z

source

theorem inf_lt_inf_of_lt_of_sup_le_sup {α : Type u_1} [lattice α] [is_modular_lattice α] {x y z : α} (hxy : x < y) (hinf : y ⊔ z ≤ x ⊔ z) :

x ⊓ z < y ⊓ z

source

theorem well_founded_lt_exact_sequence {α : Type u_1} [lattice α] [is_modular_lattice α] {β : Type u_2} {γ : Type u_3} [partial_order β] [preorder γ] (h₁ : well_founded has_lt.lt) (h₂ : well_founded has_lt.lt) (K : α) (f₁ : β → α) (f₂ : α → β) (g₁ : γ → α) (g₂ : α → γ) (gci : galois_coinsertion f₁ f₂) (gi : galois_insertion g₂ g₁) (hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K) (hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K) :

well_founded has_lt.lt

A generalization of the theorem that if N is a submodule of M and N and M / N are both Artinian, then M is Artinian.

source

theorem well_founded_gt_exact_sequence {α : Type u_1} [lattice α] [is_modular_lattice α] {β : Type u_2} {γ : Type u_3} [preorder β] [partial_order γ] (h₁ : well_founded gt) (h₂ : well_founded gt) (K : α) (f₁ : β → α) (f₂ : α → β) (g₁ : γ → α) (g₂ : α → γ) (gci : galois_coinsertion f₁ f₂) (gi : galois_insertion g₂ g₁) (hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K) (hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K) :

well_founded gt

A generalization of the theorem that if N is a submodule of M and N and M / N are both Noetherian, then M is Noetherian.

source

@[simp]

theorem inf_Icc_order_iso_Icc_sup_symm_apply_coe {α : Type u_1} [lattice α] [is_modular_lattice α] (a b : α) (x : ↥(set.Icc b (a ⊔ b))) :

↑(⇑(rel_iso.symm (inf_Icc_order_iso_Icc_sup a b)) x) = a ⊓ ↑x

source

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

inf_Icc_order_iso_Icc_sup a b = {to_equiv := {to_fun := λ (x : ↥(set.Icc (a ⊓ b) a)), ⟨↑x ⊔ b, _⟩, inv_fun := λ (x : ↥(set.Icc b (a ⊔ b))), ⟨a ⊓ ↑x, _⟩, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[simp]

theorem inf_Icc_order_iso_Icc_sup_apply_coe {α : Type u_1} [lattice α] [is_modular_lattice α] (a b : α) (x : ↥(set.Icc (a ⊓ b) a)) :

↑(⇑(inf_Icc_order_iso_Icc_sup a b) x) = ↑x ⊔ b

source

theorem inf_strict_mono_on_Icc_sup {α : Type u_1} [lattice α] [is_modular_lattice α] {a b : α} :

strict_mono_on (λ (c : α), a ⊓ c) (set.Icc b (a ⊔ b))

source

theorem sup_strict_mono_on_Icc_inf {α : Type u_1} [lattice α] [is_modular_lattice α] {a b : α} :

strict_mono_on (λ (c : α), c ⊔ b) (set.Icc (a ⊓ b) a)

source

@[simp]

theorem inf_Ioo_order_iso_Ioo_sup_apply_coe {α : Type u_1} [lattice α] [is_modular_lattice α] (a b : α) (c : ↥(set.Ioo (a ⊓ b) a)) :

↑(⇑(inf_Ioo_order_iso_Ioo_sup a b) c) = ↑c ⊔ b

source

@[simp]

theorem inf_Ioo_order_iso_Ioo_sup_symm_apply_coe {α : Type u_1} [lattice α] [is_modular_lattice α] (a b : α) (c : ↥(set.Ioo b (a ⊔ b))) :

↑(⇑(rel_iso.symm (inf_Ioo_order_iso_Ioo_sup a b)) c) = a ⊓ ↑c

source

def inf_Ioo_order_iso_Ioo_sup {α : Type u_1} [lattice α] [is_modular_lattice α] (a b : α) :

↥(set.Ioo (a ⊓ b) a) ≃o ↥(set.Ioo b (a ⊔ b))

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

Equations

inf_Ioo_order_iso_Ioo_sup a b = {to_equiv := {to_fun := λ (c : ↥(set.Ioo (a ⊓ b) a)), ⟨↑c ⊔ b, _⟩, inv_fun := λ (c : ↥(set.Ioo b (a ⊔ b))), ⟨a ⊓ ↑c, _⟩, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[protected, instance]

def is_modular_lattice.to_is_lower_modular_lattice {α : Type u_1} [lattice α] [is_modular_lattice α] :

is_lower_modular_lattice α

source

@[protected, instance]

def is_modular_lattice.to_is_upper_modular_lattice {α : Type u_1} [lattice α] [is_modular_lattice α] :

is_upper_modular_lattice α

source

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

↥(set.Iic a) ≃o ↥(set.Ici b)

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

Equations

h.Iic_order_iso_Ici = (order_iso.set_congr (set.Iic a) (set.Icc (a ⊓ b) a) _).trans ((inf_Icc_order_iso_Icc_sup a b).trans (order_iso.set_congr (set.Icc b (a ⊔ b)) (set.Ici b) _))

source

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

source

@[protected, instance]

def distrib_lattice.is_modular_lattice {α : Type u_1} [distrib_lattice α] :

is_modular_lattice α

source

theorem disjoint.disjoint_sup_right_of_disjoint_sup_left {α : Type u_1} [lattice α] [order_bot α] [is_modular_lattice α] {a b c : α} (h : disjoint a b) (hsup : disjoint (a ⊔ b) c) :

disjoint a (b ⊔ c)

source

theorem disjoint.disjoint_sup_left_of_disjoint_sup_right {α : Type u_1} [lattice α] [order_bot α] [is_modular_lattice α] {a b c : α} (h : disjoint b c) (hsup : disjoint a (b ⊔ c)) :

disjoint (a ⊔ b) c

source

@[protected, instance]

def is_modular_lattice.is_modular_lattice_Iic {α : Type u_1} [lattice α] [is_modular_lattice α] {a : α} :

is_modular_lattice ↥(set.Iic a)

source

@[protected, instance]

def is_modular_lattice.is_modular_lattice_Ici {α : Type u_1} [lattice α] [is_modular_lattice α] {a : α} :

is_modular_lattice ↥(set.Ici a)

source

@[protected, instance]

def is_modular_lattice.complemented_lattice_Iic {α : Type u_1} [lattice α] [is_modular_lattice α] {a : α} [bounded_order α] [complemented_lattice α] :

complemented_lattice ↥(set.Iic a)

source

@[protected, instance]

def is_modular_lattice.complemented_lattice_Ici {α : Type u_1} [lattice α] [is_modular_lattice α] {a : α} [bounded_order α] [complemented_lattice α] :

complemented_lattice ↥(set.Ici a)