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) [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.

• covBy_sup_of_inf_covBy_covBy {a b : α} : a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b

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

class IsWeakLowerModularLattice (α : 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.

• inf_covBy_of_covBy_covBy_sup {a b : α} : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a

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

class IsUpperModularLattice (α : 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.

• covBy_sup_of_inf_covBy {a b : α} : a ⊓ b ⋖ a → b ⋖ a ⊔ b

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

class IsLowerModularLattice (α : 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.

• inf_covBy_of_covBy_sup {a b : α} : a ⋖ a ⊔ b → a ⊓ b ⋖ b

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

class IsModularLattice (α : Type u_2) [Lattice α] : Prop

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)

theorem covBy_sup_of_inf_covBy_of_inf_covBy_left {α : Type u_1} [Lattice α] [IsWeakUpperModularLattice α] {a b : α} : a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b

theorem inf_covBy_of_covBy_sup_of_covBy_sup_left {α : Type u_1} [Lattice α] [IsWeakLowerModularLattice α] {a b : α} : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a

theorem covBy_sup_of_inf_covBy_of_inf_covBy_right {α : Type u_1} [Lattice α] [IsWeakUpperModularLattice α] {a b : α} : a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b

theorem inf_covBy_of_covBy_sup_of_covBy_sup_right {α : Type u_1} [Lattice α] [IsWeakLowerModularLattice α] {a b : α} : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b

theorem CovBy.sup_of_inf_of_inf_left {α : Type u_1} [Lattice α] [IsWeakUpperModularLattice α] {a b : α} : a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b

Alias of covBy_sup_of_inf_covBy_of_inf_covBy_left.

theorem CovBy.inf_of_sup_of_sup_left {α : Type u_1} [Lattice α] [IsWeakLowerModularLattice α] {a b : α} : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a

theorem CovBy.sup_of_inf_of_inf_right {α : Type u_1} [Lattice α] [IsWeakUpperModularLattice α] {a b : α} : a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b

Alias of covBy_sup_of_inf_covBy_of_inf_covBy_right.

theorem CovBy.inf_of_sup_of_sup_right {α : Type u_1} [Lattice α] [IsWeakLowerModularLattice α] {a b : α} : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b

instance instIsWeakLowerModularLatticeOrderDual {α : Type u_1} [Lattice α] [IsWeakUpperModularLattice α] : IsWeakLowerModularLattice αᵒᵈ

instance instIsWeakUpperModularLatticeOrderDual {α : Type u_1} [Lattice α] [IsWeakLowerModularLattice α] : IsWeakUpperModularLattice αᵒᵈ

theorem covBy_sup_of_inf_covBy_left {α : Type u_1} [Lattice α] [IsUpperModularLattice α] {a b : α} : a ⊓ b ⋖ a → b ⋖ a ⊔ b

theorem inf_covBy_of_covBy_sup_left {α : Type u_1} [Lattice α] [IsLowerModularLattice α] {a b : α} : a ⋖ a ⊔ b → a ⊓ b ⋖ b

theorem covBy_sup_of_inf_covBy_right {α : Type u_1} [Lattice α] [IsUpperModularLattice α] {a b : α} : a ⊓ b ⋖ b → a ⋖ a ⊔ b

theorem inf_covBy_of_covBy_sup_right {α : Type u_1} [Lattice α] [IsLowerModularLattice α] {a b : α} : b ⋖ a ⊔ b → a ⊓ b ⋖ a

theorem CovBy.sup_of_inf_left {α : Type u_1} [Lattice α] [IsUpperModularLattice α] {a b : α} : a ⊓ b ⋖ a → b ⋖ a ⊔ b

Alias of covBy_sup_of_inf_covBy_left.

theorem CovBy.inf_of_sup_left {α : Type u_1} [Lattice α] [IsLowerModularLattice α] {a b : α} : a ⋖ a ⊔ b → a ⊓ b ⋖ b

theorem CovBy.sup_of_inf_right {α : Type u_1} [Lattice α] [IsUpperModularLattice α] {a b : α} : a ⊓ b ⋖ b → a ⋖ a ⊔ b

Alias of covBy_sup_of_inf_covBy_right.

theorem CovBy.inf_of_sup_right {α : Type u_1} [Lattice α] [IsLowerModularLattice α] {a b : α} : b ⋖ a ⊔ b → a ⊓ b ⋖ a

@[instance 100]

instance IsUpperModularLattice.to_isWeakUpperModularLattice {α : Type u_1} [Lattice α] [IsUpperModularLattice α] : IsWeakUpperModularLattice α

@[instance 100]

instance IsLowerModularLattice.to_isWeakLowerModularLattice {α : Type u_1} [Lattice α] [IsLowerModularLattice α] : IsWeakLowerModularLattice α

instance instIsLowerModularLatticeOrderDual {α : Type u_1} [Lattice α] [IsUpperModularLattice α] : IsLowerModularLattice αᵒᵈ

instance instIsUpperModularLatticeOrderDual {α : Type u_1} [Lattice α] [IsLowerModularLattice α] : IsUpperModularLattice αᵒᵈ

theorem sup_inf_le_assoc_of_le {α : Type u_1} [Lattice α] [IsModularLattice α] {x z : α} (y : α) : x ≤ z → (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z

theorem inf_sup_le_assoc_of_le {α : Type u_1} [Lattice α] [IsModularLattice α] {x z : α} (y : α) : z ≤ x → x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ z

theorem sup_inf_assoc_of_le {α : Type u_1} [Lattice α] [IsModularLattice α] {x : α} (y : α) {z : α} (h : x ≤ z) : (x ⊔ y) ⊓ z = x ⊔ y ⊓ z

theorem inf_sup_assoc_of_le {α : Type u_1} [Lattice α] [IsModularLattice α] {x : α} (y : α) {z : α} (h : z ≤ x) : x ⊓ y ⊔ z = x ⊓ (y ⊔ z)

theorem IsModularLattice.inf_sup_inf_assoc {α : Type u_1} [Lattice α] [IsModularLattice α] {x y z : α} : x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z

theorem IsModularLattice.sup_inf_sup_assoc {α : Type u_1} [Lattice α] [IsModularLattice α] {x y z : α} : (x ⊔ z) ⊓ (y ⊔ z) = (x ⊔ z) ⊓ y ⊔ z

instance instIsModularLatticeOrderDual {α : Type u_1} [Lattice α] [IsModularLattice α] : IsModularLattice αᵒᵈ

theorem eq_of_le_of_inf_le_of_le_sup {α : Type u_1} [Lattice α] [IsModularLattice α] {x y z : α} (hxy : x ≤ y) (hinf : y ⊓ z ≤ x) (hsup : y ≤ x ⊔ z) : x = y

theorem eq_of_le_of_sup_le_of_le_inf {α : Type u_1} [Lattice α] [IsModularLattice α] {x y z : α} (hxy : y ≤ x) (hsup : x ≤ y ⊔ z) (hinf : x ⊓ z ≤ y) : x = y

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

theorem eq_of_le_of_sup_le_of_inf_le {α : Type u_1} [Lattice α] [IsModularLattice α] {x y z : α} (hxy : y ≤ x) (hsup : x ⊔ z ≤ y ⊔ z) (hinf : x ⊓ z ≤ y ⊓ z) : x = y

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

theorem inf_lt_inf_of_lt_of_sup_le_sup {α : Type u_1} [Lattice α] [IsModularLattice α] {x y z : α} (hxy : x < y) (hsup : y ⊔ z ≤ x ⊔ z) : x ⊓ z < y ⊓ z

theorem strictMono_inf_prod_sup {α : Type u_1} [Lattice α] [IsModularLattice α] {z : α} : StrictMono fun (x : α) => (x ⊓ z, x ⊔ z)

theorem wellFounded_lt_exact_sequence {α : Type u_1} [Lattice α] [IsModularLattice α] {β : Type u_2} {γ : Type u_3} [Preorder β] [Preorder γ] [h₁ : WellFoundedLT β] [h₂ : WellFoundedLT γ] (K : α) (f₁ : β → α) (f₂ : α → β) (g₁ : γ → α) (g₂ : α → γ) (gci : GaloisCoinsertion f₁ f₂) (gi : GaloisInsertion g₂ g₁) (hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K) (hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K) : WellFoundedLT α

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} [Lattice α] [IsModularLattice α] {β : Type u_2} {γ : Type u_3} [Preorder β] [Preorder γ] [WellFoundedGT β] [WellFoundedGT γ] (K : α) (f₁ : β → α) (f₂ : α → β) (g₁ : γ → α) (g₂ : α → γ) (gci : GaloisCoinsertion f₁ f₂) (gi : GaloisInsertion g₂ g₁) (hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K) (hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K) : WellFoundedGT α

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.

def infIccOrderIsoIccSup {α : Type u_1} [Lattice α] [IsModularLattice α] (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

• infIccOrderIsoIccSup a b = { toFun := fun (x : ↑(Set.Icc (a ⊓ b) a)) => ⟨↑x ⊔ b, ⋯⟩, invFun := fun (x : ↑(Set.Icc b (a ⊔ b))) => ⟨a ⊓ ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem infIccOrderIsoIccSup_apply_coe {α : Type u_1} [Lattice α] [IsModularLattice α] (a b : α) (x : ↑(Set.Icc (a ⊓ b) a)) : ↑((infIccOrderIsoIccSup a b) x) = ↑x ⊔ b

@[simp]

theorem infIccOrderIsoIccSup_symm_apply_coe {α : Type u_1} [Lattice α] [IsModularLattice α] (a b : α) (x : ↑(Set.Icc b (a ⊔ b))) : ↑((RelIso.symm (infIccOrderIsoIccSup a b)) x) = a ⊓ ↑x

theorem inf_strictMonoOn_Icc_sup {α : Type u_1} [Lattice α] [IsModularLattice α] {a b : α} : StrictMonoOn (fun (c : α) => a ⊓ c) (Set.Icc b (a ⊔ b))

theorem sup_strictMonoOn_Icc_inf {α : Type u_1} [Lattice α] [IsModularLattice α] {a b : α} : StrictMonoOn (fun (c : α) => c ⊔ b) (Set.Icc (a ⊓ b) a)

def infIooOrderIsoIooSup {α : Type u_1} [Lattice α] [IsModularLattice α] (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

• infIooOrderIsoIooSup a b = { toFun := fun (c : ↑(Set.Ioo (a ⊓ b) a)) => ⟨↑c ⊔ b, ⋯⟩, invFun := fun (c : ↑(Set.Ioo b (a ⊔ b))) => ⟨a ⊓ ↑c, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem infIooOrderIsoIooSup_symm_apply_coe {α : Type u_1} [Lattice α] [IsModularLattice α] (a b : α) (c : ↑(Set.Ioo b (a ⊔ b))) : ↑((RelIso.symm (infIooOrderIsoIooSup a b)) c) = a ⊓ ↑c

@[simp]

theorem infIooOrderIsoIooSup_apply_coe {α : Type u_1} [Lattice α] [IsModularLattice α] (a b : α) (c : ↑(Set.Ioo (a ⊓ b) a)) : ↑((infIooOrderIsoIooSup a b) c) = ↑c ⊔ b

@[instance 100]

instance IsModularLattice.to_isLowerModularLattice {α : Type u_1} [Lattice α] [IsModularLattice α] : IsLowerModularLattice α

@[instance 100]

instance IsModularLattice.to_isUpperModularLattice {α : Type u_1} [Lattice α] [IsModularLattice α] : IsUpperModularLattice α

def IsCompl.IicOrderIsoIci {α : Type u_1} [Lattice α] [BoundedOrder α] [IsModularLattice α] {a b : α} (h : IsCompl a b) : ↑(Set.Iic a) ≃o ↑(Set.Ici b)

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

Equations

• h.IicOrderIsoIci = (OrderIso.setCongr (Set.Iic a) (Set.Icc (a ⊓ b) a) ⋯).trans ((infIccOrderIsoIccSup a b).trans (OrderIso.setCongr (Set.Icc b (a ⊔ b)) (Set.Ici b) ⋯))

theorem le_iff_eq_of_codisjoint_of_disjoint {α : Type u_1} [Lattice α] [BoundedOrder α] [IsModularLattice α] {a b c : α} (h₀ : Codisjoint a b) (h₁ : Disjoint b c) : a ≤ c ↔ a = c

theorem isModularLattice_iff_inf_sup_inf_assoc {α : Type u_1} [Lattice α] : IsModularLattice α ↔ ∀ (x y z : α), x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z

@[instance 100]

instance DistribLattice.instIsModularLattice {α : Type u_1} [DistribLattice α] : IsModularLattice α

theorem Disjoint.disjoint_sup_right_of_disjoint_sup_left {α : Type u_1} {a b c : α} [Lattice α] [OrderBot α] [IsModularLattice α] (h : Disjoint a b) (hsup : Disjoint (a ⊔ b) c) : Disjoint a (b ⊔ c)

theorem Codisjoint.codisjoint_inf_right_of_codisjoint_inf_left {α : Type u_1} {a b c : α} [Lattice α] [OrderTop α] [IsModularLattice α] (h : Codisjoint a b) (hinf : Codisjoint (a ⊓ b) c) : Codisjoint a (b ⊓ c)

theorem Disjoint.disjoint_sup_left_of_disjoint_sup_right {α : Type u_1} {a b c : α} [Lattice α] [OrderBot α] [IsModularLattice α] (h : Disjoint b c) (hsup : Disjoint a (b ⊔ c)) : Disjoint (a ⊔ b) c

theorem Codisjoint.codisjoint_inf_left_of_codisjoint_inf_right {α : Type u_1} {a b c : α} [Lattice α] [OrderTop α] [IsModularLattice α] (h : Codisjoint b c) (hinf : Codisjoint a (b ⊓ c)) : Codisjoint (a ⊓ b) c

theorem disjoint_sup_right_of_disjoint_sup_right {α : Type u_1} {a b c : α} [Lattice α] [OrderBot α] [IsModularLattice α] (h₁ : Disjoint a (b ⊔ c)) (h₂ : Disjoint b (c ⊔ a)) : Disjoint c (a ⊔ b)

theorem codisjoint_inf_right_of_codisjoint_inf_right {α : Type u_1} {a b c : α} [Lattice α] [OrderTop α] [IsModularLattice α] (h₁ : Codisjoint a (b ⊓ c)) (h₂ : Codisjoint b (c ⊓ a)) : Codisjoint c (a ⊓ b)

theorem Disjoint.isCompl_sup_right_of_isCompl_sup_left {α : Type u_1} {a b c : α} [Lattice α] [BoundedOrder α] [IsModularLattice α] (h : Disjoint a b) (hcomp : IsCompl (a ⊔ b) c) : IsCompl a (b ⊔ c)

theorem Codisjoint.isCompl_inf_right_of_isCompl_inf_left {α : Type u_1} {a b c : α} [Lattice α] [BoundedOrder α] [IsModularLattice α] (h : Codisjoint 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 : α} [Lattice α] [BoundedOrder α] [IsModularLattice α] (h : Disjoint b c) (hcomp : IsCompl a (b ⊔ c)) : IsCompl (a ⊔ b) c

theorem Codisjoint.isCompl_inf_left_of_isCompl_inf_right {α : Type u_1} {a b c : α} [Lattice α] [BoundedOrder α] [IsModularLattice α] (h : Codisjoint b c) (hcomp : IsCompl a (b ⊓ c)) : IsCompl (a ⊓ b) c

theorem Set.Iic.isCompl_inf_inf_of_isCompl_of_le {α : Type u_1} [Lattice α] [BoundedOrder α] [IsModularLattice α] {a b c : α} (h₁ : IsCompl b c) (h₂ : b ≤ a) : IsCompl ⟨a ⊓ b, ⋯⟩ ⟨a ⊓ c, ⋯⟩

instance IsModularLattice.isModularLattice_Iic {α : Type u_1} [Lattice α] [IsModularLattice α] {a : α} : IsModularLattice ↑(Set.Iic a)

instance IsModularLattice.isModularLattice_Ici {α : Type u_1} [Lattice α] [IsModularLattice α] {a : α} : IsModularLattice ↑(Set.Ici a)

theorem IsModularLattice.exists_inf_eq_and_sup_eq {α : Type u_1} [Lattice α] [IsModularLattice α] {a b c : α} [BoundedOrder α] [ComplementedLattice α] (hb : a ≤ b) (hc : b ≤ c) : ∃ (b' : α), b ⊓ b' = a ∧ b ⊔ b' = c

theorem IsModularLattice.exists_disjoint_and_sup_eq {α : Type u_1} [Lattice α] [IsModularLattice α] {a b : α} [BoundedOrder α] [ComplementedLattice α] (h : a ≤ b) : ∃ (a' : α), Disjoint a a' ∧ a ⊔ a' = b

theorem IsModularLattice.exists_inf_eq_and_codisjoint {α : Type u_1} [Lattice α] [IsModularLattice α] {a b : α} [BoundedOrder α] [ComplementedLattice α] (h : a ≤ b) : ∃ (b' : α), b ⊓ b' = a ∧ Codisjoint b b'

instance IsModularLattice.complementedLattice_Icc {α : Type u_1} [Lattice α] [IsModularLattice α] {a b : α} [BoundedOrder α] [ComplementedLattice α] [Fact (a ≤ b)] : ComplementedLattice ↑(Set.Icc a b)

instance IsModularLattice.complementedLattice_Iic {α : Type u_1} [Lattice α] [IsModularLattice α] {a : α} [BoundedOrder α] [ComplementedLattice α] : ComplementedLattice ↑(Set.Iic a)

instance IsModularLattice.complementedLattice_Ici {α : Type u_1} [Lattice α] [IsModularLattice α] {a : α} [BoundedOrder α] [ComplementedLattice α] : ComplementedLattice ↑(Set.Ici a)

theorem Disjoint.exists_isCompl {α : Type u_1} [Lattice α] [IsModularLattice α] [BoundedOrder α] [ComplementedLattice α] {a b : α} (hab : Disjoint a b) : ∃ (a' : α), a ≤ a' ∧ IsCompl a' b

A disjoint element can be enlarged to a complementary element.

theorem Codisjoint.exists_isCompl {α : Type u_1} [Lattice α] [IsModularLattice α] [BoundedOrder α] [ComplementedLattice α] {a b : α} (hab : Codisjoint a b) : ∃ a' ≤ a, IsCompl a' b

A codisjoint element can be shrunk to a complementary element.