Representation of ortholattices by orthogonality relations

This file embeds an ortholattice with a join-dense subset V into the ortholattice of concepts of an orthogonality relation. The points are the nonzero elements of V, two points are orthogonal when one lies below the complement of the other, and a is represented by the points below it. This is the converse of the construction of an ortholattice from an orthogonality relation in Core/Order/Concept.lean.

Main definitions

• JoinDense V: every element of L is the least upper bound of the elements of V below it.
• InvolutiveCompl.Orthogonal V: the orthogonality relation a ≤ bᶜ on the nonzero elements of V.
• InvolutiveCompl.represent V: the concept of the points below an element.

Main results

• InvolutiveCompl.represent_le_iff, represent_inf, represent_compl, represent_sup: represent V is an ortholattice embedding for any join-dense V.

Implementation notes

The embedding uses only the order-reversing involution. The ortholattice laws are needed only for orthogonality to be irreflexive, which makes the concepts an ortholattice.

References

• [HM24]

def JoinDense {L : Type u_1} [Preorder L] (V : Set L) : Prop

A set V is join-dense in L when every element is the least upper bound of the elements of V below it.

Equations

• JoinDense V = ∀ (a : L), IsLUB (V ∩ Set.Iic a) a

@[reducible, inline]

abbrev InvolutiveCompl.Point {L : Type u_1} [Lattice L] [BoundedOrder L] (V : Set L) : Type u_1

The points of the representation over V are the nonzero elements of V.

Equations

• InvolutiveCompl.Point V = ↑(V \ {⊥})

def InvolutiveCompl.Orthogonal {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] (V : Set L) (a b : Point V) : Prop

Two points are orthogonal when one lies below the complement of the other ([HM24] Theorem 4.13, where compatibility is a ≰ ¬b).

Equations

• InvolutiveCompl.Orthogonal V a b = (↑a ≤ (↑b)ᶜ)

@[simp]

theorem InvolutiveCompl.orthogonal_iff {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {V : Set L} {a b : Point V} : Orthogonal V a b ↔ ↑a ≤ (↑b)ᶜ

instance InvolutiveCompl.instSymmPointOrthogonal {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] (V : Set L) : Std.Symm (Orthogonal V)

instance InvolutiveCompl.instIrreflPointOrthogonalOfIsOrtholattice {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] [IsOrtholattice L] (V : Set L) : Std.Irrefl (Orthogonal V)

def InvolutiveCompl.represent {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] (V : Set L) (a : L) : Concept (Point V) (Point V) (Orthogonal V)

represent V a is the concept whose extent is the points below a.

Equations

• InvolutiveCompl.represent V a = Concept.ofObjects (InvolutiveCompl.Orthogonal V) {b : InvolutiveCompl.Point V | ↑b ≤ a}

theorem InvolutiveCompl.upperPolar_Iic {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {V : Set L} (hV : JoinDense V) (x : L) : upperPolar (Orthogonal V) {c : Point V | ↑c ≤ x} = {d : Point V | x ≤ (↑d)ᶜ}

The upper polar of {c | c ≤ x} is {d | x ≤ dᶜ} (uses join-density at x).

theorem InvolutiveCompl.isExtent_Iic {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {V : Set L} (hV : JoinDense V) (a : L) : Order.IsExtent (Orthogonal V) {b : Point V | ↑b ≤ a}

{b ∈ V\{0} | b ≤ a} is a concept extent (uses join-density).

theorem InvolutiveCompl.represent_extent {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {V : Set L} (hV : JoinDense V) (a : L) : (represent V a).extent = {b : Point V | ↑b ≤ a}

The representation map's extent is exactly {b ∈ V\{0} | b ≤ a} (Thm 4.13).

The representation is an order-embedding preserving the lattice operations

theorem InvolutiveCompl.represent_le_iff {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {V : Set L} (hV : JoinDense V) {a a' : L} : represent V a ≤ represent V a' ↔ a ≤ a'

represent V preserves and reflects the order.

theorem InvolutiveCompl.represent_inf {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {V : Set L} (hV : JoinDense V) (a a' : L) : represent V (a ⊓ a') = represent V a ⊓ represent V a'

represent preserves meets (Concept inf is extent intersection).

theorem InvolutiveCompl.represent_top {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {V : Set L} (hV : JoinDense V) : represent V ⊤ = ⊤

represent preserves the top.

theorem InvolutiveCompl.represent_bot {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {V : Set L} (hV : JoinDense V) : represent V ⊥ = ⊥

represent preserves the bottom (the zero is excluded from the carrier).

theorem InvolutiveCompl.represent_compl {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {V : Set L} (hV : JoinDense V) (a : L) : represent V aᶜ = (represent V a)ᶜ

represent V sends complements to orthocomplements ([HM24] Theorem 4.13).

theorem InvolutiveCompl.represent_sup {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {V : Set L} (hV : JoinDense V) (a a' : L) : represent V (a ⊔ a') = represent V a ⊔ represent V a'

represent preserves joins (from ⊓- and ᶜ-preservation via De Morgan).