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 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 αᵒᵈ

Equations

• (_ : IsWeakLowerModularLattice αᵒᵈ) = (_ : 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 αᵒᵈ

Equations

• (_ : IsWeakUpperModularLattice αᵒᵈ) = (_ : 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 α

Equations

• (_ : IsWeakUpperModularLattice α) = (_ : IsWeakUpperModularLattice α)

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

Equations

• (_ : IsLowerModularLattice αᵒᵈ) = (_ : 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 α

Equations

• (_ : IsWeakLowerModularLattice α) = (_ : IsWeakLowerModularLattice α)

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

Equations

• (_ : IsUpperModularLattice αᵒᵈ) = (_ : 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 αᵒᵈ

Equations

• (_ : 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]

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• (_ : IsLowerModularLattice α) = (_ : IsLowerModularLattice α)

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

Equations

• (_ : IsUpperModularLattice α) = (_ : 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

• One or more equations did not get rendered due to their size.

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 α

Equations

• (_ : IsModularLattice α) = (_ : 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 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 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 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

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

Equations

• (_ : IsModularLattice ↑(Set.Iic a)) = (_ : IsModularLattice ↑(Set.Iic a))

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

Equations

• (_ : IsModularLattice ↑(Set.Ici a)) = (_ : IsModularLattice ↑(Set.Ici a))

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

Equations

• (_ : ComplementedLattice ↑(Set.Iic a)) = (_ : ComplementedLattice ↑(Set.Iic a))

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

Equations

• (_ : ComplementedLattice ↑(Set.Ici a)) = (_ : ComplementedLattice ↑(Set.Ici a))