Orthocomplemented and orthomodular lattices

This file defines orthocomplemented lattices, or ortholattices, and orthomodular lattices. An ortholattice is a bounded lattice with an involutive, order-reversing complement ᶜ satisfying non-contradiction, a ⊓ aᶜ = ⊥, and so, by De Morgan, excluded middle, a ⊔ aᶜ = ⊤.

Heyting algebras and ortholattices weaken Boolean algebras in opposite directions. A Heyting algebra keeps distributivity and the pseudocomplement law a ⊓ b = ⊥ → b ≤ aᶜ but gives up the involution; an ortholattice keeps the involution and the complement laws but gives up distributivity.

An ortholattice is orthomodular when a ≤ b implies b = a ⊔ (aᶜ ⊓ b). Every modular ortholattice, and so every Boolean algebra, is orthomodular. The motivating example is the lattice of closed subspaces of a Hilbert space, Birkhoff and von Neumann's propositions of quantum mechanics. The regular propositions of Holliday and Mandelkern's epistemic compatibility frames form an ortholattice that is not orthomodular.

Main definitions

• IsOrtholattice α: the Prop mixin over [Lattice α] [BoundedOrder α] [InvolutiveCompl α] (the involutive antitone ᶜ of Core/Order/InvolutiveCompl.lean) adding non-contradiction.
• IsOrthomodularLattice α: an ortholattice satisfying the orthomodular law.

Main results

• IsModularLattice.toIsOrthomodularLattice: a modular ortholattice is orthomodular.

TODO

Upstream candidate for Mathlib/Order/Ortholattice.lean. The mathlib instance is the lattice of closed subspaces of a Hilbert space, in Mathlib/Analysis/InnerProductSpace/Projection/: ClosedSubmodule.orthogonal is an InvolutiveCompl by ClosedSubmodule.orthogonal_orthogonal_eq and ClosedSubmodule.orthogonal_le, non-contradiction is ClosedSubmodule.inf_orthogonal_eq_bot, and orthomodularity is Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection.

References

• [BvN36]
• [HM24]

class IsOrtholattice (α : Type u_2) [Lattice α] [BoundedOrder α] [InvolutiveCompl α] : Prop

An ortholattice is a bounded lattice whose involutive complement satisfies non-contradiction, a ⊓ aᶜ ≤ ⊥ ([HM24] Definition 3.3). It is the sibling of mathlib's ComplementedLattice with the complement chosen by ᶜ. Excluded middle follows by De Morgan, IsOrtholattice.top_le_sup_compl.

• inf_compl_le_bot (a : α) : a ⊓ aᶜ ≤ ⊥

  Every element is disjoint from its complement, a ⊓ aᶜ ≤ ⊥.

@[simp]

theorem IsOrtholattice.inf_compl_eq_bot {α : Type u_1} [Lattice α] [BoundedOrder α] [InvolutiveCompl α] [IsOrtholattice α] (a : α) : a ⊓ aᶜ = ⊥

theorem IsOrtholattice.top_le_sup_compl {α : Type u_1} [Lattice α] [BoundedOrder α] [InvolutiveCompl α] [IsOrtholattice α] (a : α) : ⊤ ≤ a ⊔ aᶜ

Excluded middle, the De Morgan dual of non-contradiction.

@[simp]

theorem IsOrtholattice.sup_compl_eq_top {α : Type u_1} [Lattice α] [BoundedOrder α] [InvolutiveCompl α] [IsOrtholattice α] (a : α) : a ⊔ aᶜ = ⊤

theorem IsOrtholattice.isCompl_compl {α : Type u_1} [Lattice α] [BoundedOrder α] [InvolutiveCompl α] [IsOrtholattice α] (a : α) : IsCompl a aᶜ

theorem IsOrtholattice.disjoint_compl_right {α : Type u_1} [Lattice α] [BoundedOrder α] [InvolutiveCompl α] [IsOrtholattice α] (a : α) : Disjoint a aᶜ

theorem IsOrtholattice.disjoint_of_le_compl {α : Type u_1} [Lattice α] [BoundedOrder α] [InvolutiveCompl α] [IsOrtholattice α] {a b : α} (h : a ≤ bᶜ) : Disjoint a b

Orthogonal elements are disjoint. The converse is the pseudocomplement law, which holds only in Boolean algebras ([HM24] Proposition 3.7).

@[instance 100]

instance IsOrtholattice.toComplementedLattice {α : Type u_1} [Lattice α] [BoundedOrder α] [InvolutiveCompl α] [IsOrtholattice α] : ComplementedLattice α

Every ortholattice is complemented, with ᶜ as the chosen complement.

@[instance 100]

instance BooleanAlgebra.toIsOrtholattice {α : Type u_1} [BooleanAlgebra α] : IsOrtholattice α

Every Boolean algebra is orthocomplemented.

Orthomodular lattices

class IsOrthomodularLattice (α : Type u_2) [Lattice α] [BoundedOrder α] [InvolutiveCompl α] extends IsOrtholattice α : Prop

An orthomodular lattice is an ortholattice in which a ≤ b implies b = a ⊔ (aᶜ ⊓ b) ([HM24] Definition 3.5). We only require ≤, since the other inequality holds in every lattice.

• inf_compl_le_bot (a : α) : a ⊓ aᶜ ≤ ⊥
• le_sup_compl_inf_of_le {a b : α} : a ≤ b → b ≤ a ⊔ aᶜ ⊓ b

  If a ≤ b, then b ≤ a ⊔ (aᶜ ⊓ b).

@[instance 100]

instance IsModularLattice.toIsOrthomodularLattice {α : Type u_1} [Lattice α] [BoundedOrder α] [InvolutiveCompl α] [IsOrtholattice α] [IsModularLattice α] : IsOrthomodularLattice α

A modular ortholattice is orthomodular ([HM24] footnote 4), and so, through DistribLattice, is every Boolean algebra.

theorem sup_compl_inf_of_le {α : Type u_1} [Lattice α] [BoundedOrder α] [InvolutiveCompl α] [IsOrthomodularLattice α] {a b : α} (h : a ≤ b) : a ⊔ aᶜ ⊓ b = b