1 Introduction

Different quantum structures emphasize different aspects of quantum reasoning. In this paper, we focus on two types of quantum structures. One structure is a complete orthomodular lattice, whose points are viewed as testable properties of a quantum system. While these structures are natural settings for reasoning about the properties of a system, they leave implicit important quantum structures, such as quantum actions. The other structure is the quantum dynamic algebra, a quantale augmented with an orthocomplementation. These structures were proposed in [2] as providing a type of algebraic quantum structure that makes actions first-class citizens. A quantale is a complete lattice with an additional semi-group (often a monoidal) operator, and this additional operator is viewed as function composition, with the lattice points abstractions of functions. (Please refer to [5] for a detailed survey of quantales.) In this way, quantales are often described as abstractions of operator algebras such as C -algebras, though their connection to orthomodular lattices or even the more restrictive Hilbert lattices (lattice of closed subspaces of a Hilbert space) has received little attention.

The goal of this paper is to compare the quantale with the orthomodular lattice, and we do so by establishing a categorical equivalence between complete orthomodular lattices and orthomodular dynamic algebras, a type of quantum dynamic algebra. This equivalence clarifies how dynamics arises from orthomodular or Hilbert lattices, and establishes a clearer connection between quantales and orthomodular lattices, thus clarifying how they can be used for quantum reasoning.

The best connection we have found between orthomodular lattices and quantum dynamic algebras is in [2]. The goal of that work was to connect to quantum dynamic frames, a graph-like counterpart to the Hilbert lattice. But it did more to suggest connections than to establish rigorous equivalence, and it did not involve categorical structure.

Categorical equivalence along with categorical duality have been extensively used to establish meaningful relationships among different structures and to help transfer results about one structure to results about another. A categorical equivalence consists of a pair of functors from each category to the other such that the composition of the two functors (composed in either way) is naturally isomorphic to the corresponding identity functor. A duality is an equivalence between one category and the opposite of another category, that is, where in the second category all morphisms are reversed.

Categorical equivalences with quantum significance include those between quantum geometries and quantum lattices (between Hilbert geometries and propositional systems, as well as projective geometries and projective lattices), as given in [7], and significant categorical dualities include those between quantum lattices and quantum graph-like structures (between Piron lattices and quantum dynamic algebras), as given in [3]. Our equivalence connects quantales to these structures by connecting them to a class of lattices that includes propositional systems and Piron lattices.

The paper is organized as follows. In Section 2, we introduce the categories of complete orthomodular lattices and orthomodular dynamic algebras. In Section 3, we define the functors that make up the categorical equivalence. These involve defining translations from each object in one category to an object in the other category, and mapping morphisms in one to morphisms in the other. In Section 4, we prove the functors defined in the previous section form a categorical equivalence. This involves defining appropriate natural isomorphisms between the compositions of the functors and the identity functors. Finally, in Section 5, we conclude the paper with some remarks and suggestions for future work.

2 The Categories

2.1 The Category \(\mathbb {L}\) of Complete Orthomodular Lattices

Definition 1

Consider a tuple \(\mathfrak {L} = (L , {\leq } , -^{\bot } )\) where L is a non-empty set, ≤⊆ L × L is a partial order and − : LL is a function. It is an ortho-lattice, if it satisfies (1)–(3) below. It is a complete orthomodular lattice, if it satisfies (1)–(5).

  1. 1.

    (L,≤) is a lattice: any p, qL have a least upper bound pq in L, called the join, and a greatest lower bound pq in L, called the meet;

  2. 2.

    there are O, IL such that OpI, for each pL;

  3. 3.

    is an orthocomplementation, i.e. for any p, qL;

    1. (a)

      pp = O and pp = I;

    2. (b)

      pqq p ;

    3. (c)

      p ⊥⊥ = p;

  4. 4.

    (L,≤) is a complete lattice: for any {p i LiI}, they have a join \(\bigvee \{ p_{i} \in L \mid i \in I \}\) and a meet \(\bigwedge \{ p_{i} \in L \mid i \in I \}\) in L;

  5. 5.

    orthomodularity holds, i.e. for any p, qL, pq implies that p = q ∧ (pq ).

In an ortho-lattice \(\mathfrak {L} = (L , {\leq } , -^{\bot } )\), for each pL, we can define an important pair of operations called the Sasaki projection (onto p) and Sasaki hook (from p) [6]:

$$\begin{array}{lllllll} f_{p} : L \rightarrow L :: q \mapsto p \wedge (p^{\bot} \vee q ) , & f^{p} : L \rightarrow L :: q \mapsto p^{\bot} \vee (p \wedge q ) . \end{array}$$

A crucial fact about this pair of order-preserving maps is that \(\mathfrak {L}\) is orthomodular (5) if and only if, for every pL, f p is left adjoint to f p [4]. Therefore, in an orthomodular lattice, Sasaki projections preserve (arbitrary) joins.

Lemma 1

In a complete orthomodular lattice \(\mathfrak {L} = (L , {\leq } , -^{\bot } )\) , for any pL and KL , \(f_{p} (\bigvee _{q \in K} q) = \bigvee _{q \in K} f_{p} (q )\) .

Definition 2

An ortho-lattice isomorphism, or \(\mathbb {L}\)-morphism, from an ortho-lattice \(\mathfrak {L}_{1} = (L_{1} , {\leq _{1}} , {-}^{\bot _{1}} )\) to \(\mathfrak {L}_{2} = (L_{2} , {\leq _{2}} , {-}^{\bot _{2}} )\) is a function k : L 1L 2 such that, for any p 1, q 1L 1,

  1. 6.

    k is a bijection;

  2. 7.

    p 11 q 1k(p 1) ≤2 k(q 1);

  3. 8.

    \(k (p_{1}^{\bot _{1}}) = (k (p_{1}) )^{\bot _{2}}\).

Theorem 1

Complete orthomodular lattices equipped with ortho-lattice isomorphisms form a category \(\mathbb {L}\) .

Proof

This proof is routine, and hence we omit details. □

2.2 The Category \(\mathbb {Q}\) of Orthomodular Dynamic Algebras

In this section, we define the category of orthomodular dynamic algebras. Roughly speaking, an orthomodular dynamic algebra is an enrichment of a quantale. We first recall the definition of a quantale and introduce some other notions, and then we give the definition of the quantum dynamic algebra.

Definition 3

A quantale is a tuple \((Q, {\sqsubseteq } , {\cdot } )\), such that

  1. 1.

    \((Q , {\sqsubseteq })\) is a complete lattice, that is, a partially ordered set, where every (potentially infinite) subset A has a least upper bound \(\bigsqcup A\) called the join of A;Footnote 1

  2. 2.

    ⋅ is associative: for any x, y, zQ, (xy) ⋅ z = x ⋅ (yz);

  3. 3.

    ⋅ distributes over \({\bigsqcup }\): for any xQ and KQ,

    $$x \cdot \bigsqcup K = \bigsqcup \{ x \cdot y \mid y \in K \} \text{ and } \left( \bigsqcup K \right) \cdot x = \bigsqcup \{ y \cdot x \mid y \in K \} ; $$

Definition 4

A generalized dynamic algebra is a tuple \(\mathfrak {Q} = (Q , {\bigsqcup } , {\cdot } , {\sim } )\) such that Q is a non-empty set, and all of \({\bigsqcup } : \&\#x2118; (Q ) \rightarrow Q\), ⋅ : Q × QQ and ∼ : QQ are functions.

The following are some constructions on a generalized dynamic algebra.

$$\begin{array}{llllll} {\sqsubseteq} & \overset{\text{def}}{=} \left\{ (x,y) \in Q \times Q \mid \bigsqcup \{ x , y \} = y \right\} \\ \mathcal{P}_{\mathfrak{Q}} & \overset{\text{def}}{=} \{ \sim x \mid x \in Q \} \\ \bigvee X & \overset{\text{def}}{=} \sim \sim \bigsqcup X \text{, for any } X \subseteq \mathcal{P}_{\mathfrak{Q}} \\ \bigwedge X & \overset{\text{def}}{=} \sim \bigsqcup \{ \sim x \mid x \in X \} \text{, for any } X \subseteq \mathcal{P}_{\mathfrak{Q}} \\ {\preceq} & \overset{\text{def}}{=} \left\{ (p,q) \in \mathcal{P}_{\mathfrak{Q}} \times \mathcal{P}_{\mathfrak{Q}} \mid \bigvee \{ p , q \} = q \right\} \\ \ulcorner x \urcorner & \overset{\text{def}}{=} \lambda y. \sim \sim (x \cdot y ) \\ {\equiv} & \overset{\text{def}}{=} \{ (x,y) \in Q \times Q \mid \ulcorner x \urcorner (p) = \ulcorner y \urcorner (p) \text{, for each } p \in \mathcal{P}_{\mathfrak{Q}} \} \\ \mathcal{T}_{\mathfrak{Q}} & \overset{\text{def}}{=} \{ x \in Q \mid x = p_{1} \cdot {\cdots} \cdot p_{n} \text{, for some } n \in \mathbb{N}^{+} \text{ and } p_{1} , {\dots} , p_{n} \in \mathcal{P}_{\mathfrak{Q}} \} \end{array}$$

Note that \(\mathcal {T}_{\mathfrak {Q}}\) is the smallest subset of Q containing \(\mathcal {P}_{\mathfrak {Q}}\) which is closed under the operation ⋅.

In the following, for simplicity, we write xy for \(\bigsqcup \{ x, y \}\), xy for \(\bigvee \{ x , y \}\) and xy for \(\bigwedge \{ x , y \}\); and we may omit the subscripts in \(\mathcal {P}_{\mathfrak {Q}}\) and \(\mathcal {T}_{\mathfrak {Q}}\).

Definition 5

An orthomodular dynamic algebra is a generalized dynamic algebra \(\mathfrak {Q} = (Q , {\bigsqcup } , {\cdot } , \sim )\) such that

  1. 9.

    \((Q, {\sqsubseteq } , {\cdot } )\) is a quantale, and \(\bigsqcup \) is the arbitrary join.Footnote 2

  2. 10.

    \((\mathcal {P} , {\preceq } , \sim )\) is a complete orthomodular lattice;

  3. 11.

    If X is such that

    1. (a)

      \(\mathcal {P} \subseteq X\subseteq Q\),

    2. (b)

      X is closed under the operation ⋅, and

    3. (c)

      X is closed under \(\bigsqcup \), by which we mean, for any \(\mathcal {X}\in \&\#x2118;(X) \), \(\bigsqcup \mathcal {X}\in X\).

    Then X = Q (minimality);

  4. 12.

    for any \(X , Y \subseteq \mathcal {T} \), \(\bigsqcup X = \bigsqcup Y\), if and only if X = Y (sets);

  5. 13.

    for any \(x,y\in \mathcal {T} \), x = y if and only if xy (completeness);

  6. 14.

    for any \(p , q \in \mathcal {P} \), \(\ulcorner p \urcorner (q) = f_{p}(q)\), i.e. ∼∼ (pq) = p ∧ (∼ pq) (Sasaki projection);

  7. 15.

    \(\ulcorner x \urcorner (y) = \ulcorner x \urcorner (\sim \sim y)\), for each x, yQ (composition).

We now prove two useful lemmas. The first one says that there is a normal form for each element in an orthomodular dynamic algebra.

Lemma 2

For each xQ , there is a unique set \(\{ x_{i} \mid i \in I \} \subseteq \mathcal {T} \) such that \(x = \bigsqcup \{ x_{i} \mid i \in I \}\) .

Proof

Recall that by (9), \({\bigsqcup }\) is the arbitrary join of the complete lattice \((Q , {\sqsubseteq })\), and hence

  1. (i)

    \(\bigsqcup \{ x \} = x\), for each xQ;

  2. (ii)

    \(\bigsqcup \{ \bigsqcup \{ x_{(i , j)} \mid j \in J_{i} \} \mid i \in I \} = \bigsqcup \{ x_{(i , j)} \mid (i,j) \in \bigcup _{i \in I} (\{ i \} \times J_{i}) \}\), for any \(\{ x_{(i , j)} \in Q \mid (i,j) \in \bigcup _{i \in I} (\{ i \} \times J_{i}) \}\).

To prove existence, let ZQ consist of each x in Q for which there is a set \(\{ x_{i} \mid i \in I \} \subseteq \mathcal {T} \) such that \(x = \bigsqcup \{ x_{i} \mid i \in I \}\). We will show that Z = Q by showing that Z satisfies each of the three conditions in (11).

  • Clearly \(\mathcal {P}\subseteq \mathcal {T}\) and \(\mathcal {T} \subseteq Z\), and hence \(\mathcal {P} \subseteq Z\).

  • Suppose y, zZ, and let x = yz. We wish to show that xZ. Now \(y = \bigsqcup \{ y_{i} \mid i \in I \}\) and \(z = \bigsqcup \{ z_{j} \mid j \in J \}\), for some \(\{ y_{i} \mid i \in I \} \subseteq \mathcal {T} \) and \(\{ z_{j} \mid j \in J \} \subseteq \mathcal {T} \). Thus

    $$\begin{array}{@{}rcl@{}} x = y \cdot z &= \ & \bigsqcup \{ y_{i} \mid i \in I \} \cdot \bigsqcup \{ z_{j} \mid j \in J \} \\ &= \ & \bigsqcup \left\{ \bigsqcup \{ y_{i} \mid i \in I \} \cdot z_{j} \mid j \in J \right\} \qquad \qquad\qquad\qquad\qquad\quad\qquad\!\!\text{(by (3))}\\ &= \ & \bigsqcup \left\{ \bigsqcup \{ y_{i} \cdot z_{j} \mid i \in I \} \mid j \in J \right\} \qquad\qquad\qquad\qquad\qquad\qquad\quad\!\!\text{(by (3))}\\ &= \ & \bigsqcup \{ y_{i} \cdot z_{j} \mid (i , j ) \in I \times J \}\qquad\qquad\qquad\qquad\qquad\qquad\qquad\quad\text{(by (ii))} \end{array} $$

    Note that \(\{ y_{i} \cdot z_{j} \mid (i , j ) \in I \times J \} \subseteq \mathcal {T} \).

  • Suppose \(\{ x^{\prime }_{i} \mid i \in I \} \in \&\#x2118;(Z)\), and let \(x = \bigsqcup \{ x^{\prime }_{i} \mid i \in I \}\). We wish to show that xZ. Now, for each iI, \(x^{\prime }_{i} = \bigsqcup \{ y_{(i,j) } \mid j \in J_{i} \}\) for some \(\{ y_{(i,j) } \mid j \in J_{i} \} \subseteq \mathcal {T} \). Thus

    $$x = \bigsqcup \{ x^{\prime}_{i} \! \mid \! i \! \in \! I \} = \bigsqcup \left\{ \bigsqcup \{ y_{(i,j) } \! \mid \! j \! \in J_{i} \} \! \mid \! i \! \in \! I \right\} = \bigsqcup \left\{ y_{(i,j) } \! \mid \! (i,j) \! \in \! \bigcup_{i \in I} (\{ i \} \times J_{i} ) \right\} $$

    where the third equality is by (ii). Note that \(\left \{ y_{(i,j) } \mid (i,j) \in \bigcup _{i \in I} (\{ i \} \times J_{i} ) \right \} \subseteq \mathcal {T} \).

Thus by (11), Z = Q, i.e., the desired existence property holds for every xQ.

Uniqueness follows directly from (12). □

Since \({\bigsqcup }\) is the join in the complete lattice \((Q , {\sqsubseteq })\), this lemma means that the elements of \(\mathcal {T}\) are the atoms of this lattice and this lattice is atomistic.

The second lemma shows that (14) can be generalized.

Lemma 3

For any \(n \in \mathbb {N}^{+}\) and \(p_{1} , {\dots } , p_{n} \in \mathcal {P} \) , \(\ulcorner p_{1} \cdot {\cdots } \cdot p_{n} \urcorner = \ulcorner p_{1} \urcorner \circ {\cdots } \circ \ulcorner p_{n} \urcorner \) . In particular, \(\ulcorner p_{1} \cdot {\cdots } \cdot p_{n} \urcorner = \ulcorner p_{1} \urcorner \circ {\cdots } \circ \ulcorner p_{n} \urcorner = f_{p_{1}} \circ {\cdots } \circ f_{p_{n}}\) on \(\mathcal {P}\) .

Proof

We use induction on n to show that \(\ulcorner p_{1} \cdot {\cdots } \cdot p_{n} \urcorner = \ulcorner p_{1} \urcorner \circ {\cdots } \circ \ulcorner p_{n} \urcorner \).

Base Step: :

n = 1. This case is trivial.

Induction Step: :

n = k + 1. For each xQ,

$$\begin{array}{@{}rcl@{}} \ulcorner p_{1} \cdot {\cdots} \cdot p_{k} \cdot p_{k+1} \urcorner (x) &= \ & \sim \sim (p_{1} \cdot {\cdots} \cdot p_{k} \cdot p_{k+1} \cdot x ) \\ &= \ & \ulcorner p_{1} \urcorner (p_{2} \cdot {\cdots} \cdot p_{k} \cdot p_{k+1} \cdot x ) \\ &= \ & \ulcorner p_{1} \urcorner (\sim \sim (p_{2} \cdot {\cdots} \cdot p_{k} \cdot p_{k+1} \cdot x ) ) \quad(\text{by (15)}) \\ &= \ & \ulcorner p_{1} \urcorner (\ulcorner p_{2} \cdot {\cdots} \cdot p_{k} \cdot p_{k+1} \urcorner (x) ) \\ &= \ & \ulcorner p_{1} \urcorner ((\ulcorner p_{2} \urcorner \circ {\cdots} \circ \ulcorner p_{k} \urcorner \circ \ulcorner p_{k+1} \urcorner ) (x) ) \qquad(\text{IH}) \\ &= \ & (\ulcorner p_{1} \urcorner \circ {\cdots} \circ \ulcorner p_{k} \urcorner \circ \ulcorner p_{k+1} \urcorner ) (x) \end{array} $$

This finishes the proof by induction.

Note that, for each \(p \in \mathcal {P}\), by (14) the restriction of \(\ulcorner p \urcorner \) on \(\mathcal {P}\) is the same function as f p . Therefore, \(\ulcorner p_{1} \cdot {\cdots } \cdot p_{n} \urcorner = \ulcorner p_{1} \urcorner \circ {\cdots } \circ \ulcorner p_{n} \urcorner = f_{p_{1}} \circ {\cdots } \circ f_{p_{n}}\) on \(\mathcal {P}\). □

Definition 6

A function 𝜃 : Q 1Q 2 is a \(\mathbb {Q}\)-morphism from an orthomodular dynamic algebra \(\mathfrak {Q}_{1} = (Q_{1} , {\bigsqcup _{1}} , \cdot _{1} , \sim _{1} )\) to \(\mathfrak {Q}_{2} = (Q_{2} , {\bigsqcup _{2}} , \cdot _{2} , \sim _{2} )\), if:

  1. 16.

    𝜃 restricted to \(\mathcal {P}_{1} = \{\sim x\mid x\in Q_{1}\}\) is an ortho-lattice isomorphism from \((\mathcal {P}_{1} , {\!\preceq _{1}} , \!\sim _{1})\) to \((\mathcal {P}_{2} , {\preceq _{2}} , \sim _{2} )\);

  2. 17.

    𝜃 preserves \(\bigsqcup \) and ⋅, i.e. for any \(A_{1} \subseteq \mathcal {Q}_{1}\) and \(x_{1} , y_{1} \in \mathcal {Q}_{1}\),

    \(\theta (\bigsqcup _{1} A_{1}) = \bigsqcup _{2} \theta [A_{1}]\) 𝜃(x 11 y 1) = 𝜃(x 1) ⋅2 𝜃(x 2)

Theorem 2

Orthomodular dynamic algebras equipped with \(\mathbb {Q}\) -morphisms form a category \(\mathbb {Q}\) .

Proof

Let the identity arrows be the identity maps, and arrow composition be function compositions.

It is obvious that the identity maps are \(\mathbb {Q}\)-morphisms, and function compositions of \(\mathbb {Q}\)-morphisms are still \(\mathbb {Q}\)-morphisms and satisfy associativity.

3 The Functors

3.1 From Complete Orthomodular Lattices to Orthomodular Dynamic Algebras

In this subsection, we define a functor \(\mathbf {F} : \mathbb {L} \rightarrow \mathbb {Q}\).

Mapping of Objects

Fix a complete orthomodular lattice \(\mathfrak {L} = (L , {\leq } , -^{\bot })\). Let

  1. 18.

    \(\mathcal {F}_{T}\) be the smallest set containing {f p pL} and closed under function composition ∘; recall that f p is the Sasaki projection onto p;

  2. 19.

    \(\mathcal {Q} \overset {\text {def}}{=} \&\#x2118; (\mathcal {F}_{T})\);

  3. 20.

    \(\cdot : \mathcal {Q} \times \mathcal {Q} \rightarrow \mathcal {Q} :: A \cdot B \mapsto \{ a \circ b \in \mathcal {F}_{T} \mid a \in A\) and bB};

  4. 21.

    \(\sim : \mathcal {Q} \rightarrow \mathcal {Q} :: A \mapsto \{ f_{(\bigvee \{ a (I) \mid a \in A \} )^{\bot } } \}\).

It is easy to see that the tuple \(\mathbf {F} (\mathfrak {L}) = (\mathcal {Q} , {\bigcup } , {\cdot } , \sim )\) is a generalized dynamic algebra. We will show that it is an orthomodular dynamic algebra by verifying the conditions in the definition one by one. (Notice that \(\bigcup \) plays the role of \(\bigsqcup \).)

Before doing this, we prove a lemma containing a useful calculation.

Lemma 4

For any \(A \in \mathcal {Q}\) , \(\sim \sim A = \{ f_{\bigvee \{ a (I) \mid a \in A \} } \}\) .

Proof

\(\sim \sim A = \sim \{ f_{(\bigvee \{ a (I) \mid a \in A \} )^{\bot } } \} = \{ f_{(f_{(\bigvee \{ a (I) \mid a \in A \} )^{\bot } } (I) )^{\bot } } \} = \{ f_{(\bigvee \{ a (I) \mid a \in A \} )^{\bot \bot } } \} = \{ f_{\bigvee \{ a (I) \mid a \in A \} } \}\)

Proposition 1

\(\mathbf {F} (\mathfrak {L})\) satisfies (9), i.e. \((\mathcal {Q} , {\sqsubseteq } , {\cdot } )\) is a quantale.

Proof

First, we show that \((\mathcal {Q} , {\sqsubseteq })\) is a complete lattice. Note that

$${\sqsubseteq} \overset{\text{def}}{=} \left\{ (A,B) \in \mathcal{Q} \times \mathcal{Q} \mid A \cup B = B \right\} = \{ (A,B) \in \mathcal{Q} \times \mathcal{Q} \mid A \subseteq B \} = {\subseteq} $$

Since \((\mathcal {Q} , {\sqsubseteq }) = (\&\#x2118; (\mathcal {F}_{T}) , {\subseteq })\) is the power set algebra of \(\mathcal {F}_{T}\), it is a complete lattice. A powerset algebra has the union as its arbitrary join, and hence our original \(\bigcup \) is the arbitrary join of the lattice.

Second, since function composition ∘ is associative, it is easy to see that ⋅ is associative. Moreover, the distributivity between \(\bigcup \) and ⋅ is also easy to show. □

Proposition 2

The function \(\chi : L \rightarrow \mathcal {Q} :: p \rightarrow \{ f_{p} \}\) is an ortho-lattice isomorphism from \(\mathfrak {L}\) to \((\mathcal {P} , {\preceq } , \sim )\) , so \((\mathcal {P} , {\preceq } , \sim )\) is a complete orthomodular lattice ((10) for \(\mathbf {F} (\mathfrak {L})\) ).

Proof

First we show injectivity. Assume that p, qL satisfy χ(p) = χ(q). Then f p = f q . By definition p = f p (I) = f q (I) = q.

Second, we show surjectivity. Note that, for each \(A \in \mathcal {Q}\),

$$\begin{array}{@{}rcl@{}} A \in \mathcal{P} &\Leftrightarrow \ & A = \sim B \text{, for some } B \in \mathcal{Q} \\ &\Leftrightarrow \ & A = \{ f_{(\bigvee \{ b(I) \mid b \in B \} )^{\bot}} \} \text{, for some } B \in \mathcal{Q} \\ &\Leftrightarrow \ & A = \{ f_{p} \} \text{, for some } p \in L \qquad\qquad\qquad\qquad(\text{for}\, \Leftarrow, \ \text{take} \,B = \{ f_{p^{\bot}} \}) \end{array} $$

Therefore, \(\mathcal {P} = \{ \{ f_{p} \} \mid p \in L \}\) and the surjectivity of χ follows.

Third, we show that χ preserves the partial order. Note that, for any PL,

$$\begin{array}{@{}rcl@{}} && \bigvee \{ \chi (p) \mid p \in P \} = \sim \sim \bigcup \{ \chi (p) \mid p \in P \} = \sim \sim \{ f_{p} \mid p \in P \} = \{ f_{\bigvee \{ f_{p} (I) \mid p \in P \} } \} \\ && \chi (\bigvee P) = \{ f_{\bigvee P } \} = \{ f_{\bigvee \{ p \mid p \in P \} } \} = \{ f_{\bigvee \{ f_{p} (I) \mid p \in P \} } \} \end{array} $$

Hence \(\bigvee \{ \chi (p) \mid p \in P \} = \chi (\bigvee P)\). It follows that, for any p, qL,

$$p \leq q \ \Leftrightarrow \ p \vee q = q \ \Leftrightarrow \ \chi (p \vee q) = \chi (q) \ \Leftrightarrow \ \chi (p) \vee \chi (q) = \chi (q) \ \Leftrightarrow \ \chi (p) \preceq \chi (q) $$

Finally, we show that χ preserves orthocomplements. For each pL,

$$\sim \chi (p) = \sim \{ f_{p} \} = \{ f_{(f_{p} (I) )^{\bot} } \} = \{ f_{p^{\bot}} \} = \chi (p^{\bot} ).$$

Proposition 3

\(\mathbf {F} (\mathfrak {L})\) satisfies (11), i.e. \(\mathcal {Q}\) is the smallest set containing \(\mathcal {P} \) that is closed underand \(\bigcup \) .

Proof

This is immediate from the definition of \(\mathcal {Q}\). □

Proposition 4

\(\mathbf {F} (\mathfrak {L})\) satisfies (12), i.e. for any \(X , Y \subseteq \mathcal {T} \) , \(\bigcup X = \bigcup Y\) , if and only if X = Y . (Recall that \(\mathcal {T} \) is the smallest subset of \(\mathcal {Q}\) which contains \(\mathcal {P} \) and is closed under the operation ⋅.)

Proof

Let \(X , Y \subseteq \mathcal {T} \) be arbitrary. Note that by definition both X and Y are sets of singletons in \(\mathcal {Q}\). Then the result follows easily from Axiom of Extensionality. □

Proposition 5

\(\mathbf {F} (\mathfrak {L})\) satisfies (13), i.e. for any \(A , B \in \mathcal {T} \) , the following are equivalent:

  1. (i)

    A = B ;

  2. (ii)

    AB , i.e. \(\ulcorner A \urcorner (P) = \ulcorner B \urcorner (P)\) for each \(P \in \mathcal {P} \) .

Proof

From (i) to (ii): :

This direction is obvious.

From (ii) to (i): :

Since \(A , B \in \mathcal {T} \), by definition there are \(m , n \in \mathbb {N}^{+}\) and q 1,…, q m , r 1,…, r n L such that \(A = \{ f_{q_{1}} \circ {\cdots } \circ f_{q_{m}} \}\) and \(B = \{ f_{r_{1}} \circ {\cdots } \circ f_{r_{n}} \}\). By Proposition 2, for each pL, \(\{ f_{p} \} \in \mathcal {P} \) and

$$\begin{array}{@{}rcl@{}} \ulcorner A \urcorner (\{ f_{p} \} ) \,=\, \ulcorner B \urcorner (\{ f_{p} \} ) &\Leftrightarrow & \!\sim \sim\! (A \cdot \{ f_{p} \} ) \!= \sim \sim (B \!\cdot\! \{ f_{p} \} ) \\ &\Leftrightarrow & \!\sim \sim (\{ f_{q_{1}} \circ\! \cdots\! \circ f_{q_{m}} \} \cdot \{ f_{p} \} ) \!= \sim \sim (\{ f_{r_{1}} \circ {\cdots} \circ f_{r_{n}} \} \cdot \{ f_{p} \} ) \\ &\Leftrightarrow & \!\sim \sim (\{ f_{q_{1}} \circ {\cdots} \circ f_{q_{m}} \circ f_{p} \} ) = \sim \sim (\{ f_{r_{1}} \circ {\cdots} \circ f_{r_{n}} \circ f_{p} \} ) \\ &\Leftrightarrow & \!\{ f_{(f_{q_{1}} \circ {\cdots} \circ f_{q_{m}} \circ f_{p} ) (I) } \} \,=\, \{ f_{(f_{r_{1}} \circ {\cdots} \circ f_{r_{n}} \circ f_{p} ) (I) } \} \quad\quad~~(\text{Lemma 4}) \\ &\Leftrightarrow & \!(f_{q_{1}} \circ {\cdots} \circ f_{q_{m}} ) (p) \,=\, (f_{r_{1}} \circ {\cdots} \circ f_{r_{n}} ) (p) \end{array} $$

Now for each pL, by (ii) and the above equivalence we have \((f_{q_{1}} \circ {\cdots } \circ f_{q_{m}} ) (p) = (f_{r_{1}} \circ {\cdots } \circ f_{r_{n}} ) (p)\). Hence \(f_{q_{1}} \circ {\cdots } \circ f_{q_{m}} = f_{r_{1}} \circ \cdots \circ f_{r_{n}}\). Therefore, A = B.

Proposition 6

\(\mathbf {F} (\mathfrak {L})\) satisfies (14): for any \(A , B \in \mathcal {P} \) , \(\ulcorner A \urcorner (B) = f_{A} (B)\) .

Proof

By Proposition 2 there are p, qL such that A = χ(p) = {f p } and B = χ(q) = {f q }. Then by Lemma 4 and Proposition 2,

$$\begin{array}{@{}rcl@{}} && \ulcorner A \urcorner (B) = \sim \sim (A \cdot B) = \sim \sim (\{ f_{p} \} \cdot \{ f_{q} \} ) = \sim \sim \{ f_{p} \circ f_{q} \} = \{ f_{f_{p} \circ f_{q} (I) } \} = \{ f_{f_{p} (q) } \} \\ && f_{A} (B) = A \wedge (\sim A \vee B) = \chi (p) \wedge (\sim \chi (p) \vee \chi (q) ) = \chi (p \wedge (p^{\bot} \vee q ) ) = \{ f_{f_{p} (q) } \} \end{array} $$

Therefore, \(\ulcorner A \urcorner (B) = \{ f_{f_{p} (q) } \} = f_{A} (B)\). □

Proposition 7

\(\mathbf {F} (\mathfrak {L})\) satisfies (5), i.e. for any \(A , B \in \mathcal {Q}\) , \(\ulcorner A \urcorner (B) = \ulcorner A \urcorner (\sim \sim B )\) .

Proof

Recall that by Lemma 1 Sasaki projections preserve arbitrary joins, and thus the same holds for compositions of Sasaki projections. Then

$$\begin{array}{@{}rcl@{}}&&\ulcorner A \urcorner (\sim \sim B ) = \sim \sim (A \cdot \sim \sim B ) = \sim \sim (A \cdot \{ f_{\bigvee \{ b(I) \mid b \in B \} } \} ) = \sim \sim \{ a \circ f_{\bigvee_{b \in B } b(I) } \! \mid \! a \in \! A \} \\ &&= \{ f_{\bigvee \{ a \circ f_{\bigvee_{b \in B } b(I) } (I) \mid a \in A \} } \} = \{ f_{\bigvee \{ a (\bigvee_{ b \in B } b(I) ) \mid a \in A \} } \} = \{ f_{\bigvee \{ a \circ b (I) \mid a \in A, b \in B \} } \} . \end{array} $$

Since \(\ulcorner A \urcorner (B) = \sim \sim (A \cdot B ) = \sim \sim \{ a \circ b \mid a \in A , b \in B \} = \{ f_{ \bigvee \{ a \circ b (I) \mid a \in A, b \in B \} } \}\), \(\ulcorner A \urcorner (\sim \sim B ) = \{ f_{\bigvee \{ a \circ b (I) \mid a \in A, b \in B \} } \} = \ulcorner A \urcorner (B )\). □

Theorem 3

\(\mathbf {F} (\mathfrak {L})\) is an orthomodular dynamic algebra.

Proof

It follows from the definition and the previous propositions. □

Mapping of Arrows

Fix an \(\mathbb {L}\)-morphism k from \(\mathfrak {L}_{1} = (L_{1} , {\leq _{1}} , {-}^{\bot _{1}} )\) to \(\mathfrak {L}_{2} = (L_{2} , {\leq _{2}} , {-}^{\bot _{2}} )\). Define

$$\mathbf{F} (k) : \mathcal{Q}_{1} \rightarrow \mathcal{Q}_{2} :: A_{1} \mapsto \{ k\circ a\circ k^{-1} \mid a_{1} \in A_{1} \} $$

Note that, for each pL 1, f k(p) = kf p k −1, because for each qL 1,

$$\begin{array}{@{}rcl@{}} f_{k (p)} (q) &=& k(p) \wedge \left( k (p)^{\bot} \vee q \right) = k \left( p \wedge \left( p^{\bot} \vee k^{-1} (q) \right) \right) = k \left( f_{p} \left( k^{-1} (q) \right) \right)\\ &=& (k \circ f_{p} \circ k^{-1} ) (q) \end{array} $$

Theorem 4

F(k)is a \(\mathbb {Q}\) -morphism from \(\mathbf {F} (\mathfrak {L}_{1})\) to \(\mathbf {F} (\mathfrak {L}_{2})\) .

Proof

First, we observe that F(k) is an ortho-lattice isomorphism from \((\mathcal {P}_{1} , {\preceq _{1}} , \sim _{1} )\) to \((\mathcal {P}_{2} , {\preceq _{2}} , \sim _{2} )\). By Proposition 2, \(\mathcal {P}_{1} = \{ \{ f_{p} \} \mid p \in L_{1} \}\) and \(\mathcal {P}_{2} = \{ \{ f_{p} \} \mid p \in L_{2} \}\). Note that \(\mathbf {F} (k) = \chi _{2} \circ k \circ \chi _{1}^{-1}\) on \(\mathcal {P}_{1}\); because, for each \(\{ f_{p} \} \in \mathcal {P}_{1}\),

$$(\chi_{2} \circ k \circ \chi_{1}^{-1} ) (\{ f_{p} \} ) = \chi_{2} (k(p) ) = \{ f_{k(p) } \} = \{ k \circ f_{p} \circ k^{-1} \} = \mathbf{F} (k) (\{ f_{p} \} ) $$

Since all of χ 2, k and \(\chi _{1}^{-1}\) are ortho-lattice isomorphisms, so is F(k) on \(\mathcal {P}_{1}\).

Second, we show that F(k) preserves \(\bigcup \). Let \(\{ A^{i} \in \mathcal {Q}_{1} \mid i \in I \}\) be arbitrary.

$$\begin{array}{@{}rcl@{}} \mathbf{F} (k) (\bigcup \{ A^{i} \mid i \in I \} ) &= \ & \mathbf{F} (k) (\{ a \in \mathcal{F}_{T , 1} \mid a \in A^{i} \text{, for some } i \in I \} ) \\ &= \ & \{ k \circ a \circ k^{-1} \in \mathcal{F}_{T , 1} \mid a \in A^{i} \text{, for some } i \in I \} \\ &= \ & \bigcup \left\{ \{ k \circ a \circ k^{-1} \in \mathcal{F}_{T , 1} \mid a \in A^{i} \} \mid i \in I \right\} \\ &= \ & \bigcup \{ \mathbf{F} (k) (A^{i}) \mid i \in I \} \end{array} $$

Third, we show that F(k) preserves ⋅. Let \(A , B \in \mathcal {Q}_{1}\) be arbitrary.

$$\begin{array}{@{}rcl@{}} \mathbf{F} (k) (A \cdot B )& = \ & \mathbf{F} (k) (\{ a \circ b \mid a \in A , b \in B \} ) \\ &= \ & \{ k \circ a \circ b \circ k^{-1} \mid a \in A , b \in B \} \\ &= \ & \{ k \circ a \circ k^{-1} \circ k \circ b \circ k^{-1} \mid a \in A , b \in B \} \\ &= \ & \mathbf{F} (k) (A ) \cdot \mathbf{F} (k) (B ) \end{array} $$

Theorem 5

F is a functor from \(\mathbb {L}\) to \(\mathbb {Q}\) .

Proof

By Theorems 3 and 4, F maps objects in \(\mathbb {L}\) to objects in \(\mathbb {Q}\), and maps arrows \(k : \mathfrak {L}_{1} \rightarrow \mathfrak {L}_{2}\) in \(\mathbb {L}\) to arrows \(\mathbf {F} (k) : \mathbf {F} (\mathfrak {L}_{1}) \rightarrow \mathbf {F} (\mathfrak {L}_{2})\) in \(\mathbb {Q}\).

It is easy to see from the definition that F preserves the identity arrows. For arrow compositions, let \(k : \mathfrak {L}_{1} \rightarrow \mathfrak {L}_{2}\) and \(l : \mathfrak {L}_{2} \rightarrow \mathfrak {L}_{3}\) be two arbitrary \(\mathbb {L}\)-morphisms. Then F(l) ∘F(k) = F(lk) holds, because for any \(A_{1} \in \mathcal {Q}_{1}\)

$$\begin{array}{@{}rcl@{}} (\mathbf{F} (l) \circ \mathbf{F} (k) ) (A_{1} ) &= \ & \mathbf{F} (l) \left( \{ k \circ a_{1} \circ k^{-1} \mid a_{1} \in A_{1} \} \right) \\ &= \ & \{ l \circ (k \circ a_{1} \circ k^{-1} ) \circ l^{-1} \mid a_{1} \in A_{1} \} \\ &= \ & \{ (l \circ k ) \circ a_{1} \circ (l \circ k)^{-1} \mid a_{1} \in A_{1} \} \\ &= \ & \mathbf{F} (l \circ k) (A_{1}) \end{array} $$

3.2 From Orthomodular Dynamic Algebras to Complete Orthomodular Lattices

In this subsection, we define a functor \(\mathbf {U} : \mathbb {Q} \rightarrow \mathbb {L}\).

Mapping of Objects

Fix an orthomodular dynamic algebra \(\mathfrak {Q} = (Q , {\bigsqcup } , \cdot , \sim )\). Define \(\mathbf {U} (\mathfrak {Q}) = (\mathcal {P} , {\preceq } , \sim )\).

Theorem 6

\(\mathbf {U} (\mathfrak {Q})\) is a complete orthomodular lattice.

Proof

It follows directly from the definition of orthomodular dynamic algebras. □

Mapping of Arrows

Fix a \(\mathbb {Q}\)-morphism \(\theta : \mathfrak {Q}_{1} \rightarrow \mathfrak {Q}_{2}\). Let U(𝜃) be the restriction of 𝜃 to \(\mathcal {P}_{1}\).

Theorem 7

U(𝜃)is an \(\mathbb {L}\) -morphism from \(\mathbf {U} (\mathfrak {Q}_{1})\) to \(\mathbf {U} (\mathfrak {Q}_{2})\) .

Proof

This follows directly from the definition of \(\mathbb {Q}\)-morphisms. □

Theorem 8

U is a functor from \(\mathbb {Q}\) to \(\mathbb {L}\) .

Proof

By Theorems 6 and 7 U maps objects in \(\mathbb {Q}\) to objects in \(\mathbb {L}\), and maps arrows \(\theta : \mathfrak {Q}_{1} \rightarrow \mathfrak {Q}_{2}\) in \(\mathbb {Q}\) to arrows \(\mathbf {U} (\theta ) : \mathbf {U} (\mathfrak {Q}_{1}) \rightarrow \mathbf {U} (\mathfrak {Q}_{2})\) in \(\mathbb {L}\). It is obvious from the definition that U preserves the identity arrows and arrow composition. □

4 The Equivalence

4.1 The Natural Isomorphism \(\tau : 1_{\mathbb {L}} \rightarrow \mathbf {U} \circ \mathbf {F}\)

For each complete orthomodular lattice \(\mathfrak {L} = (L , {\leq } , -^{\bot })\), we let \(\tau _{\mathfrak {L}} = \chi \) which is defined in Proposition 2.

Theorem 9

\(\tau : 1_{\mathbb {L}} \rightarrow \mathbf {U} \circ \mathbf {F}\) is a natural isomorphism.

Proof

For each object \(\mathfrak {L}\) in \(\mathbb {L}\), by Proposition 2, \(\tau _{\mathfrak {L}} = \chi \) is a bijective \(\mathbb {L}\)-morphism, so it is not hard to show that \(\tau _{\mathfrak {L}}\) has an inverse in \(\mathbb {L}\) and is an isomorphism in \(\mathbb {L}\).

For naturality, assume that \(k : \mathfrak {L}_{1} \rightarrow \mathfrak {L}_{2}\) is an \(\mathbb {L}\)-morphism. For each pL 1,

$$\begin{array}{@{}rcl@{}} &&((\mathbf{U} \circ \mathbf{F}) (k) \circ \tau_{\mathfrak{L}_{1}} ) (p) = (\mathbf{U} \circ \mathbf{F}) (k) (\{ f_{p} \} ) = \mathbf{U}(\mathbf{F} (k) (\{ f_{p} \} )) = \mathbf{U}(\{ k \circ f_{p} \circ k^{-1} \})=\\ && \mathbf{U}(\{ f_{k (p) } \}) = \{ f_{k (p) } \} = (\tau_{\mathfrak{L}_{2}} \circ k ) (p) \end{array} $$

Therefore, \((\mathbf {U} \circ \mathbf {F}) (k) \circ \tau _{\mathfrak {L}_{1}} = \tau _{\mathfrak {L}_{2}} \circ k\). □

4.2 The Natural Isomorphism \(\eta : 1_{\mathbb {Q}} \rightarrow \mathbf {F} \circ \mathbf {U}\)

For each orthomodular dynamic algebra \(\mathfrak {Q} = (Q , {\bigsqcup } , {\cdot } , \sim )\), we define a function \(\eta _{\mathfrak {Q}} : 1_{\mathbb {Q}} (\mathfrak {Q} ) \rightarrow (\mathbf {F} \circ \mathbf {U} ) (\mathfrak {Q} )\) as follows:

$$\eta_{\mathfrak{Q}} :: x = \bigsqcup \{ p_{(i,1)} \cdot {\cdots} \cdot p_{(i, n_{i})} \mid i \in I \} \mapsto \{ f_{p_{(i,1)}} \circ {\cdots} \circ f_{p_{(i,n_{i})}} \mid i \in I \} $$

where \(p_{(i,j)} \in \mathcal {P}_{\mathfrak {Q}}\), for each \((i,j) \in \bigcup _{i \in I} (\{ i \} \times \{ 1 , {\dots } , n_{i} \} )\). By Lemma 2, each element in Q has a unique normal form, so the function \(\eta _{\mathfrak {Q}}\) is well defined.

Proposition 8

For each \(\mathfrak {Q} = (Q , {\bigsqcup } , {\cdot } , \sim )\) , \(\eta _{\mathfrak {Q}}\) is an isomorphism in \(\mathbb {Q}\) .

Proof

First we show that \(\eta _{\mathfrak {Q}}\) is injective. Assume that in their normal form \(x = \bigsqcup \{ p_{(i,1)} \cdot {\cdots } \cdot p_{(i, n_{i})} \mid i \in I \}\) and \(y = \bigsqcup \{ q_{(j,1)} \cdot {\cdots } \cdot q_{(j, n_{j})} \mid j \in J \}\) are such that \(\eta _{\mathfrak {Q}} (x) = \eta _{\mathfrak {Q}} (y)\). We will show that x = y. By Lemma 2 it suffices to show that \(\{ p_{(i,1)} \cdot {\cdots } \cdot p_{(i, n_{i})} \mid i \in I \} = \{ q_{(j,1)} \cdot {\cdots } \cdot q_{(j, n_{j})} \mid j \in J \}\).

Assume that \(p_{1} \cdot {\cdots } \cdot p_{m} \in \{ p_{(i,1)} \cdot {\cdots } \cdot p_{(i, n_{i})} \mid i \in I \}\). Then \(f_{p_{1}} \circ {\cdots } \circ f_{p_{m}} \in \eta _{\mathfrak {Q}} (x) = \eta _{\mathfrak {Q}} (y)\). Hence there is a \(q_{1} \cdot {\cdots } \cdot q_{n} \in \{ q_{(j,1)} \cdot {\cdots } \cdot q_{(j, n_{j})} \mid j \in J \}\) such that \( f_{p_{1}} \circ {\cdots } \circ f_{p_{m}} = f_{q_{1}} \circ {\cdots } \circ f_{q_{n}}\). Then, for each \(r \in \mathcal {P}_{\mathfrak {Q}}\), \((f_{p_{1}} \circ {\cdots } \circ f_{p_{m}} ) (r) = (f_{q_{1}} \circ {\cdots } \circ f_{q_{n}} ) (r)\), so by Lemma 3 \(\ulcorner p_{1} \cdot {\cdots } \cdot p_{m} \urcorner (r) = (f_{p_{1}} \circ \cdots \circ f_{p_{m}} ) (r) = (f_{q_{1}} \circ {\cdots } \circ f_{q_{n}} ) (r) = \ulcorner q_{1} \cdot {\cdots } \cdot q_{n} \urcorner (r)\). Hence by (5) \(p_{1} \cdot {\cdots } \cdot p_{m} = q_{1} \cdot {\cdots } \cdot q_{n} \in \{ q_{(j,1)} \cdot {\cdots } \cdot q_{(j, n_{j})} \mid j \in J \}\).

Symmetrically we can show that each \(q_{1} \cdot {\cdots } \cdot q_{m} \in \{ q_{(j,1)} \cdot {\cdots } \cdot q_{(j, n_{j})} \mid j \in J \}\) is in \(\{ p_{(i,1)} \cdot {\cdots } \cdot p_{(i, n_{i})} \mid i \in I \}\). Therefore, x = y, and thus \(\eta _{\mathfrak {Q}}\) is injective.

Second we show that \(\eta _{\mathfrak {Q}}\) is surjective. Let A be an arbitrary element of \((\mathbf {F} \circ \mathbf {U}) (\mathfrak {Q})\). Since \((\mathbf {F} \circ \mathbf {U}) (\mathfrak {Q} )\) is an orthomodular dynamic algebra, by Lemma 2, \(A = \bigcup \{ \{ f_{p_{(i,1)}} \} \cdot {\cdots } \cdot \{ f_{p_{(i,n_{i})}} \} \mid i \in I \}\), where each \(\{ f_{p_{(i,j)}} \} \in \mathcal {P}_{(\mathbf {F} \circ \mathbf {U}) (\mathfrak {Q}) }\). It is obvious from the definition that \(\eta _{\mathfrak {Q}} (\bigsqcup \{ p_{(i,1)} \cdot {\cdots } \cdot p_{(i,n_{i})} \mid i \in I \} ) = \{ f_{p_{(i,1)}} \circ {\cdots } \circ f_{p_{(i,n_{i})}} \mid i \in I \} = A\).

Third we show that \(\eta _{\mathfrak {Q}}\) is a \(\mathbb {Q}\)-morphism. It is obvious that \(\eta _{\mathfrak {Q}}\) restricted to \(\mathcal {P}_{\mathfrak {Q}}\) is the same function as χ. Since χ is an ortho-lattice isomorphism, so is this restriction of \(\eta _{\mathfrak {Q}}\). Moreover, it is not hard to show that \(\eta _{\mathfrak {Q}}\) preserves \({\bigsqcup }\). Besides, \(\eta _{\mathfrak {L}}\) preserves ⋅, because for any \(x = \bigsqcup \{ x_{i} \mid i \in I \}\) and \(y = \bigsqcup \{ y_{j} \mid j \in J \}\) in their normal forms in \(\mathfrak {Q}\),

$$\begin{array}{@{}rcl@{}} && \eta_{\mathfrak{Q}} (\bigsqcup \{ x_{i} \mid i \in I \} \cdot \bigsqcup \{ y_{j} \mid j \in J \} ) \\ &= \ & \eta_{\mathfrak{Q}} (\bigsqcup \{ x_{i} \cdot y_{j} \mid i \in I, j \in J \} ) \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\quad~(\text{by (3)})\\ &= \ & \bigcup \{ \eta_{\mathfrak{Q}} (x_{i} \cdot y_{j} ) \mid i \in I, j \in J \} \qquad\qquad\qquad\qquad\qquad\qquad\qquad\quad(\eta_{\mathfrak{Q}} \, \text{preserves}\, {\bigsqcup}) \\ &= \ & \bigcup \{ \eta_{\mathfrak{Q}} (x_{i} ) \cdot \eta_{\mathfrak{Q}} (y_{j} ) \mid i \in I, j \in J \} \qquad\qquad\qquad\qquad\qquad~~(\text{by the definition of}\, \eta_{\mathfrak{Q}}) \\ &= \ & \bigcup \{ \bigcup \{ \eta_{\mathfrak{Q}} (x_{i} ) \mid i \in I \} \cdot \eta_{\mathfrak{Q}} (y_{j} ) \mid j \in J \} \\ &= \ & \bigcup \{ \eta_{\mathfrak{Q}} (x_{i} ) \mid i \in I \} \cdot \bigcup \{ \eta_{\mathfrak{Q}} (y_{j} ) \mid j \in J \} \end{array} $$

Since \(\eta _{\mathfrak {Q}}\) is a bijective \(\mathbb {Q}\)-morphism, it is not hard to show that it has an inverse in \(\mathbb {Q}\) and thus is an isomorphism in \(\mathbb {Q}\). □

Proposition 9

η satisfies naturality.

Proof

Let \(\theta : \mathfrak {Q}_{1} \rightarrow \mathfrak {Q}_{2}\) be a \(\mathbb {Q}\)-morphism. For each \(x = \bigsqcup \{ p_{(i,1)} \cdot {\cdots } \cdot p_{(i, n_{i})} \mid i \in I \}\) in its normal form in \(\mathfrak {Q}_{1}\),

$$\begin{array}{@{}rcl@{}} \left( (\mathbf{F} \circ \mathbf{U}) (\theta) \circ \eta_{\mathfrak{Q}_{1}} \right) (x) &= \ & \left( (\mathbf{F} \circ \mathbf{U}) (\theta) \circ \eta_{\mathfrak{Q}_{1}} \right) \left( \bigsqcup \{ p_{(i,1)} \cdot {\cdots} \cdot p_{(i, n_{i})} \mid i \in I \} \right) \\ &= \ & (\mathbf{F} \circ \mathbf{U}) (\theta) (\{ f_{p_{(i,1)}} \circ {\cdots} \circ f_{p_{(i, n_{i})}} \mid i \in I \} ) \\ &= \ & \{ f_{\mathbf{U} (\theta) (p_{(i,1)}) } \circ {\cdots} \circ f_{\mathbf{U} (\theta) (p_{(i, n_{i})}) } \mid i \in I \} \\ &= \ & \{ f_{\theta (p_{(i,1)}) } \circ {\cdots} \circ f_{\theta (p_{(i, n_{i})}) } \mid i \in I \} \\ &= \ & \eta_{\mathfrak{Q}_{2}} (\bigsqcup \{ \theta (p_{(i,1)} ) \cdot {\cdots} \cdot \theta (p_{(i, n_{i})} ) \mid i \in I \} ) \\ &= \ & (\eta_{\mathfrak{Q}_{2}} \circ \theta ) (\bigsqcup \{ p_{(i,1)} \cdot {\cdots} \cdot p_{(i, n_{i})} \mid i \in I \} ) \\ &= \ & (\eta_{\mathfrak{Q}_{2}} \circ \theta ) (x) \end{array} $$

Therefore, \((\mathbf {F} \circ \mathbf {U}) (\theta ) \circ \eta _{\mathfrak {Q}_{1}} = \eta _{\mathfrak {Q}_{2}} \circ \theta \). □

Theorem 10

\(\eta : 1_{\mathbb {Q}} \rightarrow \mathbf {F} \circ \mathbf {U}\) is a natural isomorphism.

Proof

It follows from the previous two propositions. □

Finally, we come to the conclusion of this paper.

Theorem 11

(F, U, τ, η)forms a categorical equivalence between \(\mathbb {L}\) and \(\mathbb {Q}\) .

Remark 1

Had we replaced complete orthomodular lattice in Definitions 5 and 10 with a more restricted type of lattice such as a Hilbert lattice or Piron lattice, we could then show these quantum dynamic algebras are categorically equivalent to the corresponding category of latices (Hillbert lattice or Piron lattice with ortho-lattice isomorphisms) using the same functors and natural isomorphisms as we use here. The proof remains exactly the same. This thus establishes a link between quantum dynamic algebras and Hilbert spaces (or other important quantum structures) via these stronger lattice structures, particularly the Hilbert lattices.

5 Conclusion

It can be argued that this equivalence we establish in this paper is the simplest meaningful connection between quantales and orthomodular lattices. As quantales are complete lattices, it is natural that they correspond to orthomodular lattices that are complete. As orthomodular lattices have an orthocomplementation, it is natural to involve an orthocomplementation in the quantale structure too, which is why the orthomodular dynamic algebra as well as the quantum dynamic algebra includes a unary operator that resembles an orthocomplementation. Although one could easily define a semi-group structure on-top of any lattice to form a quantale, we employ the Sasaki projection to ensure that our semi-group structure has quantum significance and resembles to some extent the composition in an operator algebra as intended. We realize the quantale join as sets of functions, in order to capture non-determinism, which is also in line with the intended interpretation of quantales. Furthermore, via Remark 1, our result establishes an equivalence between different types of quantale structures and different types of quantum lattice structures that in turn relate to Hilbert spaces and other important quantum structures.

There are other ways of realizing a lattice structure as a quantum dynamic algebra. One is to realize the quantale join, not as sets of functions but as relations that are unions of functions. This would be comparably effective in establishing non-determinism, but will lack certain properties, such as atomicity, that may be useful. Another way is to extend the types of elements that form the quantale from projectors to automorphisms, unitaries, or linear maps. This would potentially strengthen the connection to operator algebras.

Quantales can be put into action by acting on a module as in [1]. A logic can further be developed on the quantale or the quantale actions, and the categorical equivalence may provide a setting in which we can compare logics natural to quantales with orthomodular quantum logic that is axiomatized for orthomodular lattices.