Representation of ortholattices by orthoframes

[HM24] Theorem 4.13: every complete ortholattice is isomorphic to Orthoframe.Regular of its canonical orthoframe; every finite ortholattice via its join-irreducibles (Corollary 4.14). This is the converse of the Orthoframe layer (which gives frame → ortholattice).

Translation: our Orthoframe carries the orthogonality relation, so the paper's compatibility a ◇ b ↔ a ≰ ¬b becomes orthogonality a ⊥ b ↔ a ≤ bᶜ. Points are the nonzero elements of a join-dense V, and the representation map is a ↦ {b ∈ V\{0} | b ≤ a}.

Status

Theorem 4.13 is complete and sorry-free. The construction (ofOrtholattice), the extent characterization, the full ortholattice embedding (⊓ ⊔ ¬ ⊤ ⊥ preserved, order-reflecting), and — for a CompleteOrthocomplementedLattice — the isomorphism representation : L ≃o (ofOrtholattice V).Regular over any join-dense V. The orthocomplement preservation (represent_compl, the heart) falls out of the upperPolar computation upperPolar_Iic; no De Morgan over the join is needed. Corollary 4.14 (representationFinite) specialises the isomorphism to a well-founded (e.g. finite) ortholattice, taking V to be the join-irreducibles.

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

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

Equations

• JoinDense V = ∀ (a : L), IsLUB {b : L | b ∈ V ∧ b ≤ a} a

@[reducible, inline]

abbrev Orthoframe.Point {L : Type u_1} [OrthocomplementedLattice L] (V : Set L) : Type u_1

Points of the canonical orthoframe of (L, V): the nonzero elements of V.

Equations

• Orthoframe.Point V = { a : L // a ∈ V ∧ a ≠ ⊥ }

def Orthoframe.ofOrtholattice {L : Type u_1} [OrthocomplementedLattice L] (V : Set L) : Orthoframe (Point V)

The canonical orthoframe ([HM24] Theorem 4.13): the nonzero elements of V, orthogonal when a ≤ bᶜ (incompatible).

Equations

• Orthoframe.ofOrtholattice V = { ortho := fun (a b : Orthoframe.Point V) => ↑a ≤ (↑b)ᶜ, ortho_symm := ⋯, ortho_irrefl := ⋯ }

@[simp]

theorem Orthoframe.ofOrtholattice_ortho {L : Type u_1} [OrthocomplementedLattice L] {V : Set L} (a b : Point V) : (ofOrtholattice V).ortho a b ↔ ↑a ≤ (↑b)ᶜ

def Orthoframe.represent {L : Type u_1} [OrthocomplementedLattice L] (V : Set L) (a : L) : (ofOrtholattice V).Regular

The representation map a ↦ {b ∈ V\{0} | b ≤ a}, as a concept.

Equations

• Orthoframe.represent V a = Concept.ofObjects (Orthoframe.ofOrtholattice V).ortho {b : Orthoframe.Point V | ↑b ≤ a}

theorem Orthoframe.upperPolar_Iic {L : Type u_1} [OrthocomplementedLattice L] {V : Set L} (hV : JoinDense V) (x : L) : upperPolar (ofOrtholattice V).ortho {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 Orthoframe.isExtent_Iic {L : Type u_1} [OrthocomplementedLattice L] {V : Set L} (hV : JoinDense V) (a : L) : Order.IsExtent (ofOrtholattice V).ortho {b : Point V | ↑b ≤ a}

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

theorem Orthoframe.represent_extent {L : Type u_1} [OrthocomplementedLattice 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 Orthoframe.represent_le_iff {L : Type u_1} [OrthocomplementedLattice L] {V : Set L} (hV : JoinDense V) {a a' : L} : represent V a ≤ represent V a' ↔ a ≤ a'

represent is an order-embedding: represent V a ≤ represent V a' ↔ a ≤ a'.

theorem Orthoframe.represent_inf {L : Type u_1} [OrthocomplementedLattice 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 Orthoframe.represent_top {L : Type u_1} [OrthocomplementedLattice L] {V : Set L} (hV : JoinDense V) : represent V ⊤ = ⊤

represent preserves the top.

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

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

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

Orthocomplement preservation ([HM24] Theorem 4.13). The orthocomplement of represent V a has extent upperPolar ortho {b ≤ a}, which upperPolar_Iic computes as {d | a ≤ dᶜ} = {d | d ≤ aᶜ} — exactly the extent of represent V aᶜ. No De Morgan over the join is needed: the upperPolar computation already carries the argument.

theorem Orthoframe.represent_sup {L : Type u_1} [OrthocomplementedLattice 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).

The representation isomorphism (complete case, Theorem 4.13)

theorem Orthoframe.represent_surjective {L : Type u_2} [CompleteOrthocomplementedLattice L] {V : Set L} (hV : JoinDense V) (c : (ofOrtholattice V).Regular) : represent V (sSup (Subtype.val '' c.extent)) = c

Surjectivity (the ← of Theorem 4.13): every concept is represent V a, taking a to be the join of the underlying elements of its extent.

theorem Orthoframe.sSup_represent_extent {L : Type u_2} [CompleteOrthocomplementedLattice L] {V : Set L} (hV : JoinDense V) (a : L) : sSup (Subtype.val '' (represent V a).extent) = a

The join of represent V a's extent recovers a (the → of Theorem 4.13).

def Orthoframe.representation {L : Type u_2} [CompleteOrthocomplementedLattice L] {V : Set L} (hV : JoinDense V) : L ≃o (ofOrtholattice V).Regular

The representation isomorphism ([HM24] Theorem 4.13): a complete ortholattice is order-isomorphic to Orthoframe.Regular of its canonical orthoframe over any join-dense V.

Equations

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

Corollary 4.14 — the finite case via join-irreducibles

theorem Orthoframe.joinDense_supIrred {L : Type u_2} [CompleteOrthocomplementedLattice L] [WellFoundedLT L] : JoinDense {a : L | SupIrred a}

The join-irreducibles are join-dense in a well-founded ortholattice (every finite ortholattice is well-founded): each element is the least upper bound of the join-irreducibles below it, by exists_supIrred_decomposition.

def Orthoframe.representationFinite {L : Type u_2} [CompleteOrthocomplementedLattice L] [WellFoundedLT L] : L ≃o (ofOrtholattice {a : L | SupIrred a}).Regular

Corollary 4.14 ([HM24]): a finite (more generally, well-founded) ortholattice is order-isomorphic to Orthoframe.Regular of the orthoframe on its join-irreducibles.

Equations

• Orthoframe.representationFinite = Orthoframe.representation ⋯