# Modular Lattices #

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.

• IsWeakUpperModularLattice: Weakly upper modular lattices. Lattice where a ⊔ b covers a and b if a and b both cover a ⊓ b.
• IsWeakLowerModularLattice: Weakly lower modular lattices. Lattice where a and b cover a ⊓ b if a ⊔ b covers both a and b
• IsUpperModularLattice: Upper modular lattices. Lattices where a ⊔ b covers a if b covers a ⊓ b.
• IsLowerModularLattice: Lower modular lattices. Lattices where a covers a ⊓ b if a ⊔ b covers b.
• IsModularLattice: 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 #

• infIccOrderIsoIccSup 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 #

• isModularLattice_iff_inf_sup_inf_assoc: Modularity is equivalent to the inf_sup_inf_assoc: (x ⊓ z) ⊔ (y ⊓ z) = ((x ⊓ z) ⊔ y) ⊓ z
• DistribLattice.isModularLattice: Distributive lattices are modular.

## References #

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

## TODO #

• Relate atoms and coatoms in modular lattices
class IsWeakUpperModularLattice (α : Type u_2) [] :

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

• covBy_sup_of_inf_covBy_covBy : ∀ {a b : α}, a b aa b ba a b

a ⊔ b covers a and b if a and b both cover a ⊓ b.

Instances
theorem IsWeakUpperModularLattice.covBy_sup_of_inf_covBy_covBy {α : Type u_2} [] [self : ] {a : α} {b : α} :
a b aa b ba a b

a ⊔ b covers a and b if a and b both cover a ⊓ b.

class IsWeakLowerModularLattice (α : Type u_2) [] :

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

• inf_covBy_of_covBy_covBy_sup : ∀ {a b : α}, a a bb a ba b a

a and b cover a ⊓ b if a ⊔ b covers both a and b

Instances
theorem IsWeakLowerModularLattice.inf_covBy_of_covBy_covBy_sup {α : Type u_2} [] [self : ] {a : α} {b : α} :
a a bb a ba b a

a and b cover a ⊓ b if a ⊔ b covers both a and b

class IsUpperModularLattice (α : Type u_2) [] :

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.

• covBy_sup_of_inf_covBy : ∀ {a b : α}, a b ab a b

a ⊔ b covers a and b if either a or b covers a ⊓ b

Instances
theorem IsUpperModularLattice.covBy_sup_of_inf_covBy {α : Type u_2} [] [self : ] {a : α} {b : α} :
a b ab a b

a ⊔ b covers a and b if either a or b covers a ⊓ b

class IsLowerModularLattice (α : Type u_2) [] :

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

• inf_covBy_of_covBy_sup : ∀ {a b : α}, a a ba b b

a and b both cover a ⊓ b if a ⊔ b covers either a or b

Instances
theorem IsLowerModularLattice.inf_covBy_of_covBy_sup {α : Type u_2} [] [self : ] {a : α} {b : α} :
a a ba b b

a and b both cover a ⊓ b if a ⊔ b covers either a or b

class IsModularLattice (α : Type u_2) [] :

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

• sup_inf_le_assoc_of_le : ∀ {x : α} (y : α) {z : α}, x z(x y) z x y z

Whenever x ≤ z, then for any y, (x ⊔ y) ⊓ z ≤ x ⊔ (y ⊓ z)

Instances
theorem IsModularLattice.sup_inf_le_assoc_of_le {α : Type u_2} [] [self : ] {x : α} (y : α) {z : α} :
x z(x y) z x y z

Whenever x ≤ z, then for any y, (x ⊔ y) ⊓ z ≤ x ⊔ (y ⊓ z)

theorem covBy_sup_of_inf_covBy_of_inf_covBy_left {α : Type u_1} [] {a : α} {b : α} :
a b aa b ba a b
theorem covBy_sup_of_inf_covBy_of_inf_covBy_right {α : Type u_1} [] {a : α} {b : α} :
a b aa b bb a b
theorem CovBy.sup_of_inf_of_inf_left {α : Type u_1} [] {a : α} {b : α} :
a b aa b ba a b

Alias of covBy_sup_of_inf_covBy_of_inf_covBy_left.

theorem CovBy.sup_of_inf_of_inf_right {α : Type u_1} [] {a : α} {b : α} :
a b aa b bb a b

Alias of covBy_sup_of_inf_covBy_of_inf_covBy_right.

Equations
• =
theorem inf_covBy_of_covBy_sup_of_covBy_sup_left {α : Type u_1} [] {a : α} {b : α} :
a a bb a ba b a
theorem inf_covBy_of_covBy_sup_of_covBy_sup_right {α : Type u_1} [] {a : α} {b : α} :
a a bb a ba b b
theorem CovBy.inf_of_sup_of_sup_left {α : Type u_1} [] {a : α} {b : α} :
a a bb a ba b a

Alias of inf_covBy_of_covBy_sup_of_covBy_sup_left.

theorem CovBy.inf_of_sup_of_sup_right {α : Type u_1} [] {a : α} {b : α} :
a a bb a ba b b

Alias of inf_covBy_of_covBy_sup_of_covBy_sup_right.

Equations
• =
theorem covBy_sup_of_inf_covBy_left {α : Type u_1} [] {a : α} {b : α} :
a b ab a b
theorem covBy_sup_of_inf_covBy_right {α : Type u_1} [] {a : α} {b : α} :
a b ba a b
theorem CovBy.sup_of_inf_left {α : Type u_1} [] {a : α} {b : α} :
a b ab a b

Alias of covBy_sup_of_inf_covBy_left.

theorem CovBy.sup_of_inf_right {α : Type u_1} [] {a : α} {b : α} :
a b ba a b

Alias of covBy_sup_of_inf_covBy_right.

@[instance 100]
Equations
• =
instance instIsLowerModularLatticeOrderDual {α : Type u_1} [] :
Equations
• =
theorem inf_covBy_of_covBy_sup_left {α : Type u_1} [] {a : α} {b : α} :
a a ba b b
theorem inf_covBy_of_covBy_sup_right {α : Type u_1} [] {a : α} {b : α} :
b a ba b a
theorem CovBy.inf_of_sup_left {α : Type u_1} [] {a : α} {b : α} :
a a ba b b

Alias of inf_covBy_of_covBy_sup_left.

theorem CovBy.inf_of_sup_right {α : Type u_1} [] {a : α} {b : α} :
b a ba b a

Alias of inf_covBy_of_covBy_sup_right.

@[instance 100]
Equations
• =
instance instIsUpperModularLatticeOrderDual {α : Type u_1} [] :
Equations
• =
theorem sup_inf_assoc_of_le {α : Type u_1} [] [] {x : α} (y : α) {z : α} (h : x z) :
(x y) z = x y z
theorem IsModularLattice.inf_sup_inf_assoc {α : Type u_1} [] [] {x : α} {y : α} {z : α} :
x z y z = (x z y) z
theorem inf_sup_assoc_of_le {α : Type u_1} [] [] {x : α} (y : α) {z : α} (h : z x) :
x y z = x (y z)
instance instIsModularLatticeOrderDual {α : Type u_1} [] [] :
Equations
• =
theorem IsModularLattice.sup_inf_sup_assoc {α : Type u_1} [] [] {x : α} {y : α} {z : α} :
(x z) (y z) = (x z) y z
theorem eq_of_le_of_inf_le_of_sup_le {α : Type u_1} [] [] {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} [] [] {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} [] [] {x : α} {y : α} {z : α} (hxy : x < y) (hinf : y z x z) :
x z < y z
theorem wellFounded_lt_exact_sequence {α : Type u_1} [] [] {β : Type u_2} {γ : Type u_3} [] [] (h₁ : WellFounded fun (x x_1 : β) => x < x_1) (h₂ : WellFounded fun (x x_1 : γ) => x < x_1) (K : α) (f₁ : βα) (f₂ : αβ) (g₁ : γα) (g₂ : αγ) (gci : ) (gi : GaloisInsertion g₂ g₁) (hf : ∀ (a : α), f₁ (f₂ a) = a K) (hg : ∀ (a : α), g₁ (g₂ a) = a K) :
WellFounded fun (x x_1 : α) => x < x_1

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 wellFounded_gt_exact_sequence {α : Type u_1} [] [] {β : Type u_2} {γ : Type u_3} [] [] (h₁ : WellFounded fun (x x_1 : β) => x > x_1) (h₂ : WellFounded fun (x x_1 : γ) => x > x_1) (K : α) (f₁ : βα) (f₂ : αβ) (g₁ : γα) (g₂ : αγ) (gci : ) (gi : GaloisInsertion g₂ g₁) (hf : ∀ (a : α), f₁ (f₂ a) = a K) (hg : ∀ (a : α), g₁ (g₂ a) = a K) :
WellFounded fun (x x_1 : α) => x > x_1

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 infIccOrderIsoIccSup_symm_apply_coe {α : Type u_1} [] [] (a : α) (b : α) (x : (Set.Icc b (a b))) :
(() x) = a x
@[simp]
theorem infIccOrderIsoIccSup_apply_coe {α : Type u_1} [] [] (a : α) (b : α) (x : (Set.Icc (a b) a)) :
(() x) = x b
def infIccOrderIsoIccSup {α : Type u_1} [] [] (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
• One or more equations did not get rendered due to their size.
Instances For
theorem inf_strictMonoOn_Icc_sup {α : Type u_1} [] [] {a : α} {b : α} :
StrictMonoOn (fun (c : α) => a c) (Set.Icc b (a b))
theorem sup_strictMonoOn_Icc_inf {α : Type u_1} [] [] {a : α} {b : α} :
StrictMonoOn (fun (c : α) => c b) (Set.Icc (a b) a)
@[simp]
theorem infIooOrderIsoIooSup_apply_coe {α : Type u_1} [] [] (a : α) (b : α) (c : (Set.Ioo (a b) a)) :
(() c) = c b
@[simp]
theorem infIooOrderIsoIooSup_symm_apply_coe {α : Type u_1} [] [] (a : α) (b : α) (c : (Set.Ioo b (a b))) :
(() c) = a c
def infIooOrderIsoIooSup {α : Type u_1} [] [] (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
• One or more equations did not get rendered due to their size.
Instances For
@[instance 100]
Equations
• =
@[instance 100]
Equations
• =
def IsCompl.IicOrderIsoIci {α : Type u_1} [] [] [] {a : α} {b : α} (h : IsCompl a b) :
() ≃o ()

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

Equations
Instances For
theorem isModularLattice_iff_inf_sup_inf_assoc {α : Type u_1} [] :
∀ (x y z : α), x z y z = (x z y) z
@[instance 100]
instance DistribLattice.instIsModularLattice {α : Type u_1} [] :
Equations
• =
theorem Disjoint.disjoint_sup_right_of_disjoint_sup_left {α : Type u_1} {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} {a : α} {b : α} {c : α} [] [] [] (h : Disjoint b c) (hsup : Disjoint a (b c)) :
Disjoint (a b) c
theorem Disjoint.isCompl_sup_right_of_isCompl_sup_left {α : Type u_1} {a : α} {b : α} {c : α} [] [] [] (h : Disjoint a b) (hcomp : IsCompl (a b) c) :
IsCompl a (b c)
theorem Disjoint.isCompl_sup_left_of_isCompl_sup_right {α : Type u_1} {a : α} {b : α} {c : α} [] [] [] (h : Disjoint b c) (hcomp : IsCompl a (b c)) :
IsCompl (a b) c
theorem Set.Iic.isCompl_inf_inf_of_isCompl_of_le {α : Type u_1} [] [] [] {a : α} {b : α} {c : α} (h₁ : IsCompl b c) (h₂ : b a) :
IsCompl a b, a c,
instance IsModularLattice.isModularLattice_Iic {α : Type u_1} [] [] {a : α} :
Equations
• =
instance IsModularLattice.isModularLattice_Ici {α : Type u_1} [] [] {a : α} :
Equations
• =
instance IsModularLattice.complementedLattice_Iic {α : Type u_1} [] [] {a : α} [] :
Equations
• =
instance IsModularLattice.complementedLattice_Ici {α : Type u_1} [] [] {a : α} [] :
Equations
• =