# mathlib3documentation

order.modular_lattice

# 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.

## TODO #

• Relate atoms and coatoms in modular lattices
@[class]
structure is_weak_upper_modular_lattice (α : Type u_2) [lattice α] :
Prop

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
@[class]
structure is_weak_lower_modular_lattice (α : Type u_2) [lattice α] :
Prop

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
@[class]
structure is_upper_modular_lattice (α : Type u_2) [lattice α] :
Prop

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
@[class]
structure is_lower_modular_lattice (α : Type u_2) [lattice α] :
Prop

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
@[class]
structure is_modular_lattice (α : Type u_2) [lattice α] :
Prop

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

Instances of this typeclass
theorem covby_sup_of_inf_covby_of_inf_covby_left {α : Type u_1} [lattice α] {a b : α} :
a b a a b b a a b
theorem covby_sup_of_inf_covby_of_inf_covby_right {α : Type u_1} [lattice α] {a b : α} :
a b a a b b b a b
theorem covby.sup_of_inf_of_inf_left {α : Type u_1} [lattice α] {a b : α} :
a b a a b b a a b

Alias of covby_sup_of_inf_covby_of_inf_covby_left.

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

Alias of covby_sup_of_inf_covby_of_inf_covby_right.

@[protected, instance]
theorem inf_covby_of_covby_sup_of_covby_sup_left {α : Type u_1} [lattice α] {a b : α} :
a a b b a b a b a
theorem inf_covby_of_covby_sup_of_covby_sup_right {α : Type u_1} [lattice α] {a b : α} :
a a b b a b a b b
theorem covby.inf_of_sup_of_sup_left {α : Type u_1} [lattice α] {a b : α} :
a a b b a b a b a

Alias of inf_covby_of_covby_sup_of_covby_sup_left.

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

Alias of inf_covby_of_covby_sup_of_covby_sup_right.

@[protected, instance]
theorem covby_sup_of_inf_covby_left {α : Type u_1} [lattice α] {a b : α} :
a b a b a b
theorem covby_sup_of_inf_covby_right {α : Type u_1} [lattice α] {a b : α} :
a b b a a b
theorem covby.sup_of_inf_left {α : Type u_1} [lattice α] {a b : α} :
a b a b a b

Alias of covby_sup_of_inf_covby_left.

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

Alias of covby_sup_of_inf_covby_right.

@[protected, instance]
@[protected, instance]
theorem inf_covby_of_covby_sup_left {α : Type u_1} [lattice α] {a b : α} :
a a b a b b
theorem inf_covby_of_covby_sup_right {α : Type u_1} [lattice α] {a b : α} :
b a b a b a
theorem covby.inf_of_sup_left {α : Type u_1} [lattice α] {a b : α} :
a a b a b b

Alias of inf_covby_of_covby_sup_left.

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

Alias of inf_covby_of_covby_sup_right.

@[protected, instance]
@[protected, instance]
theorem sup_inf_assoc_of_le {α : Type u_1} [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 α] {x y z : α} :
x z y z = (x z y) z
theorem inf_sup_assoc_of_le {α : Type u_1} [lattice α] {x : α} (y : α) {z : α} (h : z x) :
x y z = x (y z)
@[protected, instance]
def order_dual.is_modular_lattice {α : Type u_1} [lattice α]  :
theorem is_modular_lattice.sup_inf_sup_assoc {α : Type u_1} [lattice α] {x y z : α} :
(x z) (y z) = (x z) y z
theorem eq_of_le_of_inf_le_of_sup_le {α : Type u_1} [lattice α] {x y z : α} (hxy : x y) (hinf : y z x z) (hsup : y z x z) :
x = y
theorem sup_lt_sup_of_lt_of_inf_le_inf {α : Type u_1} [lattice α] {x y z : α} (hxy : x < y) (hinf : y z x z) :
x z < y z
theorem inf_lt_inf_of_lt_of_sup_le_sup {α : Type u_1} [lattice α] {x y z : α} (hxy : x < y) (hinf : y z x z) :
x z < y z
theorem well_founded_lt_exact_sequence {α : Type u_1} [lattice α] {β : Type u_2} {γ : Type u_3} [preorder γ] (h₁ : well_founded has_lt.lt) (h₂ : well_founded has_lt.lt) (K : α) (f₁ : β α) (f₂ : α β) (g₁ : γ α) (g₂ : α γ) (gci : f₂) (gi : g₁) (hf : (a : α), f₁ (f₂ a) = a K) (hg : (a : α), g₁ (g₂ a) = a K) :

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.

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

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.

@[simp]
theorem inf_Icc_order_iso_Icc_sup_symm_apply_coe {α : Type u_1} [lattice α] (a b : α) (x : (set.Icc b (a b))) :
( x) = a x
def inf_Icc_order_iso_Icc_sup {α : Type u_1} [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
@[simp]
theorem inf_Icc_order_iso_Icc_sup_apply_coe {α : Type u_1} [lattice α] (a b : α) (x : (set.Icc (a b) a)) :
( x) = x b
theorem inf_strict_mono_on_Icc_sup {α : Type u_1} [lattice α] {a b : α} :
strict_mono_on (λ (c : α), a c) (set.Icc b (a b))
theorem sup_strict_mono_on_Icc_inf {α : Type u_1} [lattice α] {a b : α} :
strict_mono_on (λ (c : α), c b) (set.Icc (a b) a)
@[simp]
theorem inf_Ioo_order_iso_Ioo_sup_apply_coe {α : Type u_1} [lattice α] (a b : α) (c : (set.Ioo (a b) a)) :
( c) = c b
@[simp]
theorem inf_Ioo_order_iso_Ioo_sup_symm_apply_coe {α : Type u_1} [lattice α] (a b : α) (c : (set.Ioo b (a b))) :
( c) = a c
def inf_Ioo_order_iso_Ioo_sup {α : Type u_1} [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
@[protected, instance]
@[protected, instance]
def is_compl.Iic_order_iso_Ici {α : Type u_1} [lattice α] {a b : α} (h : 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 α] :
(x y z : α), x z y z = (x z y) z
@[protected, instance]
theorem disjoint.disjoint_sup_right_of_disjoint_sup_left {α : Type u_1} [lattice α] [order_bot α] {a b c : α} (h : b) (hsup : disjoint (a b) c) :
(b c)
theorem disjoint.disjoint_sup_left_of_disjoint_sup_right {α : Type u_1} [lattice α] [order_bot α] {a b c : α} (h : c) (hsup : (b c)) :
disjoint (a b) c
@[protected, instance]
def is_modular_lattice.is_modular_lattice_Iic {α : Type u_1} [lattice α] {a : α} :
@[protected, instance]
def is_modular_lattice.is_modular_lattice_Ici {α : Type u_1} [lattice α] {a : α} :
@[protected, instance]
def is_modular_lattice.complemented_lattice_Iic {α : Type u_1} [lattice α] {a : α}  :
@[protected, instance]
def is_modular_lattice.complemented_lattice_Ici {α : Type u_1} [lattice α] {a : α}  :