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

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

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

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

• 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

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

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

• 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

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.

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

• 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

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

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

• 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)

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

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

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

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 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.inf_of_sup_of_sup_left {α : Type u_1} [Lattice α] [IsWeakLowerModularLattice α] {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 α] [IsWeakLowerModularLattice α] {a : α} {b : α} : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b

Alias of inf_covby_of_covby_sup_of_covby_sup_right.

instance instIsWeakUpperModularLatticeOrderDualLattice {α : 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 covby_sup_of_inf_covby_right {α : Type u_1} [Lattice α] [IsUpperModularLattice α] {a : α} {b : α} : a ⊓ b ⋖ b → a ⋖ a ⊔ b

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

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

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

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

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

theorem Covby.inf_of_sup_left {α : Type u_1} [Lattice α] [IsLowerModularLattice α] {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 α] [IsLowerModularLattice α] {a : α} {b : α} : b ⋖ a ⊔ b → a ⊓ b ⋖ a

Alias of inf_covby_of_covby_sup_right.

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

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

theorem sup_inf_assoc_of_le {α : Type u_1} [Lattice α] [IsModularLattice α] {x : α} (y : α) {z : α} (h : x ≤ z) : (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 inf_sup_assoc_of_le {α : Type u_1} [Lattice α] [IsModularLattice α] {x : α} (y : α) {z : α} (h : z ≤ x) : x ⊓ y ⊔ z = x ⊓ (y ⊔ z)

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

theorem IsModularLattice.sup_inf_sup_assoc {α : Type u_1} [Lattice α] [IsModularLattice α] {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 α] [IsModularLattice α] {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 α] [IsModularLattice α] {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 α] [IsModularLattice α] {x : α} {y : α} {z : α} (hxy : x < y) (hinf : y ⊔ z ≤ x ⊔ z) : x ⊓ z < y ⊓ z

theorem wellFounded_lt_exact_sequence {α : Type u_1} [Lattice α] [IsModularLattice α] {β : Type u_2} {γ : Type u_3} [PartialOrder β] [Preorder γ] (h₁ : WellFounded fun x x_1 => x < x_1) (h₂ : WellFounded fun x x_1 => x < x_1) (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) : 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} [Lattice α] [IsModularLattice α] {β : Type u_2} {γ : Type u_3} [Preorder β] [PartialOrder γ] (h₁ : WellFounded fun x x_1 => x > x_1) (h₂ : WellFounded fun x x_1 => x > x_1) (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) : 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_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

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]

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)

@[simp]

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

@[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

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

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

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.

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

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

theorem Disjoint.disjoint_sup_right_of_disjoint_sup_left {α : Type u_1} [Lattice α] [OrderBot α] [IsModularLattice α] {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} [Lattice α] [OrderBot α] [IsModularLattice α] {a : α} {b : α} {c : α} (h : Disjoint b c) (hsup : Disjoint a (b ⊔ c)) : Disjoint (a ⊔ b) 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)

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)