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

• IsModularLattice: Modular lattices. Lattices where a ≤ c → (a ⊔ b) ⊓ c = a ⊔ (b ⊓ c)≤ c → (a ⊔ b) ⊓ c = a ⊔ (b ⊓ c)→ (a ⊔ b) ⊓ c = a ⊔ (b ⊓ c)⊔ b) ⊓ c = a ⊔ (b ⊓ c)⊓ c = a ⊔ (b ⊓ c)⊔ (b ⊓ c)⊓ 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]⊓ b, a] and [b, a ⊔ b]⊔ 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⊓ z) ⊔ (y ⊓ z) = ((x ⊓ z) ⊔ y) ⊓ z⊔ (y ⊓ z) = ((x ⊓ z) ⊔ y) ⊓ z⊓ z) = ((x ⊓ z) ⊔ y) ⊓ z⊓ z) ⊔ y) ⊓ z⊔ y) ⊓ z⊓ 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

ink

class IsWeakUpperModularLattice (α : Type u_1) [inst : Lattice α] : Prop

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

  covby_sup_of_inf_covby_covby : ∀ {a b : α}, a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b

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

ink

class IsWeakLowerModularLattice (α : Type u_1) [inst : Lattice α] : Prop

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

  inf_covby_of_covby_covby_sup : ∀ {a b : α}, a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a

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

ink

class IsUpperModularLattice (α : Type u_1) [inst : Lattice α] : Prop

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

  covby_sup_of_inf_covby : ∀ {a b : α}, a ⊓ b ⋖ a → b ⋖ a ⊔ b

An upper modular lattice, aka semimodular lattice, is a lattice where a ⊔ b⊔ b covers a and b if either a or b covers a ⊓ b⊓ b.

ink

class IsLowerModularLattice (α : Type u_1) [inst : Lattice α] : Prop

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

  inf_covby_of_covby_sup : ∀ {a b : α}, a ⋖ a ⊔ b → a ⊓ b ⋖ b

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

ink

class IsModularLattice (α : Type u_1) [inst : Lattice α] : Prop

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

  sup_inf_le_assoc_of_le : ∀ {x : α} (y : α) {z : α}, x ≤ z → (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z

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

ink

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

ink

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

ink

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

Alias of covby_sup_of_inf_covby_of_inf_covby_left.

ink

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

Alias of covby_sup_of_inf_covby_of_inf_covby_right.

ink

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

Equations

• @instIsWeakLowerModularLatticeOrderDualLattice = @instIsWeakLowerModularLatticeOrderDualLattice.proof_1

ink

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

ink

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

ink

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

Alias of inf_covby_of_covby_sup_of_covby_sup_left.

ink

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

Alias of inf_covby_of_covby_sup_of_covby_sup_right.

ink

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

Equations

• @instIsWeakUpperModularLatticeOrderDualLattice = @instIsWeakUpperModularLatticeOrderDualLattice.proof_1

ink

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

ink

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

ink

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

Alias of covby_sup_of_inf_covby_left.

ink

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

Alias of covby_sup_of_inf_covby_right.

ink

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

Equations

• @IsUpperModularLattice.to_isWeakUpperModularLattice = @IsUpperModularLattice.to_isWeakUpperModularLattice.proof_1

ink

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

Equations

• @instIsLowerModularLatticeOrderDualLattice = @instIsLowerModularLatticeOrderDualLattice.proof_1

ink

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

ink

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

ink

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

Alias of inf_covby_of_covby_sup_left.

ink

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

Alias of inf_covby_of_covby_sup_right.

ink

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

Equations

• @IsLowerModularLattice.to_isWeakLowerModularLattice = @IsLowerModularLattice.to_isWeakLowerModularLattice.proof_1

ink

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

Equations

• @instIsUpperModularLatticeOrderDualLattice = @instIsUpperModularLatticeOrderDualLattice.proof_1

ink

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

ink

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

ink

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

ink

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

Equations

• @instIsModularLatticeOrderDualLattice = @instIsModularLatticeOrderDualLattice.proof_1

ink

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

ink

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

ink

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

ink

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

ink

theorem wellFounded_lt_exact_sequence {α : Type u_3} [inst : Lattice α] [inst : IsModularLattice α] {β : Type u_1} {γ : Type u_2} [inst : PartialOrder β] [inst : 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.

ink

theorem wellFounded_gt_exact_sequence {α : Type u_3} [inst : Lattice α] [inst : IsModularLattice α] {β : Type u_1} {γ : Type u_2} [inst : Preorder β] [inst : 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.

ink

@[simp]

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

ink

@[simp]

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

ink

def infIccOrderIsoIccSup {α : Type u_1} [inst : Lattice α] [inst : IsModularLattice α] (a : α) (b : α) : ↑(Set.Icc (a ⊓ b) a) ≃o ↑(Set.Icc b (a ⊔ b))

The diamond isomorphism between the intervals [a ⊓ b, a]⊓ b, a] and [b, a ⊔ b]⊔ b]

Equations

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

def infIooOrderIsoIooSup {α : Type u_1} [inst : Lattice α] [inst : IsModularLattice α] (a : α) (b : α) : ↑(Set.Ioo (a ⊓ b) a) ≃o ↑(Set.Ioo b (a ⊔ b))

The diamond isomorphism between the intervals ]a ⊓ b, a[⊓ b, a[ and }b, a ⊔ b[⊔ b[.

Equations

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

ink

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

Equations

• @IsModularLattice.to_isLowerModularLattice = @IsModularLattice.to_isLowerModularLattice.proof_1

ink

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

Equations

• @IsModularLattice.to_isUpperModularLattice = @IsModularLattice.to_isUpperModularLattice.proof_1

ink

def IsCompl.IicOrderIsoIci {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] [inst : 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.

ink

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

ink

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

Equations

• @DistribLattice.instIsModularLatticeToLattice = @DistribLattice.instIsModularLatticeToLattice.proof_1

ink

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

ink

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

ink

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

Equations

• @IsModularLattice.isModularLattice_Iic = @IsModularLattice.isModularLattice_Iic.proof_1

ink

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

Equations

• @IsModularLattice.isModularLattice_Ici = @IsModularLattice.isModularLattice_Ici.proof_1

ink

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

Equations

• @IsModularLattice.complementedLattice_Iic = @IsModularLattice.complementedLattice_Iic.proof_1

ink

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

Equations

• @IsModularLattice.complementedLattice_Ici = @IsModularLattice.complementedLattice_Ici.proof_1