--- abstract: 'This paper is a sequel to @HeunenJ10a and continues the study of quantum logic via dagger kernel categories. It develops the relation between these categories and both orthomodular lattices and Foulis semigroups. The relation between the latter two notions has been uncovered in the 1960s. The current categorical perspective gives a broader context and reconstructs this relationship between orthomodular lattices and Foulis semigroups as special instances.' address: 'Institute for Computing and Information Sciences (iCIS), Radboud University Nijmegen, The Netherlands' author: - Bart Jacobs title: | Orthomodular lattices, Foulis Semigroups\ and Dagger Kernel Categories --- Introduction {#IntroSec} ============ Dagger kernel categories have been introduced in @HeunenJ10a as a relatively simple setting in which to study categorical quantum logic. These categories turn out to have orthomodular logic built in, via their posets ${\ensuremath{\mathrm{KSub}}}(X)$ of kernel subobjects that can be used to interprete predicates on $X$. The present paper continues the study of dagger kernel categories, especially in relation to orthomodular lattices and Foulis semigroups. The latter two notions have been studied extensively in the context of quantum logic. The main results of this paper are as follows. (1) A special category <span>$\mathbf{OMLatGal}$</span> is defined with orthomodular lattices as objects and Galois connections between them as morphisms; it is shown that: 1. <span>$\mathbf{OMLatGal}$</span> is itself a dagger kernel category—with some additional structure such as dagger biproducts, and an opclassifier; 2. for each dagger kernel category <span>$\mathbf{D}$</span> there is a functor ${\ensuremath{\mathbf{D}}} \rightarrow {\ensuremath{\mathbf{OMLatGal}}}$ preserving the dagger kernel structure; hence <span>$\mathbf{OMLatGal}$</span> contains in a sense all dagger kernel categories. (2) For each object $X$ in a dagger kernel category, the homset ${\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(X)} = {\ensuremath{\mathbf{D}}}(X,X)$ of endo-maps is a Foulis semigroup. (3) Every Foulis semigroup $S$ yields a dagger kernel category ${\mathcal{K}^{\dag}(S)}$ via the "dagger Karoubi" construction ${\mathcal{K}^{\dag}(-)}$. Translations between orthomodular lattices and Foulis semigroups have been described in the 1960s, see *e.g.* @Foulis60 [@Foulis62; @Foulis63; @BlythJ72; @Kalmbach83]. These translations appear as special instances of the above results: 1. given a Foulis semigroup $S$, all the kernel posets ${\ensuremath{\mathrm{KSub}}}(s)$ are orthomodular lattices, for each object $s\in{\mathcal{K}^{\dag}(S)}$ of the associated dagger kernel category (using point (3) mentioned above). For the unit element $s=1$ this yields the "old" translation from Foulis semigroups to orthomodular lattices; 2. given an arbitrary orthomodular lattice $X$, the set of (Galois) endomaps ${\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(X)} = {\ensuremath{\mathbf{OMLatGal}}}(X, X)$ on $X$ in the dagger kernel category <span>$\mathbf{OMLatGal}$</span> forms a Foulis semigroup—using points (1) and (2). Again this is the "old" translation, from orthomodular lattices to Foulis semigroups. Since dagger kernel categories are essential in these constructions we see (further) evidence of the relevance of categories in general, and of dagger kernel categories in particular, in the setting of quantum (logical) structures. The paper is organised as follows. Section \[DagKerSec\] first recalls the essentials about dagger kernel categories from @HeunenJ10a and also about the (dagger) Karoubi envelope. It shows that dagger kernel categories are closed under this construction. Section \[OMLatDagKerSec\] introduces the fundamental category <span>$\mathbf{OMLatGal}$</span> of orthomodular lattices with Galois connections between them, investigates some of its properties, and introduces the functor ${\ensuremath{\mathrm{KSub}}}\colon {\ensuremath{\mathbf{D}}}\rightarrow {\ensuremath{\mathbf{OMLatGal}}}$ for any dagger kernel category <span>$\mathbf{D}$</span>. Subsequently, Section \[FoulisDagKerSec\] recalls the definition of Foulis semigroups, shows how they arise as endo-homsets in dagger kernel categories, and proves that their dagger Karoubi envelope yields a dagger kernel category. The paper ends with some final remarks and further questions in Section \[ConclusionSec\]. ### Added in print {#added-in-print .unnumbered} After this paper has been accepted for publication, it became clear that the category <span>$\mathbf{OMLatGal}$</span> that plays a central role in this paper was already defined some thirty five years ago, namely by Crown in @Crown75. There however, the category was not investigated systematically, nor its central position in the context of categorical quantum logic (in terms of dagger kernel categories). Dagger kernel categories {#DagKerSec} ======================== Since the notion of dagger kernel category is fundamental in this paper we recall the essentials from @HeunenJ10a, where this type of category is introduced. Further details can be found there. A dagger kernel category consists of a category <span>$\mathbf{D}$</span> with a dagger functor $\dag \colon {\ensuremath{\mathbf{D}}}{\ensuremath{^{\mathrm{op}}}}\rightarrow {\ensuremath{\mathbf{D}}}$, a zero object $0\in{\ensuremath{\mathbf{D}}}$, and dagger kernels. The functor $\dag$ is the identity on objects $X\in{\ensuremath{\mathbf{D}}}$ and satisfies $f^{\dag\dag} = f$ on morphisms $f$. The zero object $0$ yields a zero map, also written as $0$, namely $X\rightarrow 0 \rightarrow Y$ between any two objects $X,Y\in{\ensuremath{\mathbf{D}}}$. A dagger kernel of a map $f\colon X\rightarrow Y$ is a kernel map, written as $\smash{\xymatrix@C-1pc{k\colon K\ar@{ |>->}[r] & X}}\!$, which is—or can be chosen as—a dagger mono, meaning that $k^{\dag} {\mathrel{\circ}}k = {\ensuremath{\mathrm{id}_{K}}}$. Often we write $\ker(f)$ for the kernel of $f$, and ${\ensuremath{\mathrm{coker}}}(f) = \ker(f^{\dag})^{\dag}$ for its cokernel. The definition $k^{\perp} = \ker(k^{\dag})$ for a kernel $k$ yields an orthocomplement. We write <span>$\mathbf{DKC}$</span> for the category with dagger kernel categories as objects and functors preserving $\dag, 0, \ker$. The main examples of dagger kernel categories are: <span><span>$\mathbf{Rel}$</span></span>, the category of sets and relations, its subcategory <span>$\mathbf{pInj}$</span> of sets and partial injections, <span><span>$\mathbf{Hilb}$</span></span>, the category of Hilbert spaces and bounded/continuous linear maps between them, and <span><span>$\mathbf{PHilb}$</span></span>, the category of projective Hilbert spaces. This paper adds another example, namely <span>$\mathbf{OMLatGal}$</span>. The main results from @HeunenJ10a about dagger kernel categories are as follows. (1) Each poset ${\ensuremath{\mathrm{KSub}}}(X)$ of kernel subobjects of an object $X$ is an orthomodular lattice; this is the basis of the relevance of dagger kernel categories to quantum logic. (2) Pullbacks of kernels exist along arbitrary maps $f\colon X\rightarrow Y$, yielding a pullback (or substitution) functor $f^{-1} \colon {\ensuremath{\mathrm{KSub}}}(Y) \rightarrow {\ensuremath{\mathrm{KSub}}}(X)$. Explicitly, as in @Freyd64, $f^{-1}(n) = \ker({\ensuremath{\mathrm{coker}}}(n) {\mathrel{\circ}}f)$. (3) This pullback functor $f^{-1}$ has a left adjoint $\exists_{f} \colon {\ensuremath{\mathrm{KSub}}}(X)\rightarrow {\ensuremath{\mathrm{KSub}}}(Y)$, corresponding to image factorisation. These $f^{-1}$ and $\exists_f$ only preserve part of the logical structure—meets are preserved by $f^{-1}$ and joins by $\exists_f$, via the adjointness—but for instance negations and joins are not preserved by substitution $f^{-1}$, unlike what is standard in categorical logic, see *e.g.* @Jacobs99a. Substitution $f^{-1}$ and existential quantification $\exists_{f}$ are inter-expressible, via the equation $f^{-1}(m)^{\perp} = \exists_{f^\dag}(m^{\perp})$. (4) The logical "Sasaki" hook ${\mathrel{\supset}}$ and "and-then" ${\mathrel{\&}}$ connectives—together with the standard adjunction between them @Finch70 [@CoeckeS04]—arise via this adjunction $\exists_{f} \dashv f^{-1}$, namely for $m,n,k\in {\ensuremath{\mathrm{KSub}}}(X)$ as: $$\begin{array}{rclcrcl} m {\mathrel{\supset}}n & = & {\mathfrak{E}(m)}^{-1}(n) & \quad & k {\mathrel{\&}}m & = & \exists_{{\mathfrak{E}(m)}}(k) \\ & = & m^{\perp} {\mathrel{\vee}}(m{\mathrel{\wedge}}n) & & & = & m {\mathrel{\wedge}}(m^{\perp} {\mathrel{\vee}}k), \end{array}$$ where ${\mathfrak{E}(m)} = m {\mathrel{\circ}}m^{\dag}\colon X\rightarrow X$ is the effect (see @DvurecenskijP00) associated with the kernel $m$. Karoubi envelope {#KaroubiSubsec} ---------------- Next we recall the essentials of the so-called Karoubi envelope (see @Karoubi78 or @Freyd64 [Chapter 2, Exercise B]) construction—and its "dagger" version—involving the free addition of splittings of idempotents to a category. The construction will be used in Section \[FoulisDagKerSec\] to construct a dagger kernel category out of a Foulis semigroup. It is thus instrumental, and not studied in its own right. An idempotent in a category is an endomap $s\colon X\rightarrow X$ satisfying $s{\mathrel{\circ}}s = s$. A splitting of such an idempotent $s$ is a pair of maps $e\colon X\rightarrow Y$ and $m\colon Y\rightarrow X$ with $m{\mathrel{\circ}}e = s$ and $e{\mathrel{\circ}}m = {\ensuremath{\mathrm{id}_{Y}}}$. Clearly, $m$ is then a mono and $e$ is an epi. Such a splitting, if it exists, is unique up to isomorphism. <span> **PROOF:** **ENDPROOF**</span> For an arbitrary category <span>$\mathbf{C}$</span> the so-called Karoubi envelope ${\mathcal{K}({\ensuremath{\mathbf{C}}})}$ has idempotents $s\colon X\rightarrow X$ in <span>$\mathbf{C}$</span> as objects. A morphism $\smash{(X\stackrel{s}{\rightarrow}X) \,\stackrel{f}{\longrightarrow}\, (Y\stackrel{t}{\rightarrow}Y)}$ in ${\mathcal{K}({\ensuremath{\mathbf{C}}})}$ consists of a map $f\colon X\rightarrow Y$ in <span>$\mathbf{C}$</span> with $f{\mathrel{\circ}}s = f = t{\mathrel{\circ}}f$. The identity on an object $(X,s)\in{\mathcal{K}({\ensuremath{\mathbf{C}}})}$ is the map $s$ itself. Composition in ${\mathcal{K}({\ensuremath{\mathbf{C}}})}$ is as in <span>$\mathbf{C}$</span>. The mapping $X\mapsto (X,{\ensuremath{\mathrm{id}_{X}}})$ thus yields a full and faithful functor $\mathcal{I}\colon {\ensuremath{\mathbf{C}}} \rightarrow {\mathcal{K}({\ensuremath{\mathbf{C}}})}$. The Karoubi envelope ${\mathcal{K}({\ensuremath{\mathbf{C}}})}$ can be understood as the free completion of <span>$\mathbf{C}$</span> with splittings of idempotents. Indeed, an idempotent $f\colon (X,s)\rightarrow (X,s)$ in ${\mathcal{K}({\ensuremath{\mathbf{C}}})}$ can be split as $f = \big((X,s) \,\smash{\stackrel{f}{\rightarrow}}\, (X,f) \,\smash{\stackrel{f}{\rightarrow}}\, (X,s)\big)$. If $F\colon {\ensuremath{\mathbf{C}}}\rightarrow {\ensuremath{\mathbf{D}}}$ is a functor to a category <span>$\mathbf{D}$</span> in which endomorphisms split, then there is an up to isomorphism unique functor $\overline{F}\colon {\mathcal{K}({\ensuremath{\mathbf{C}}})}\rightarrow {\ensuremath{\mathbf{D}}}$ with $\overline{F}{\mathrel{\circ}}\mathcal{I} \cong F$. <span> **PROOF:** **ENDPROOF**</span> Hayashi @Hayashi85 (see also @HoofmanM95) has developed a theory of semi-functors and semi-adjunctions that can be used to capture non-extensional features, without uniqueness of mediating maps, like for exponents $\Rightarrow$ @Scott80a [@LambekS86], products $\prod$ @Jacobs91b, or exponentials $!$ @Hoofman92. The Karoubi envelope can be used to turn such "semi" notions into proper (extensional) ones. This also happens in Section \[FoulisDagKerSec\]. Now assume <span>$\mathbf{D}$</span> is a dagger category. An endomap $s\colon X \rightarrow X$ in <span>$\mathbf{D}$</span> is called a self-adjoint idempotent if $s^{\dag} = s = s{\mathrel{\circ}}s$. A splitting of such an $s$ consists, as before, of maps $m,e$ with $m{\mathrel{\circ}}e = s$ and $e{\mathrel{\circ}}m = {\ensuremath{\mathrm{id}_{}}}$. In that case $e^{\dag}, m^{\dag}$ is also a splitting of $s$, so that we get an isomorphism $\varphi = m^{\dag} {\mathrel{\circ}}m$ in a commuting diagram: $$\xymatrix@R-1pc@C+1pc{ X\ar[dd]_{s}\ar[dr]_{e}\ar@/^2ex/[drr]^-{m^{\dag}} \\ & Y\ar[dl]_{m}\ar[r]^(0.4){\varphi}_(0.4){\cong} & Y\ar@/^2ex/[dll]^-{e^{\dag}} \\ X }$$ Hence $e^{\dag} = m$, as subobjects, and $m^{\dag} = e$ as quotients. The dagger Karoubi envelope ${\mathcal{K}^{\dag}({\ensuremath{\mathbf{D}}})}$ of ${\ensuremath{\mathbf{D}}}$ is the full subcategory of ${\mathcal{K}({\ensuremath{\mathbf{D}}})}$ with self-adjoint idempotents as objects, see also @Selinger08. This is again a dagger category, since if $f\colon (X,s) \rightarrow (Y,t)$ in ${\mathcal{K}^{\dag}({\ensuremath{\mathbf{D}}})}$, then $f^{\dag} \colon (Y,t) \rightarrow (X,s)$ because: $$s {\mathrel{\circ}}f^{\dag} = s^{\dag} {\mathrel{\circ}}f^{\dag} = (f {\mathrel{\circ}}s)^{\dag} = f^{\dag},$$ and similarly $f^{\dag} {\mathrel{\circ}}t = f^{\dag}$. The functor $\mathcal{I}\colon {\ensuremath{\mathbf{D}}} \rightarrow {\mathcal{K}({\ensuremath{\mathbf{D}}})}$ factors via ${\mathcal{K}^{\dag}({\ensuremath{\mathbf{D}}})} \rightarrow {\mathcal{K}({\ensuremath{\mathbf{D}}})}$. One can understand ${\mathcal{K}^{\dag}({\ensuremath{\mathbf{D}}})}$ as the free completion of <span>$\mathbf{D}$</span> with splittings of self-adjoint idempotents. Selinger @Selinger08 shows that the dagger Karoubi envelope construction ${\mathcal{K}^{\dag}(-)}$ preserves dagger biproducts and dagger compact closedness. Here we extend this with dagger kernels in the next result. It will not be used in the sequel but is included to show that the dagger Karoubi envelope is quite natural in the current setting. \[KaroubiKernelProp\] If <span>$\mathbf{D}$</span> is a dagger kernel category, then so is ${\mathcal{K}^{\dag}({\ensuremath{\mathbf{D}}})}$. Moreover, the embedding $\mathcal{I}\colon {\ensuremath{\mathbf{D}}} \rightarrow {\mathcal{K}^{\dag}({\ensuremath{\mathbf{D}}})}$ is a map of dagger kernel categories. For each object $X\in{\ensuremath{\mathbf{D}}}$, the zero map $0\colon X\rightarrow X$ is a zero object in ${\mathcal{K}^{\dag}({\ensuremath{\mathbf{D}}})}$, since there is precisely one map $(X,0)\rightarrow (Y,t)$ in ${\mathcal{K}^{\dag}({\ensuremath{\mathbf{D}}})}$, namely the zero map $0\colon X\rightarrow Y$. As canonical choice we take the zero object $0\in{\ensuremath{\mathbf{D}}}$ with zero map $0 = {\ensuremath{\mathrm{id}_{0}}}\colon 0\rightarrow 0$, which is in the range of $\mathcal{I}\colon {\ensuremath{\mathbf{D}}} \rightarrow {\mathcal{K}^{\dag}({\ensuremath{\mathbf{D}}})}$. For an arbitrary map $f\colon (X,s)\rightarrow (Y,t)$ in ${\mathcal{K}^{\dag}({\ensuremath{\mathbf{D}}})}$, let $k\colon K\rightarrowtail X$ be the kernel of $f\colon X\rightarrow Y$ in <span>$\mathbf{D}$</span>. We obtain a map $s'\colon K\rightarrow K$, as in: $$\xymatrix@C+1pc@R-1pc{ K\ar@{ |>->}[r]^-{k} & X\ar[r]^-{f} & Y \\ K\ar@{..>}[u]^{s'}\ar[r]_-{k} & X\ar[u]_{s} }$$ since $f{\mathrel{\circ}}s {\mathrel{\circ}}k = f{\mathrel{\circ}}k = 0$. We obtain that $s'$ is a self-adjoint idempotent, using that $k$ is a dagger mono (*i.e.* satisfies $k^{\dag} {\mathrel{\circ}}k = {\ensuremath{\mathrm{id}_{}}}{}$). $$\begin{array}{ccc} \begin{array}{rcl} s' {\mathrel{\circ}}s' & = & k^{\dag} {\mathrel{\circ}}k {\mathrel{\circ}}s' {\mathrel{\circ}}s' \\ & = & k^{\dag} {\mathrel{\circ}}s {\mathrel{\circ}}k {\mathrel{\circ}}s' \\ & = & k^{\dag} {\mathrel{\circ}}s{\mathrel{\circ}}s {\mathrel{\circ}}k \\ & = & k^{\dag} {\mathrel{\circ}}s{\mathrel{\circ}}k \\ & = & k^{\dag} {\mathrel{\circ}}k {\mathrel{\circ}}s' \\ & = & s'. \end{array} & \qquad & \begin{array}{rcl} s'^{\dag} & = & s'^{\dag} {\mathrel{\circ}}k^{\dag} {\mathrel{\circ}}k \\ & = & (k{\mathrel{\circ}}s')^{\dag} {\mathrel{\circ}}k \\ & = & (s {\mathrel{\circ}}k)^{\dag} {\mathrel{\circ}}k \\ & = & k^{\dag} {\mathrel{\circ}}s^{\dag} {\mathrel{\circ}}k \\ & = & k^{\dag} {\mathrel{\circ}}s {\mathrel{\circ}}k \\ & = & k^{\dag} {\mathrel{\circ}}k {\mathrel{\circ}}s' \\ & = & s'. \end{array} \end{array}$$ This yields a dagger kernel in ${\mathcal{K}^{\dag}({\ensuremath{\mathbf{D}}})}$, $$\xymatrix@C+1pc{ (K,s')\ar[r]^-{s{\mathrel{\circ}}k} & (X,s)\ar[r]^-{f} & (Y,t) }$$ since: 1. $s{\mathrel{\circ}}k$ is a morphism in ${\mathcal{K}^{\dag}({\ensuremath{\mathbf{D}}})}$: $s{\mathrel{\circ}}(s {\mathrel{\circ}}k) = s{\mathrel{\circ}}k$ and $(s{\mathrel{\circ}}k) {\mathrel{\circ}}s' = s{\mathrel{\circ}}s{\mathrel{\circ}}k = s{\mathrel{\circ}}k$; 2. $s{\mathrel{\circ}}k$ is a dagger mono: $$\begin{array}{rcl} (s{\mathrel{\circ}}k)^{\dag} {\mathrel{\circ}}(s{\mathrel{\circ}}k) & = & (k {\mathrel{\circ}}s')^{\dag} {\mathrel{\circ}}(k{\mathrel{\circ}}s') \\ & = & s'^{\dag} {\mathrel{\circ}}k^{\dag} {\mathrel{\circ}}k {\mathrel{\circ}}s' \\ & = & s' {\mathrel{\circ}}s' \\ & = & s' \\ & = & {\ensuremath{\mathrm{id}_{(K,s')}}}; \end{array}$$ 3. $f{\mathrel{\circ}}(s {\mathrel{\circ}}k) = f{\mathrel{\circ}}k = 0$; 4. if $g\colon (Z,r)\rightarrow (X,s)$ satisfies $f{\mathrel{\circ}}g = 0$, then there is a map $h\colon Z\rightarrow K$ in <span>$\mathbf{D}$</span> with $k{\mathrel{\circ}}h = g$. Then $s' {\mathrel{\circ}}h = h$, since $k{\mathrel{\circ}}s' {\mathrel{\circ}}h = s {\mathrel{\circ}}k {\mathrel{\circ}}h = s {\mathrel{\circ}}g = g = k {\mathrel{\circ}}h$. Similarly, $h {\mathrel{\circ}}r = h$, since $k{\mathrel{\circ}}h {\mathrel{\circ}}r = g {\mathrel{\circ}}r = g = k{\mathrel{\circ}}h$. Hence $h$ is a morphism $(Z,r)\rightarrow (K,s')$ in ${\mathcal{K}^{\dag}({\ensuremath{\mathbf{D}}})}$ with $(s{\mathrel{\circ}}k) {\mathrel{\circ}}h = s{\mathrel{\circ}}g = g$. It is the unique such mapping with this property since $s{\mathrel{\circ}}k$ is a (dagger) mono. ${\square}$ \[KaroubiKernelEx\] In the category <span><span>$\mathbf{Hilb}$</span></span>self-adjoint idempotents $s\colon H\rightarrow H$ are also called projections. They can be written as $s = m {\mathrel{\circ}}m^{\dag} = {\mathfrak{E}(m)}$ for a closed subspace $m\colon M\rightarrowtail H$, see any textbook on Hilbert spaces (*e.g.* @Dvurecenskij92). Hence they split already in <span><span>$\mathbf{Hilb}$</span></span>, and so the dagger Karoubi envelope ${\mathcal{K}^{\dag}({{\ensuremath{\mathbf{Hilb}}}\xspace})}$ is isomorphic to <span><span>$\mathbf{Hilb}$</span></span>: it does not add anything. For the category <span><span>$\mathbf{Rel}$</span></span>of sets and relations the sitation is different. A self-adjoint idempotent $S\colon X\rightarrow X$ is a relation $S\subseteq X\times X$ that is both symmetric (since $S^{\dag} = S$) and transitive (since $S{\mathrel{\circ}}S = S$), and thus a "partial equivalence relation", commonly abbreviated as PER. The dagger Karoubi envelope ${\mathcal{K}^{\dag}({{\ensuremath{\mathbf{Rel}}}\xspace})}$ has such PERs as objects. A morphism $R \colon (S\subseteq X\times X) \rightarrow (T\subseteq Y\times Y)$ is a relation $R\colon X\rightarrow Y$ with $R{\mathrel{\circ}}S = R = T{\mathrel{\circ}}R$. Finally we describe the "effect" operation ${\mathfrak{E}(m)} = m {\mathrel{\circ}}m^{\dag}$ as a functor into a dagger Karoubi envelope. For a dagger kernel category <span>$\mathbf{D}$</span> write ${\ensuremath{\mathrm{KSub}}}({\ensuremath{\mathbf{D}}})$ for the category with kernels $M\rightarrowtail X$ as objects. A morphism $\smash{(M\stackrel{m}{\rightarrowtail}X) \stackrel{f}{\longrightarrow} (N\stackrel{n}{\rightarrowtail} Y)}$ in ${\ensuremath{\mathrm{KSub}}}({\ensuremath{\mathbf{D}}})$ is a map $f\colon X\rightarrow Y$ such that $f{\mathrel{\circ}}m$ factors through $n$. The effect operation can then be described as a functor: $$\xymatrix{ {\ensuremath{\mathrm{KSub}}}({\ensuremath{\mathbf{D}}})\ar[rr]^-{{\mathfrak{E}(-)}} & & {\mathcal{K}^{\dag}({\ensuremath{\mathbf{D}}})} }$$ via: $$\simsjonathan@example.com{ M\ar@{ |>->}[dd]_{m}\ar@{-->}[r]^-{\varphi} & N\ar@{ |>->}[dd]^{n} \\ & & \longmapsto & \Big(X\ar[r]^-{{\mathfrak{E}(m)}} & X\Big)\ar[r]^-{f{\mathrel{\circ}}{\mathfrak{E}(m)}} & \Big(Y\ar[r]^-{{\mathfrak{E}(n)}} & Y\Big) \\ X\ar[r]^-{f} & Y }$$ We use that the necessarily unique map $\varphi\colon M\rightarrow N$ with $n{\mathrel{\circ}}\varphi = f {\mathrel{\circ}}m$ satisfies $\varphi = n^{\dag} {\mathrel{\circ}}n {\mathrel{\circ}}\varphi = n^{\dag} {\mathrel{\circ}}f {\mathrel{\circ}}m$. Hence: $${\mathfrak{E}(n)} {\mathrel{\circ}}f {\mathrel{\circ}}{\mathfrak{E}(m)} = n {\mathrel{\circ}}n^{\dag} {\mathrel{\circ}}f {\mathrel{\circ}}m {\mathrel{\circ}}m^{\dag} = n {\mathrel{\circ}}\varphi {\mathrel{\circ}}m^{\dag} = f {\mathrel{\circ}}m {\mathrel{\circ}}m^{\dag} = f {\mathrel{\circ}}{\mathfrak{E}(m)},$$ so that $f {\mathrel{\circ}}{\mathfrak{E}(m)}$ is a morphism ${\mathfrak{E}(m)}\rightarrow {\mathfrak{E}(n)}$ in the dagger Karoubi envelope ${\mathcal{K}^{\dag}({\ensuremath{\mathbf{D}}})}$. It is not hard to see that this functor is full. <span> **PROOF:** **ENDPROOF**</span> Orthomodular lattices and Dagger kernel categories {#OMLatDagKerSec} ================================================== In @HeunenJ10a it was shown how each dagger kernel category gives rise to an indexed collection of orthomodular lattices, given by the posets of the kernel subobjects ${\ensuremath{\mathrm{KSub}}}(X)$ of each object $X$. Here we shall give a more systematic description of the situation and see that a suitable category <span>$\mathbf{OMLatGal}$</span> of orthomodular lattices—with Galois connections between them—is itself a dagger kernel category. The mapping ${\ensuremath{\mathrm{KSub}}}(-)$ turns out to be functor to this category <span>$\mathbf{OMLatGal}$</span>, providing a form of representation of dagger kernel categories. We start by recalling the basic notion of orthomodular lattices. They may be understood as a non-distributive generalisation of Boolean algebras. The orthomodularity formulation is due to @Husimi37, following @BirkhoffN36. \[OMLatDef\] A meet semi-lattice $(X,{\mathrel{\wedge}}1)$ is called an ortholattice if it comes equipped with a function $(-)^{\perp}\colon X \to X$ satisfying: 1. $x^{\perp\perp} = x$; 2. $x \leq y$ implies $y^\perp \leq x^\perp$; 3. $x {\mathrel{\wedge}}x^\perp$ is below every element, *i.e.* is bottom element $0$. One can thus define a bottom element as $0 = 1 {\mathrel{\wedge}}1^{\perp} = 1^\perp$ and a join as $x{\mathrel{\vee}}y = (x^{\perp}{\mathrel{\wedge}}y^{\perp})^{\perp}$, satisfying $x{\mathrel{\vee}}x^{\perp} = 1$. Such an ortholattice is called orthomodular if it satisfies (one of) the three equivalent conditions: 1. $x \leq y$ implies $y = x {\mathrel{\vee}}(x^\perp {\mathrel{\wedge}}y)$; 2. $x \leq y$ implies $x = y {\mathrel{\wedge}}(y^\perp {\mathrel{\vee}}x)$; 3. $x \leq y$ and $x^{\perp} {\mathrel{\wedge}}y = 0$ implies $x=y$. We shall consider two ways of organising orthomodular lattices into a category. The categories <span>$\mathbf{OMLat}$</span> and <span>$\mathbf{OMLatGal}$</span> both have orthomodular lattices as objects. (1) A morphism $f\colon X\rightarrow Y$ in <span>$\mathbf{OMLat}$</span> is a function $f\colon X\rightarrow Y$ between the underlying sets that preserves ${\mathrel{\wedge}}, 1, (-)^{\perp}$—and thus also $\leq$, ${\mathrel{\vee}}$ and $0$; (2) A morphism $X\rightarrow Y$ in <span>$\mathbf{OMLatGal}$</span> is a pair $f = (f_{*}, f^{*})$ of "antitone" functions $f_{*}\colon X{\ensuremath{^{\mathrm{op}}}}\rightarrow Y$ and $f^{*}\colon Y \rightarrow X{\ensuremath{^{\mathrm{op}}}}$ forming a Galois connection (or adjunction $f^{*}\dashv f_{*}$): $x\leq f^{*}(y)$ iff $y\leq f_{*}(x)$ for $x\in X$ and $y\in Y$. The identity morphism on $X$ is the pair $(\bot,\bot)$ given by the self-adjoint map ${\ensuremath{\mathrm{id}_{}}}^{*} = {\ensuremath{\mathrm{id}_{*}}} = (-)^{\perp} \colon X{\ensuremath{^{\mathrm{op}}}}\rightarrow X$. Composition of $\smash{X \stackrel{f}{\rightarrow} Y \stackrel{g}{\rightarrow} Z}$ is given by: $$\begin{array}{rclcrcl} (g{\mathrel{\circ}}f)_{*} & = & g_{*} {\mathrel{\circ}}\bot {\mathrel{\circ}}f_{*} & \quad\mbox{and}\quad & (g{\mathrel{\circ}}f)^{*} & = & f^{*} {\mathrel{\circ}}\bot {\mathrel{\circ}}g^{*}. \end{array}$$ The category <span>$\mathbf{OMLat}$</span> is the more obvious one, capturing the (universal) algebraic notion of morphism as structure preserving mapping. However, the category <span>$\mathbf{OMLatGal}$</span> has more interesting structure, as we shall see. It arises by restriction from a familiar construction to obtain a (large) dagger category with involutive categories as objects and adjunctions between them, see @Heunen10a. The components $f_{*}\colon X{\ensuremath{^{\mathrm{op}}}}\rightarrow Y$ and $f^{*}\colon Y \rightarrow X{\ensuremath{^{\mathrm{op}}}}$ of a map $f\colon X\rightarrow Y$ in <span>$\mathbf{OMLatGal}$</span> are not required to preserve any structure, but the Galois connection yields that $f_{*}$ preserves meets, as right adjoint, and thus sends joins in $X$ (meets in $X{\ensuremath{^{\mathrm{op}}}}$) to meets in $Y$, and dually, $f^{*}$ preserves joins and sends joins in $Y$ to meets in $X$. The category ${\ensuremath{\mathbf{OMLatGal}}}$ indeed has a dagger, namely by twisting: $$\begin{array}{rcl} (f_*,f^*)^{\dag} & = & (f^*,f_*). \end{array}$$ A morphism $f\colon X \rightarrow Y$ in <span>$\mathbf{OMLatGal}$</span> is a dagger mono precisely when it safisfies $f^*(f_*(x)^\perp)=x^\perp$ for all $x \in X$, because ${{\ensuremath{\mathrm{id}_{}}}}^*(x) = x^\perp = {{\ensuremath{\mathrm{id}_{*}}}}(x)$ and: $$(f^\dag {\mathrel{\circ}}f)^*(x) = f^*(f_*(x)^\perp) = (f^\dag {\mathrel{\circ}}f)_*(x).$$ In a Galois connection like $f^{*} \dashv f_{*}$ one map determines the other. This standard result can be useful in proving equalities. For convenience, we make it explicit. \[MapEqLem\] Suppose we have parallel maps $f,g\colon X\rightarrow Y$ in <span>$\mathbf{OMLatGal}$</span>. In order to prove $f=g$ it suffices to prove either $f_{*} = g_{*}$ or $f^{*}=g^{*}$. We shall prove that $f_{*} = g_{*}$ suffices to obtain also $f^{*}=g^{*}$. For all $x\in X$ and $y\in Y$, $$x\leq f^{*}(y) \Longleftrightarrow y \leq f_{*}(x) = g_{*}(x) \Longleftrightarrow x \leq g^{*}(y).$$ Given $y$ this holds for all $x$, and so in particular for $x = f^{*}(y)$ and $x=g^{*}(y)$, which yields $f^{*}(y) = g^{*}(y)$. ${\square}$ Despite this result we sometimes explicitly write out both equations $f_{*}=g_{*}$ and $f^{*}=g^{*}$, in particular when there is a special argument involved. The following elementary lemma is fundamental. \[DownsetLem\] Let $X$ be an orthomodular lattice, with element $a\in X$. (1) The (principal) downset ${\mathop{\downarrow}\!}a = {\{u\inX\;|\;u \leq a\}}$ is again an orthomodular lattice, with order, conjunctions and disjunctions as in $X$, but with its own orthocomplement $\perp_a$ given by $u^{\perp_a} = a {\mathrel{\wedge}}u^{\perp}$, where $\perp$ is the orthocomplement from $X$. (2) There is a dagger mono ${\mathop{\downarrow}\!}a \rightarrowtail X$ in <span>$\mathbf{OMLatGal}$</span>, for which we also write $a$, with $$\begin{array}{rclcrcl} a_{*}(u) & = & u^{\perp} & \quad\mbox{and}\quad & a^{*}(x) & = & a {\mathrel{\wedge}}x^{\perp}. \end{array}$$ For the first point we check, for $u\in {\mathop{\downarrow}\!}a$, $$u^{\perp_{a}\perp_{a}} = a {\mathrel{\wedge}}(a {\mathrel{\wedge}}u^{\perp})^{\perp} = a {\mathrel{\wedge}}(a^{\perp} {\mathrel{\vee}}u) = u,$$ by orthomodularity, since $u\leq a$. We get a map in <span>$\mathbf{OMLatGal}$</span> because for arbitrary $u\in {\mathop{\downarrow}\!}a$ and $x\in X$, $$x\leq a_{*}(u) = u^{\perp} \Longleftrightarrow u \leq x^{\perp} \Longleftrightarrow u \leq a {\mathrel{\wedge}}x^{\perp} = a^{*}(x).$$ This map $a\colon {\mathop{\downarrow}\!}a\rightarrow X$ is a dagger mono since: $$a^{*}(a_{*}(u)^{\perp}) = a^{*}(u^{\perp\perp}) = a^{*}(u) = a {\mathrel{\wedge}}u^{\perp} = u^{\perp_a}. \eqno{{\square}}$$ We should emphasise that the equation $u^{\perp_{a}\perp_{a}} = u$ only holds for $u\leq a$, and not for arbitrary elements $u$. Later, in Proposition \[DownsetIsKerProp\], we shall see that these maps ${\mathop{\downarrow}\!}a \rightarrowtail X$ are precisely the kernels in the category <span>$\mathbf{OMLatGal}$</span>. But we first show that this category has kernels in the first place. To begin, ${\ensuremath{\mathbf{OMLatGal}}}$ has a zero object ${\ensuremath{\underline{0}}}$, namely the one-element orthomodular lattice $\{*\}$. We can write its unique element as $*=0=1$. Let us show that the lattice ${\ensuremath{\underline{0}}}$ is indeed a final object in ${\ensuremath{\mathbf{OMLatGal}}}$. Let $X$ be an arbitrary orthomodular lattice. The only function $f_* \colon X \to {\ensuremath{\underline{0}}}$ is $f_*(x)=1$. It has an obvious left adjoint $f^* \colon {\ensuremath{\underline{0}}}\to L$ defined by $f^*(1) = 1$: $$\begin{prooftree} x \;\leq\; f^{*}(1)\rlap{$\;=1$} \Justifies 1 \leq 1\rlap{$\;=f_{*}(x)$} \end{prooftree}$$ Likewise, the unique morphism $g\colon {\ensuremath{\underline{0}}}\to Y$ is given by $g_*(1)=1$ and $g^*(y)=1$. Hence the zero morphism $z \colon X \to Y$ is determined by $z_*(x)=1$ and $z^*(y)=1$. \[OMLatGalDagKerCatThm\] The category ${\ensuremath{\mathbf{OMLatGal}}}$ is a dagger kernel category. The (dagger) kernel of a morphism $f \colon X \to Y$ is $k \colon\! {\mathop{\downarrow}\!}k \to X$, where $k = f^*(1) \in X$, as in Lemma \[DownsetLem\]. The composition $f {\mathrel{\circ}}k$ is the zero map ${\mathop{\downarrow}\!}k \rightarrow Y$. First, for $u\in {\mathop{\downarrow}\!}f^{*}(1)$, $$(f {\mathrel{\circ}}k)_*(u) = f_*(k_*(u)^\perp) = f_{*}(u^{\perp\perp}) = f_*(u) = 1,$$ because $u \leq f^*(1)$ in $X$ and so $1 \leq f_*(u)$ in $Y$. And for $y\in Y$, $$(f {\mathrel{\circ}}k)^*(y) = k^*(f^*(y)^\perp) = f^*(y) {\mathrel{\wedge}}f^*(1) = f^*(y {\mathrel{\vee}}1) = f^*(1) = k = 1_{{\mathop{\downarrow}\!}k}.$$ because $f^{*}\colon Y\rightarrow X{\ensuremath{^{\mathrm{op}}}}$ preserves joins as a left adjoint. Let $g\colon Z \to X$, and suppose $g{\mathrel{\circ}}k = 0$. We wish to show that there is a unique morphism $h\colon Z\rightarrow {\mathop{\downarrow}\!}k$ with $g = k {\mathrel{\circ}}h$. We have $f_* {\mathrel{\circ}}{\mathop{\perp}}{\mathrel{\circ}}g_*=1$ and $g^* {\mathrel{\circ}}{\mathop{\perp}}{\mathrel{\circ}}f^* = 1$. Hence for $z \in Z$ we have $1 \leq f_*(g_*(z)^\perp)$, so $g_*(z)^\perp \leq f^*(1) = k$. Define $h_* \colon Z{\ensuremath{^{\mathrm{op}}}}\to {\mathop{\downarrow}\!}k$ by $h_*(z) = g_*(z) {\mathrel{\wedge}}k$, and define $h^* \colon {\mathop{\downarrow}\!}k \to Z{\ensuremath{^{\mathrm{op}}}}$ by $h^*(u) = g^*(u)$. Then $h^* \dashv h_*$ since for $u \leq k$ and $z \in Z$: $$\begin{prooftree} \begin{prooftree} z \;\leq\; g^{*}(u) \rlap{$\;=h^{*}(u)$} \\ \Justifies u \;\leq\; g_{*}(z) \end{prooftree} \Justifies u \;\leq\; g_{*}(z) {\mathrel{\wedge}}k \rlap{$\;=h_{*}(z)$} \end{prooftree}$$ whence $h$ is a well-defined morphism of ${\ensuremath{\mathbf{OMLatGal}}}$. It satisfies: $$\begin{array}{rcl} (k {\mathrel{\circ}}h)_*(z) & = & k_*(h_*(z)^{\perp_{{\mathop{\downarrow}\!}k}}) \\ & = & k_*( (g_*(z) {\mathrel{\wedge}}k )^{\perp_{{\mathop{\downarrow}\!}k}} ) \\ & = & ( (g_*(z) {\mathrel{\wedge}}k )^{\perp_{{\mathop{\downarrow}\!}k}} {\mathrel{\wedge}}k )^\perp \\ & = & ( (g_*(z) {\mathrel{\wedge}}k)^\perp {\mathrel{\wedge}}k {\mathrel{\wedge}}k)^\perp \\ & = & (g_*(z) {\mathrel{\wedge}}k ) {\mathrel{\vee}}k^\perp \\ & = & g_*(z), \end{array}$$ where in the last step we use orthomodularity since $k^{\perp} = f^*(1)^{\perp} \leq g_*(z)$ because $g_*(z)^\perp \leq f^*(1) = k$ which follows from $1 \leq f_*(g_*(z)^\perp)$. Hence $h$ is a mediating morphism satisfying $k {\mathrel{\circ}}h = g$. It is the unique such morphism, since $k$ is a (dagger) mono. ${\square}$ <span> **PROOF:** **ENDPROOF**</span> For convenience we explicitly describe some of the basic structure that results from dagger kernels, see @HeunenJ10a, namely cokernels and factorisations, given by dagger kernels and zero-epis. We start with cokernels and zero-epis. \[CokerLem\] The cokernel of a map $f\colon X\rightarrow Y$ in <span>$\mathbf{OMLatGal}$</span> is: $$\xymatrix@R-1pc{ {\ensuremath{\mathrm{coker}}}(f) = \Big(Y \ar@{-|>}[r]^-{c} & \;{\mathop{\downarrow}\!}f_{*}(1)\Big) \qquad\mbox{with} & {\left\{\begin{array}{rcl} c_{*}(y) & = & y^{\perp} {\mathrel{\wedge}}f_{*}(1) \\ c^{*}(v) & = & v^{\perp}. \\ \end{array}\right.} }$$ Then: $$\mbox{$f$ is zero-epi} \;\;\smash{\stackrel{\textrm{def}}{\Longleftrightarrow}}\;\; {\ensuremath{\mathrm{coker}}}(f) = 0 \;\Longleftrightarrow\; f_{*}(1)=0.$$ Since: $$\xymatrix{ {\ensuremath{\mathrm{coker}}}(f) = \ker(f^{\dag})^{\dag} = \big({\mathop{\downarrow}\!}(f^{\dag})^{*}(1)\ar@{ |>->}[r] & Y\big)^{\dag} = \big(Y \ar@{-|>}[r] & {\mathop{\downarrow}\!}f_{*}(1)\big). }\eqno{{\square}}$$ We recall from @HeunenJ10a that each map $f$ in a dagger kernel category has a zero-epi/kernel factorisation $f = i_{f} {\mathrel{\circ}}e_{f}$. In combination with the factorisation of $f^{\dag}$ it yields a factorisation $f = i_{f} {\mathrel{\circ}}m_{f} {\mathrel{\circ}}(i_{f^{\dag}})^{\dag}$ as in: $$\xymatrix@R-1pc{ X\ar[rrr]^-{f}\ar@{-|>}[dr]_{(i_{f^\dag})^{\dag}} & & & Y \\ & {\ensuremath{\mathrm{Im}}}(f^{\dag})\ar@{ >->>}|{\circ}[r]_-{m_f} & {\ensuremath{\mathrm{Im}}}(f)\ar@{ |>->}[ur]_{i_f} & }$$ where the map $m_f$ is both zero-epic and zero-monic, and where $m_{f} {\mathrel{\circ}}(i_{f^{\dag}})^{\dag} = e_{f}$, the zero-epic part of $f$. \[ImFacLem\] For a map $f\colon X\rightarrow Y$ in <span>$\mathbf{OMLatGal}$</span> one has: $$\xymatrix@R-2pc@C-1pc{ \Big({\ensuremath{\mathrm{Im}}}(f) = {\mathop{\downarrow}\!}(f_{*}(1)^{\perp}) \ar@{ |>->}[r]^-{i_f} & Y\Big) \qquad\rlap{with} & {\left\{\begin{array}{rcl} (i_{f})_{*}(v) & = & v^{\perp} \\ (i_{f})^{*}(y) & = & y^{\perp} {\mathrel{\wedge}}f_{*}(1)^{\perp} \\ \end{array}\right.} \\ \Big(X \ar@{->>}[r]^-{e_f}|-{\circ} & {\mathop{\downarrow}\!}f_{*}(1)^{\perp}\Big) \quad\mbox{is} & {\left\{\begin{array}{rcl} (e_{f})_{*}(x) & = & f_{*}(x) {\mathrel{\wedge}}f_{*}(1)^{\perp} \\ (e_{f})^{*}(v) & = & f^{*}(v) \end{array}\right.} \\ \Big({\mathop{\downarrow}\!}f^{*}(1)^{\perp} \ar@{ >->>}[r]^-{m_f}|-{\circ} & {\mathop{\downarrow}\!}f_{*}(1)^{\perp}\Big) \quad\mbox{is} & {\left\{\begin{array}{rcl} (m_{f})_{*}(x) & = & f_{*}(x) {\mathrel{\wedge}}f_{*}(1)^{\perp} \\ (m_{f})^{*}(v) & = & f^{*}(v) {\mathrel{\wedge}}f^{*}(1)^{\perp}. \end{array}\right.} \\ }$$ This is just a matter of unravelling definitions. For instance, $$\xymatrix{ {\ensuremath{\mathrm{Im}}}(f) = \ker({\ensuremath{\mathrm{coker}}}(f)) = \ker\big(Y \ar@{-|>}[r]^-{c} & {\mathop{\downarrow}\!}f_{*}(1)\big) = \big({\mathop{\downarrow}\!}f_{*}(1)^{\perp} \;\ar@{ |>->}[r] & Y\big). }$$ since $c^{*}(1_{{\mathop{\downarrow}\!}f_{*}(1)}) = c^{*}(f_{*}(1)) = f_{*}(1)^{\perp}$. We check that $i_{f} {\mathrel{\circ}}e_{f} = f$, as required. $$\begin{array}{rcl} (i_{f} {\mathrel{\circ}}e_{f})_{*}(x) & = & (i_{f})_{*}((e_{f})_{*}(x)^{\perp_{f_{*}(1)^{\perp}}}) \\ & = & \big((e_{f})_{*}(x)^{\perp}{\mathrel{\wedge}}f_{*}(1)^{\perp}\big)^{\perp} \\ & = & (f_{*}(x) {\mathrel{\wedge}}f_{*}(1)^{\perp}) {\mathrel{\vee}}f_{*}(1) \\ & = & f_{*}(x), \end{array}$$ by orthomodularity, using that $f_{*}(1) \leq f_{*}(x)$, since $x\leq 1$. This map $e_f$ is indeed zero-epic by the previous lemma, since: $$(e_{f})_{*}(1) = f_{*}(1) {\mathrel{\wedge}}f_{*}(1)^{\perp} = 0.$$ Next we first observe: $$f_{*}(x {\mathrel{\vee}}f^{*}(1)) = f_{*}(x) {\mathrel{\wedge}}f_{*}(f^{*}(1)) = f_{*}(x) {\mathrel{\wedge}}1 = f_{*}(x),\eqno{(*)}$$ since there is a "unit" $1 \leq f_{*}(f^{*}(1))$. We use this twice, in the marked equations, in: $$\begin{array}[b]{rcl} (m_{f} {\mathrel{\circ}}(i_{f^\dag})^{\dag})_{*}(x) & = & \big((m_{f})_{*} {\mathrel{\circ}}(-)^{\perp_{f^{*}(1)^{\perp}}} {\mathrel{\circ}}(i_{f^{\dag}})^{*}\big)(x) \\ & = & (m_{f})_{*}\big(f^{*}(1)^{\perp} {\mathrel{\wedge}}((f^{\dag})_{*}(1)^{\perp} {\mathrel{\wedge}}x^{\perp})^{\perp}\big) \\ & = & f_{*}\big(f^{*}(1)^{\perp} {\mathrel{\wedge}}(f^{*}(1) {\mathrel{\vee}}x)\big) {\mathrel{\wedge}}f_{*}(1)^{\perp} \\ & \smash{\stackrel{(*)}{=}} & f_{*}\big(f^{*}(1) {\mathrel{\vee}}(f^{*}(1)^{\perp} {\mathrel{\wedge}}(f^{*}(1) {\mathrel{\vee}}x))\big) {\mathrel{\wedge}}f_{*}(1)^{\perp} \\ & = & f_{*}(f^{*}(1) {\mathrel{\vee}}x) {\mathrel{\wedge}}f_{*}(1)^{\perp} \\ & \smash{\stackrel{(*)}{=}} & f_{*}(x) {\mathrel{\wedge}}f_{*}(1)^{\perp} \\ & = & (e_{f})_{*}(x). \end{array}$$ The map $m_f$ is zero-epic since: $$\begin{array}{rcl} (m_{f})_{*}(1_{{\mathop{\downarrow}\!}f^{*}(1)^{\perp}}) \hspace*{\arraycolsep} = \hspace*{\arraycolsep} (m_{f})_{*}(f^{*}(1)^{\perp}) & = & f_{*}(f^{*}(1)^{\perp}) {\mathrel{\wedge}}f_{*}(1)^{\perp} \\ & \smash{\stackrel{(*)}{=}} & f_{*}(f^{*}(1) {\mathrel{\vee}}f^{*}(1)^{\perp}) {\mathrel{\wedge}}f_{*}(1)^{\perp} \\ & = & f_{*}(1) {\mathrel{\wedge}}f_{*}(1)^{\perp} \\ & = & 0. \end{array}$$ Similarly one shows that $m_f$ is zero-monic. ${\square}$ <span> **PROOF:** **ENDPROOF**</span> For the record, inverse and direct images are described explicitly. \[InvDirImLem\] For a map $f\colon X\rightarrow Y$ in <span>$\mathbf{OMLatGal}$</span> the associated inverse and direct images are: $$\xymatrix@R-2pc{ {\ensuremath{\mathrm{KSub}}}(Y)\ar[r]^-{f^{-1}} & {\ensuremath{\mathrm{KSub}}}(X) & {\ensuremath{\mathrm{KSub}}}(X)\ar[r]^-{\exists_f} & {\ensuremath{\mathrm{KSub}}}(Y) \\ \big({\mathop{\downarrow}\!}b\to Y\big)\ar@{|->}[r] & \big({\mathop{\downarrow}\!}f^{*}(b^{\perp}) \to X\big) & \big({\mathop{\downarrow}\!}a\to X\big)\ar@{|->}[r] & \big({\mathop{\downarrow}\!}(f_{*}(a)^{\perp}) \to Y\big) }$$ For $f\colon X\rightarrow Y$ and $b\in Y$, we have, using the formulation for pullback of kernels from Section \[DagKerSec\] (or @HeunenJ10a [Lemma 2.4]) and Lemma \[ImFacLem\] above, $$\begin{array}{rcll} \lefteqn{f^{-1}({\mathop{\downarrow}\!}b \rightarrow Y)} \\ & = & \ker({\ensuremath{\mathrm{coker}}}({\mathop{\downarrow}\!}b\rightarrow Y) {\mathrel{\circ}}f) \\ & = & \ker((Y\rightarrow {\mathop{\downarrow}\!}c) {\mathrel{\circ}}f), & \mbox{for } c \begin{array}[t]{ll} = & b_{*}(1_{{\mathop{\downarrow}\!}b}) = (1_{{\mathop{\downarrow}\!}b})^{\perp} = b^{\perp} \end{array} \\ & = & {\mathop{\downarrow}\!}a \rightarrow X, & \mbox{for } a \begin{array}[t]{ll} = & (c^{\dag} {\mathrel{\circ}}f)^{*}(1_{{\mathop{\downarrow}\!}b}) = f^{*}(c_{*}(1_{{\mathop{\downarrow}\!}c})^{\perp}) \\ = & f^{*}(c^{\perp\perp}) = f^{*}(c) = f^{*}(b^{\perp}) \end{array} \\ & = & {\mathop{\downarrow}\!}f^{*}(b^{\perp}) \rightarrow X. \end{array}$$ For $\exists_f$ we also use Lemma \[ImFacLem\] in: $$\begin{array}[b]{rcll} \lefteqn{\exists_{f}({\mathop{\downarrow}\!}a \rightarrow X)} \\ & = & {\ensuremath{\mathrm{Im}}}(f {\mathrel{\circ}}({\mathop{\downarrow}\!}a\rightarrow X)) \\ & = & {\mathop{\downarrow}\!}b\rightarrow Y, & \mbox{where } b = (f{\mathrel{\circ}}a)_{*}(1_{{\mathop{\downarrow}\!}a})^{\perp} = f_{*}(a_{*}(1_{{\mathop{\downarrow}\!}a})^{\perp})^{\perp} = f_{*}(a^{\perp\perp})^{\perp} \\ & = & {\mathop{\downarrow}\!}(f_{*}(a)^{\perp}) \rightarrow Y. \end{array}\eqno{{\square}}$$ As in any dagger kernel category, the kernel posets ${\ensuremath{\mathrm{KSub}}}(X)$ of <span>$\mathbf{OMLatGal}$</span> are orthomodular lattices. They turn out to be isomorphic to the underlying object $X\in{\ensuremath{\mathbf{OMLatGal}}}$. \[DownsetIsKerProp\] Each dagger mono $a\colon\! {\mathop{\downarrow}\!}a\rightarrowtail X$ from Lemma \[DownsetLem\], for $a\in X$, is actually a dagger kernel in <span>$\mathbf{OMLatGal}$</span>. This yields an isomorphism of orthomodular lattices $$\simsjonathan@example.com{ X \ar[r]^-{\cong} & {\ensuremath{\mathrm{KSub}}}(X), \quad\mbox{namely}\quad a\ar@{|->}[r] & \big({\mathop{\downarrow}\!}a\ar[r]^-{a} & X\big). }$$ It is natural in the sense that for $f\colon X\rightarrow Y$ in <span>$\mathbf{OMLatGal}$</span> the following squares commute, by Lemma \[InvDirImLem\]. $$\xymatrix@R-1pc{ X\ar[d]_{\cong}\ar[rr]^-{\bot \,{\mathrel{\circ}}\, f_{*}} & & Y\ar[d]^{\cong}\ar[rr]^-{f^{*}{\mathrel{\circ}}\bot} & & X\ar[d]^{\cong} \\ {\ensuremath{\mathrm{KSub}}}(X)\ar[rr]_-{\exists_f} & & {\ensuremath{\mathrm{KSub}}}(Y)\ar[rr]_-{f^{-1}} & & {\ensuremath{\mathrm{KSub}}}(X) }$$ We first check that the map $a\colon\! {\mathop{\downarrow}\!}a \rightarrow X$ is indeed a kernel, namely of its cokernel ${\ensuremath{\mathrm{coker}}}(a)\colon X\rightarrow {\mathop{\downarrow}\!}a_{*}(1)$, see Lemma \[CokerLem\], where $a_{*}(1) = a_{*}(1_{{\mathop{\downarrow}\!}a}) = a_{*}(a) = a^{\perp}$. Thus, $\ker({\ensuremath{\mathrm{coker}}}(a)) = {\ensuremath{\mathrm{coker}}}(a)^{*}(1) = {\ensuremath{\mathrm{coker}}}(a)^{*}(1_{{\mathop{\downarrow}\!}a^{\perp}}) = {\ensuremath{\mathrm{coker}}}(a)^{*}(a^{\perp}) = a^{\perp\perp} = a$. Theorem \[OMLatGalDagKerCatThm\] says that the mapping $X \rightarrow {\ensuremath{\mathrm{KSub}}}(X)$ is surjective. Here we shall show that it is an injective homomorphism of orthomodular lattices reflecting the order, so that it is an isomorphism in the category <span>$\mathbf{OMLat}$</span>. Assume that $a\leq b$ in $X$. We can define $\varphi \colon {\mathop{\downarrow}\!}a \rightarrow {\mathop{\downarrow}\!}b$ by $\varphi_{*}(x) = x^{\perp_{b}} = b {\mathrel{\wedge}}x^{\perp}$ and $\varphi^{*}(y) = a {\mathrel{\wedge}}y^{\perp}$, for $x\in{\mathop{\downarrow}\!}a$ and $y\in {\mathop{\downarrow}\!}b$. Then, clearly, $y\leq \varphi_{*}(x)$ iff $x\leq \varphi^{*}(y)$, so that $\varphi$ is a morphism in <span>$\mathbf{OMLatGal}$</span>. In order to show $a \leq b$ in ${\ensuremath{\mathrm{KSub}}}(X)$ we prove $b{\mathrel{\circ}}\varphi = a$. First, for $x\in {\mathop{\downarrow}\!}a$, $$\begin{array}{rcl} (b {\mathrel{\circ}}\varphi)_{*}(x) & = & b_{*}\big(\varphi_{*}(x)^{\perp_{b}}\big) \\ & = & b_{*}\big(x^{\perp_{b}\perp_{b}}\big) \\ & = & b_{*}(x) \qquad\mbox{because $x\in{\mathop{\downarrow}\!}a\subseteq {\mathop{\downarrow}\!}b$} \\ & = & x^{\perp} \\ & = & a_{*}(x). \end{array}$$ <span> **PROOF:** **ENDPROOF**</span> The map $X \rightarrow {\ensuremath{\mathrm{KSub}}}(X)$ not only preserves the order, but also reflects it: if we have an arbitrary map $\psi\colon {\mathop{\downarrow}\!}a \rightarrow {\mathop{\downarrow}\!}b$ in <span>$\mathbf{OMLatGal}$</span> with $b{\mathrel{\circ}}\psi = a$, then: $$\begin{array}{rcl} a \hspace*{\arraycolsep} = \hspace*{\arraycolsep} a^{\perp\perp} \hspace*{\arraycolsep} = \hspace*{\arraycolsep} a_{*}(a)^{\perp} & = & (b {\mathrel{\circ}}\psi)_{*}(a)^{\perp} \\ & = & b_{*}(\psi_{*}(a)^{\perp_{b}})^{\perp} \\ & = & \psi_{*}(a)^{\perp_{b}\perp\perp} \\ & = & \psi_{*}(a)^{\perp_{b}} \\ & = & b {\mathrel{\wedge}}\psi_{*}(a)^{\perp} \hspace*{\arraycolsep} \leq \hspace*{\arraycolsep} b. \end{array}$$ This map $X\rightarrow {\ensuremath{\mathrm{KSub}}}(X)$ also preserves $\perp$, since $$\xymatrix{ \big({\mathop{\downarrow}\!}a\ar@{ |>->}[r]^-{a} & X\big)^{\perp} = \ker(a^{\dag}) = \big({\mathop{\downarrow}\!}b\ar@{ |>->}[r]^-{b} & X\big) }$$ where, according to Theorem \[OMLatGalDagKerCatThm\], $b = (a^{\dag})^{*}(1_{{\mathop{\downarrow}\!}a}) = a_{*}(a) = a^{\perp}$. It remains to show that the mapping $X\rightarrow {\ensuremath{\mathrm{KSub}}}(X)$ preserves finite conjunctions. It is almost immediate that it sends the top element $1\in X$ to the identity map (top) in ${\ensuremath{\mathrm{KSub}}}(X)$. It also preserves finite conjunctions, since the intersection of the kernels ${\mathop{\downarrow}\!}a\rightarrow X$ and ${\mathop{\downarrow}\!}b\rightarrow X$ is given by ${\mathop{\downarrow}\!}(a{\mathrel{\wedge}}b)\rightarrow X$. Since $a{\mathrel{\wedge}}b \leq a, b$ there are appropriate maps ${\mathop{\downarrow}\!}(a{\mathrel{\wedge}}b) \rightarrow {\mathop{\downarrow}\!}a$ and ${\mathop{\downarrow}\!}(a{\mathrel{\wedge}}b) \rightarrow {\mathop{\downarrow}\!}b$. Suppose that we have maps $k \rightarrow {\mathop{\downarrow}\!}a$ and $k\rightarrow {\mathop{\downarrow}\!}b$, where $k \colon {\mathop{\downarrow}\!}f^{*}(1)\rightarrow X$ is a kernel of $f\colon X\rightarrow Y$. Since, as we have seen, the order is reflected, we get $f^{*}(1) \leq a, b$, and thus $f^{*}(1) \leq a{\mathrel{\wedge}}b$, yielding the required map ${\mathop{\downarrow}\!}f^{*}(1) \rightarrow {\mathop{\downarrow}\!}(a{\mathrel{\wedge}}b)$. ${\square}$ The adjunction $\exists_{f} \dashv f^{-1}$ that exists in arbitrary dagger kernel categories (see Section \[DagKerSec\] or @HeunenJ10a [Proposition 4.3]) boils down in our example <span>$\mathbf{OMLatGal}$</span> to the adjunction between $f^{*} \dashv f_{*}$ in the definition of morphisms in <span>$\mathbf{OMLatGal}$</span>, since: $$\begin{array}{rcl} \exists_{f}({\mathop{\downarrow}\!}a\rightarrow X) \leq ({\mathop{\downarrow}\!}b\rightarrow Y) & \Longleftrightarrow & ({\mathop{\downarrow}\!}f_{*}(a)^{\perp} \rightarrow Y) \leq ({\mathop{\downarrow}\!}b\rightarrow Y) \\ & \Longleftrightarrow & f_{*}(a)^{\perp} \leq b \\ & \Longleftrightarrow & b^{\perp} \leq f_{*}(a) \\ & \Longleftrightarrow & a \leq f^{*}(b^{\perp}) \\ & \Longleftrightarrow & ({\mathop{\downarrow}\!}a \rightarrow X) \leq ({\mathop{\downarrow}\!}f^{*}(b^{\perp}) \rightarrow X) \\ & \Longleftrightarrow & ({\mathop{\downarrow}\!}a \rightarrow X) \leq f^{-1}({\mathop{\downarrow}\!}b \rightarrow X). \end{array}$$ Moreover, the Sasaki hook ${\mathrel{\supset}}$ and and-then operators ${\mathrel{\&}}$ defined categorically in @HeunenJ10a [Proposition 6.1], see Section \[DagKerSec\], amount in <span>$\mathbf{OMLatGal}$</span> to their usual definitions in the theory of orthomodular lattices, see *e.g.* @Finch70 [@Kalmbach83]. This will be illustrated next. We use the "effect" ${\mathfrak{E}({\mathop{\downarrow}\!}a\rightarrow X)} = a {\mathrel{\circ}}a^{\dag} \colon X\rightarrow X$ associated with a kernel in: $$({\mathop{\downarrow}\!}a\rightarrow X) {\mathrel{\supset}}({\mathop{\downarrow}\!}b\rightarrow X) \;\smash{\stackrel{\textrm{def}}{=}}\; {\mathfrak{E}({\mathop{\downarrow}\!}a\rightarrow X)}^{-1}({\mathop{\downarrow}\!}b\rightarrow X) = ({\mathop{\downarrow}\!}c\rightarrow X),$$ where, according to the description of inverse image $(-)^{-1}$ in the previous lemma, $$c = (a {\mathrel{\circ}}a^{\dag})^{*}(b^{\perp}) = a_{*}\big(a^{*}(b^{\perp})^{\perp_a}\big) = \big(a {\mathrel{\wedge}}(a {\mathrel{\wedge}}b)^{\perp}\big)^{\perp} = a^{\perp} {\mathrel{\vee}}(a{\mathrel{\wedge}}b) = a {\mathrel{\supset}}b.$$ Similarly for and-then ${\mathrel{\&}}$: $$({\mathop{\downarrow}\!}a\rightarrow X) {\mathrel{\&}}({\mathop{\downarrow}\!}b\rightarrow X) \;\smash{\stackrel{\textrm{def}}{=}}\; \exists_{{\mathfrak{E}({\mathop{\downarrow}\!}b\rightarrow X)}}({\mathop{\downarrow}\!}a\rightarrow X) = ({\mathop{\downarrow}\!}c\rightarrow X),$$ where the description of direct image from Lemma \[InvDirImLem\] yields: $$c = (b {\mathrel{\circ}}b^{\dag})_{*}(a)^{\perp} = b_{*}\big(b^{*}(a)^{\perp_b}\big)^{\perp} = \big(b {\mathrel{\wedge}}(b {\mathrel{\wedge}}a^{\perp})^{\perp}\big)^{\perp\perp} = b {\mathrel{\wedge}}(b^{\perp} {\mathrel{\vee}}a) = a {\mathrel{\&}}b.$$ These ${\mathrel{\&}}$ and ${\mathrel{\supset}}$ are, by construction, related via an adjunction (see also @Finch70 [@CoeckeS04]). Also one can define a weakest precondition modality $[f]$ from dynamic logic in this setting: for $f\colon X\rightarrow Y$ and $y\in Y$, put: $$\begin{array}{rcl} [f](y) & \smash{\stackrel{\textrm{def}}{=}} & f^{*}(y^{\perp}). \end{array}$$ for "$y$ holds after $f$". This operation $[f](-)$ preserves conjunctions, as usual. An element $a\in X$ yields a test operation $a? = {\mathfrak{E}(a)} = a {\mathrel{\circ}}a^{\dag}$. Then one can recover the Sasaki hook $a {\mathrel{\supset}}b$ via this modality as $[a?]b$, and hence complement $a^\perp$ as $[a?]0$, see also *e.g.* @BaltagS06. There is another isomorphism of interest in this setting. \[PointLem\] Let $2 = \{0,1\}$ be the 2-element Boolean algebra, considered as an orthomodular lattice $2\in{\ensuremath{\mathbf{OMLatGal}}}$. For each orthomodular lattice $X$, there is an isomorphism (of sets): $$\xymatrix{ X \ar[r]^-{\cong} & {\ensuremath{\mathbf{OMLatGal}}}(2, X) }$$ which maps $a\in X$ to $\overline{a}\colon 2\rightarrow X$ given by: $$\begin{array}{rclcrcl} \overline{a}_{*}(w) & = & \left\{\begin{array}{ll} 1 & \mbox{if }w=0 \\ a^{\perp} & \mbox{if }w=1 \end{array}\right. & \qquad & \overline{a}^{*}(x) & = & \left\{\begin{array}{ll} 1 & \mbox{if }x\leq a^{\perp} \\ 0 & \mbox{otherwise.} \end{array}\right. \end{array}$$ This isomorphism is natural: for $f\colon X\rightarrow Y$ one has: $$\xymatrix@R-1pc{ X\ar[d]_{\cong}\ar[rr]^-{\bot\,{\mathrel{\circ}}\,f_{*}} & & Y\ar[d]^{\cong} \\ {\ensuremath{\mathbf{OMLatGal}}}(2,X)\ar[rr]^-{f{\mathrel{\circ}}-} & & {\ensuremath{\mathbf{OMLatGal}}}(2, Y) }$$ The thing to note is that for a map $g\colon 2\rightarrow X$ in <span>$\mathbf{OMLatGal}$</span> we have $g_{*}(0) = 1$ because $g_{*}\colon 2{\ensuremath{^{\mathrm{op}}}}\rightarrow X$ is a right adjoint. Hence we can only choose $g_{*}(1) \in X$. Once this is chosen, the left adjoint $g^{*}\colon X\rightarrow 2{\ensuremath{^{\mathrm{op}}}}$ is completely determined, namely as $1 \leq g^{*}(x)$ iff $x\leq g_{*}(1)$. As to naturality, it suffices to show: $$\begin{array}[b]{rcl} (f {\mathrel{\circ}}\overline{a})_{*}(1) & = & f_{*}(\overline{a}_{*}(1)^{\perp}) \\ & = & f_{*}(a^{\perp\perp}) \\ & = & f_{*}(a)^{\perp\perp} \\ & = & \overline{f_{*}(a)^{\perp}}_{*}(1) \\ & = & \overline{(\bot\,{\mathrel{\circ}}\,f_{*})(a)}_{*}(1). \end{array}\eqno{{\square}}$$ By combining the previous two results we obtain a way to classify (kernel) subobjects, as in a topos @MacLaneM92, but with naturality working in the opposite direction. In @HeunenJ10a a similar structure was found in the category <span><span>$\mathbf{Rel}$</span></span>of sets and relations, and also in the dagger kernel category associated with a Boolean algebra. \[OpClassCor\] The 2-element lattice $2\in{\ensuremath{\mathbf{OMLatGal}}}$ is an "opclassifier": there is a "characteristic" isomorphism: $$\xymatrix{ {\ensuremath{\mathrm{KSub}}}(X) \ar[r]^-{{\ensuremath{\mathrm{char}}}}_-{\cong} & {\ensuremath{\mathbf{OMLatGal}}}(2, X). }$$ which is natural: ${\ensuremath{\mathrm{char}}}{\mathrel{\circ}}\exists_{f} = f {\mathrel{\circ}}{\ensuremath{\mathrm{char}}}$. ${\square}$ We conclude our investigation of the category <span>$\mathbf{OMLatGal}$</span> with the following observation. \[BiprodProp\] The category ${\ensuremath{\mathbf{OMLatGal}}}$ has (finite) dagger biproducts $\oplus$. Explicitly, $X_1 \oplus X_2$ is the Cartesian product of (underlying sets of) orthomodular lattices, with coprojection $\kappa_1\colon X_1 \to X_1 \oplus X_2$ defined by $(\kappa_1)_*(x) = (x^\perp,1)$ and $(\kappa_1)^*(x,y) = x^\perp$. The dual product structure is given by $\pi_i = (\kappa_i)^\dag$. Let us first verify that $\kappa_1$ is a well-defined morphism of ${\ensuremath{\mathbf{OMLatGal}}}$, *i.e.* that $(\kappa_1)^* \dashv (\kappa_1)_*$: $$\begin{prooftree} \begin{prooftree} z \;\leq\; x^{\perp} \rlap{$\;=(\kappa_{1})^{*}(x,y)$} \Justifies x \;\leq\; z^{\perp} \end{prooftree} \Justifies (x,y) \;\leq\; (z^{\perp}, 1) \rlap{$\;=(\kappa_{1})_{*}(z)$} \end{prooftree}$$ Also, $\kappa_1$ is a dagger mono since: $$(\kappa_{1})^{*}\big((\kappa_{1})_{*}(x)^{\perp}\big) = (\kappa_{1})^{*}\big((x^{\perp}, 1)^{\perp}\big) = (\kappa_{1})^{*}\big(x,0\big) = x^{\perp}.$$ Likewise, there is a dagger mono $\kappa_2 \colon X_2 \to X_1 \oplus X_2$. For $i \neq j$, one finds that $(\kappa_j)^\dag {\mathrel{\circ}}\kappa_i$ is the zero morphism. <span> **PROOF:** **ENDPROOF**</span> In order to show that $X_1 \oplus X_2$ is indeed a coproduct, suppose that morphisms $f_i \colon X_i \to Y$ are given. We then define the cotuple ${\ensuremath{[ f_1,\,f_2 ]}} \colon X_1 \oplus X_2 \to Y$ by ${\ensuremath{[ f_1,\,f_2 ]}}_*(x_1,x_2) = (f_1)_*(x_1) {\mathrel{\wedge}}(f_2)_*(x_2)$ and ${\ensuremath{[ f_1,\,f_2 ]}}^*(y) = (f_1^*(y), f_2^*(y))$. Clearly, ${\ensuremath{[ f_1,\,f_2 ]}}^* \dashv {\ensuremath{[ f_1,\,f_2 ]}}_*$, and: <span> **PROOF:** **ENDPROOF**</span> $$\begin{array}{rcl} ({\ensuremath{[ f_1,\,f_2 ]}} {\mathrel{\circ}}\kappa_1)_*(x) & = & {\ensuremath{[ f_1,\,f_2 ]}}_*\big((\kappa_1)_*(x)^\perp\big) \\ & = & {\ensuremath{[ f_1,\,f_2 ]}}_*\big((x^{\perp},1)^{\perp}\big) \\ & = & (f_1)_*(x) {\mathrel{\wedge}}(f_2)_*(0) \\ & = & (f_1)_*(x) {\mathrel{\wedge}}1 \\ & = & (f_1)_*(x). \end{array}$$ <span> **PROOF:** **ENDPROOF**</span> so that ${\ensuremath{[ f_1,\,f_2 ]}} {\mathrel{\circ}}\kappa_1 = f_1$. Likewise, ${\ensuremath{[ f_1,\,f_2 ]}} {\mathrel{\circ}}\kappa_2 = f_2$. Moreover, if $g\colon X_{1}\oplus X_{2}\rightarrow Y$ also satisfies $g{\mathrel{\circ}}\kappa_{i} = f_{i}$, then: $$\begin{array}[b]{rcl} {\ensuremath{[ f_1,\,f_2 ]}}_{*}(x_{1},x_{2}) & = & (f_1)_*(x_1) {\mathrel{\wedge}}(f_2)_*(x_2) \\ & = & g_{*}\big((\kappa_{1})_{*}(x_{1})^{\perp}\big) {\mathrel{\wedge}}g_{*}\big((\kappa_{2})_{*}(x_{2})^{\perp}\big) \\ & = & g_{*}\big((x_{1}^{\perp},1)^{\perp}\big) {\mathrel{\wedge}}g_{*}\big((1,x_{2}^{\perp})^{\perp}\big) \\ & = & g_{*}\big(x_{1},0\big) {\mathrel{\wedge}}g_{*}\big(0,x_{2}\big) \\ & = & g_{*}\big((x_{1},0) {\mathrel{\vee}}(0,x_{2})\big) \\ & = & g_{*}\big(x_{1},x_{2}\big). \end{array}\eqno{{\square}}$$ From dagger kernel categories to orthomodular lattices ------------------------------------------------------ The aim in this subsection is to show that for an arbitrary dagger kernel <span>$\mathbf{D}$</span> the kernel subobject functor ${\ensuremath{\mathrm{KSub}}}(-)$ is a functor ${\ensuremath{\mathbf{D}}} \rightarrow {\ensuremath{\mathbf{OMLatGal}}}$. On a morphism $f\colon X \to Y$ of ${\ensuremath{\mathbf{D}}}$, define ${\ensuremath{\mathrm{KSub}}}(f) \colon {\ensuremath{\mathrm{KSub}}}(X) \to {\ensuremath{\mathrm{KSub}}}(Y)$ by: $$\begin{array}{rclcrcl} {\ensuremath{\mathrm{KSub}}}(f)_{*}(m) & = & \big(\exists_{f}(m)\big)^{\perp} & \qquad & {\ensuremath{\mathrm{KSub}}}(f)^{*}(n) & = & f^{-1}\big(n^{\perp}\big). \end{array}$$ Then indeed ${\ensuremath{\mathrm{KSub}}}(f)^* \dashv {\ensuremath{\mathrm{KSub}}}(f)_*$, via $\exists_{f} \dashv f^{-1}$, $$\begin{prooftree} n \;\leq\; (\exists_{f}(m))^{\perp} \rlap{$\;={\ensuremath{\mathrm{KSub}}}(f)_{*}(m)$} \Justifies \begin{prooftree} \exists_{f}(m) \;\leq\; n^{\perp} \Justifies m \;\leq\; f^{-1}(n^{\perp}) \rlap{$\;={\ensuremath{\mathrm{KSub}}}(f)^{*}(n)$} \end{prooftree} \end{prooftree}$$ <span> **PROOF:** **ENDPROOF**</span> The functor ${\ensuremath{\mathrm{KSub}}}(-)$ preserves the relevant structure. This requires the following auxiliary result. \[lem:kernelschangeofbase\] In a dagger kernel category, for any kernel $k\colon K \rightarrowtail X$ in ${\ensuremath{\mathrm{KSub}}}(X)$, there is an order isomorphism ${\ensuremath{\mathrm{KSub}}}(K) \cong {\mathop{\downarrow}\!}k \subseteq {\ensuremath{\mathrm{KSub}}}(X)$. The direction ${\ensuremath{\mathrm{KSub}}}(K) \to {\mathop{\downarrow}\!}k$ of the desired bijection is given by $m \mapsto k {\mathrel{\circ}}m$. This is well-defined since kernels are closed under composition. The other direction ${\mathop{\downarrow}\!}k \to {\ensuremath{\mathrm{KSub}}}(K)$ is $n \mapsto \varphi = k^{\dag} {\mathrel{\circ}}n$, where $n = k {\mathrel{\circ}}\varphi$. One easily checks that these maps are each other's inverse, and preserve the order. ${\square}$ \[KSubPreservationThm\] Let ${\ensuremath{\mathbf{D}}}$ be a dagger kernel category. The functor ${\ensuremath{\mathrm{KSub}}}\colon {\ensuremath{\mathbf{D}}} \to {\ensuremath{\mathbf{OMLatGal}}}$ is a map of dagger kernel categories. Preservation of daggers follows because $f^{-1}$ and $\exists_f$ are inter-expressible, see Section \[DagKerSec\] and @HeunenJ10a [Proposition 4.3]: $${\ensuremath{\mathrm{KSub}}}(f^{\dag})_{*}(n) = \big(\exists_{f^{\dag}}(n))^{\perp} = f^{-1}(n^{\perp}) = {\ensuremath{\mathrm{KSub}}}(f)^{*}(n) = \big({\ensuremath{\mathrm{KSub}}}(f)^{\dag}\big)_{*}(n).$$ Preservation of the zero object is easy: ${\ensuremath{\mathrm{KSub}}}(0) = \{0\}={\ensuremath{\underline{0}}}$. Next, let $k\colon K \to X$ be the kernel of a morphism $f \colon X \to Y$ in ${\ensuremath{\mathbf{D}}}$. We recall from @HeunenJ10a [Corollary 2.5 (ii)] that this kernel $k$ can be described as inverse image $k = f^{-1}(0) = f^{-1}(1^{\perp}) = {\ensuremath{\mathrm{KSub}}}(f)^{*}(1)$. Hence by Lemmas \[lem:kernelschangeofbase\] and \[DownsetLem\], we have the isomorphism on the left in: $$\xymatrix@R-2pc@C+2pc{ {\ensuremath{\mathrm{KSub}}}(K)\ar@{ |>->}[dr]^-{{\ensuremath{\mathrm{KSub}}}(k)}\ar[dd]_{k{\mathrel{\circ}}-}^{\cong} \\ & {\ensuremath{\mathrm{KSub}}}(X)\ar[r]^-{{\ensuremath{\mathrm{KSub}}}(f)} & {\ensuremath{\mathrm{KSub}}}(Y) \\ {\mathop{\downarrow}\!}k\ar@{ |>->}[ur]_{k} }$$ It yields a commuting triangle since for $n\in{\ensuremath{\mathrm{KSub}}}(K)$, $${\ensuremath{\mathrm{KSub}}}(k)_{*}(n) = \exists_k(n)^{\perp} = (k{\mathrel{\circ}}n)^{\perp} = k_{*}(k{\mathrel{\circ}}n).$$ Similarly for $m\in{\ensuremath{\mathrm{KSub}}}(X)$, $$k{\mathrel{\circ}}{\ensuremath{\mathrm{KSub}}}(k)^{*}(m) = k{\mathrel{\circ}}k^{-1}(m^\perp) = k {\mathrel{\wedge}}m^{\perp} = k^{*}(m).\eqno{{\square}}$$ At this stage we conclude that these ${\ensuremath{\mathrm{KSub}}}$ functors yield a well-behaved translation of a dagger kernel category into a collection of orthomodular lattices, indexed by the objects of the category. For the special case ${\ensuremath{\mathbf{D}}} = {\ensuremath{\mathbf{OMLatGal}}}$, the functor ${\ensuremath{\mathrm{KSub}}}\colon {\ensuremath{\mathbf{D}}} \rightarrow {\ensuremath{\mathbf{OMLatGal}}}$ is the identity, up to isomorphism, by Proposition \[DownsetIsKerProp\]. A translation in the other direction, from orthomodular lattices to dagger kernel categories will be postponed until after the next section, after we have seen the translation from Foulis semigroups to orthomodular lattices. \[HardingRem\] As pointed out by John Harding, the functor ${\ensuremath{\mathrm{KSub}}}\colon {\ensuremath{\mathbf{D}}} \to {\ensuremath{\mathbf{OMLatGal}}}$ need not preserve biproducts that exist in <span>$\mathbf{D}$</span>. For instance if we take <span>$\mathbf{D}$</span> to be the category of Hilbert spaces over $\mathbb{R}$, then ${\ensuremath{\mathrm{KSub}}}(\mathbb{R})$ is a two-element set, containing $\{0\}$ and $\mathbb{R}$ itself. However, ${\ensuremath{\mathrm{KSub}}}(\mathbb{R} \oplus \mathbb{R}) = {\ensuremath{\mathrm{KSub}}}(\mathbb{R}^{2})$ is much bigger than ${\ensuremath{\mathrm{KSub}}}(\mathbb{R})\times{\ensuremath{\mathrm{KSub}}}(\mathbb{R})$, since every line through the origin forms a closed subspace of $\mathbb{R}^{2}$. In the remainder of this section we shall briefly consider two special subcategories of <span>$\mathbf{OMLatGal}$</span>, namely with Boolean and with complete orthomodular lattices. The Boolean case {#BooleanSubsec} ---------------- Let ${\ensuremath{\mathbf{BoolGal}}} \hookrightarrow {\ensuremath{\mathbf{OMLatGal}}}$ be the full subcategory of Boolean algebras with (antitone) Galois connections between them. We recall that a Boolean algebra can be described as an orthomodular lattice that is distributive. The main (and only) result of this subsection is simple. \[BoolGalStructProp\] The category <span>$\mathbf{BoolGal}$</span> inherits dagger kernels and biproducts from <span>$\mathbf{OMLatGal}$</span>. Moreover, as a dagger kernel category it is Boolean. An arbitrary map $f\colon X\rightarrow Y$ in <span>$\mathbf{BoolGal}$</span> has a kernel ${\mathop{\downarrow}\!}f^{*}(1) \rightarrow X$ as in Theorem \[OMLatGalDagKerCatThm\] for orthomodular lattices because the downset ${\mathop{\downarrow}\!}f^{*}(1)$ is a Boolean algebra. Similarly, the biproducts from Proposition \[BiprodProp\] also exist in <span>$\mathbf{BoolGal}$</span> because $X_{1}\oplus X_{2}$ is a Boolean algebra if $X_{1}$ and $X_{2}$ are Boolean algebras. For each $X\in{\ensuremath{\mathbf{BoolGal}}}$ one has ${\ensuremath{\mathrm{KSub}}}(X) \cong X$ so that ${\ensuremath{\mathrm{KSub}}}(X)$ is a Boolean algebra. Hence <span>$\mathbf{BoolGal}$</span> is a Boolean dagger kernel category by @HeunenJ10a [Theorem 6.2]. ${\square}$ <span> **PROOF:** **ENDPROOF**</span> Boolean algebras thus give rise to (Boolean) dagger kernel categories on two different levels: the "large" category <span>$\mathbf{BoolGal}$</span> of all Boolean algebras is a dagger kernel category, but also each individual Boolean algebra can be turned into a "small" dagger kernel category, see @HeunenJ10a [Proposition 3.5]. Complete orthomodular lattices {#CompleteSubsec} ------------------------------ We shall write ${\ensuremath{\mathbf{OMSupGal}}}\hookrightarrow {\ensuremath{\mathbf{OMLatGal}}}$ for the full subcategory of orthomodular lattices that are complete, *i.e.* that have joins $\bigvee U$ (and thus also meets $\bigwedge U$) of all subsets $U$ (and not just the finite ones). Notice that the functor ${\ensuremath{\mathrm{KSub}}}\colon {\ensuremath{\mathbf{D}}} \rightarrow {\ensuremath{\mathbf{OMLatGal}}}$ from Theorem \[KSubPreservationThm\] is actually a functor ${\ensuremath{\mathrm{KSub}}}\colon {\ensuremath{\mathbf{D}}} \rightarrow {\ensuremath{\mathbf{OMSupGal}}}$ for <span>$\mathbf{D}$</span> = <span><span>$\mathbf{Rel}$</span></span>, <span><span>$\mathbf{PInj}$</span></span>, <span><span>$\mathbf{Hilb}$</span></span>. A morphism $f\colon X\rightarrow Y$ in <span>$\mathbf{OMSupGal}$</span> is completely determined by either $f_{*}\colon X{\ensuremath{^{\mathrm{op}}}}\rightarrow Y$ preserving all meets, or by $f^{*}\colon Y\rightarrow X{\ensuremath{^{\mathrm{op}}}}$ preserving all joins. This forms the basis for the next result. \[FreeOMLatGalProp\] The forgetful functor $U\colon {\ensuremath{\mathbf{OMSupGal}}} \to {{\ensuremath{\mathbf{Sets}}}\xspace}$ given by $X\mapsto X$ on objects and $f\mapsto f_{*} {\mathrel{\circ}}\bot$ on morphisms has a left adjoint $F$ given by $F(A) = {\mathcal{P}}{A}$, with $F(g)_{*}(U \subseteq A) = \neg\coprod_{g}(U) = \neg{\{g(a)\;|\;a\in U\}}$ and $F(g)^{*}(V\subseteq B) = g^{-1}(\neg V) = {\{a\;|\;g(a)\not\in V\}}$, for $g\colon A\rightarrow B$ in ${{\ensuremath{\mathbf{Sets}}}\xspace}$. For $A\in{{\ensuremath{\mathbf{Sets}}}\xspace}$ and $X\in{\ensuremath{\mathbf{OMSupGal}}}$ there is a bijective correspondence: $$\begin{prooftree} {\xymatrix{{\mathcal{P}}{A}\ar[r]^-{f} & X\rlap{\quad in {\ensuremath{\mathbf{OMSupGal}}}}}} \Justifies {\xymatrix{A\ar[r]_-{g} & X\rlap{\quad in {{\ensuremath{\mathbf{Sets}}}\xspace}}}} \end{prooftree}$$ given by $\overline{f}(a) = f_{*}(\{a\})^{\perp}$ and $\overline{g}_{*}(U) = \bigwedge_{a\in U}g(a)^{\perp}$ with $\overline{g}^{*}(x) = {\{a\inA\;|\;g(a) \leq x^{\perp}\}}$. Then: $$\begin{array}{rcl} x\leq \overline{g}_{*}(U) = \bigwedge_{a\in U}g(a)^{\perp} & \Longleftrightarrow & {\forall_{a\inU}.\,x\leq g(a)^{\perp}} \\ & \Longleftrightarrow & {\forall_{a\inU}.\,g(a) \leq x^{\perp}} \\ & \Longleftrightarrow & U \subseteq {\{a\inA\;|\;g(a) \leq x^{\perp}\}} = \overline{g}^{*}(x). \end{array}$$ Further, $$\begin{array}[b]{rcl} \overline{\overline{g}}(a) & = & \textstyle \overline{g}_{*}(\{a\})^{\perp} = \big(\bigwedge_{b\in\{a\}}g(b)^{\perp}\big)^{\perp} = g(a)^{\perp\perp} = g(a). \\ \overline{\overline{f}}_{*}(U) & = & \textstyle \bigwedge_{a\in U} \overline{f}(a)^{\perp} = \bigwedge_{a\in U} f_{*}(\{a\})^{\perp\perp} = f_{*}(\bigcup_{a\in U}\{a\}) = f_{*}(U) \\ \overline{\overline{f}}^{*}(x) & = & \textstyle {\{a\;|\;\overline{f}(a) \leq x^{\perp}\}} = {\{a\;|\;f_{*}(\{a\})^{\perp} \leq x^{\perp}\}} = {\{a\;|\;x \leq f_{*}(\{a\})\}} \\ & = & {\{a\;|\;\{a\}\subseteq f^{*}(x)\}} = f^{*}(x). \end{array}\eqno{{\square}}$$ <span> **PROOF:** **ENDPROOF**</span> The left adjoint $F$ of this adjunction between <span>$\mathbf{OMSupGal}$</span> and <span><span>$\mathbf{Sets}$</span></span>factors via the graph functor $\mathcal{G}\colon {{\ensuremath{\mathbf{Sets}}}\xspace}\rightarrow {{\ensuremath{\mathbf{Rel}}}\xspace}$, as in: $$\xymatrix@R-2pc@C+1pc{ & {{\ensuremath{\mathbf{Rel}}}\xspace}\ar@/^1ex/[dr]^(0.4){{\ensuremath{\mathrm{KSub}}}} \\ {{\ensuremath{\mathbf{Sets}}}\xspace}\ar@/^1ex/[ur]^-{\mathcal{G}} & \quad\bot & {\ensuremath{\mathbf{OMSupGal}}}\ar@/^2ex/[ll]^{U} }$$ It is not hard to see that the kernels from Theorem \[OMLatGalDagKerCatThm\] and biproducts $\oplus$ from Proposition \[BiprodProp\] also exist in <span>$\mathbf{OMSupGal}$</span>. For instance, the join of a subset $U\subseteq X\oplus Y$ is given as pair of joins: $$\begin{array}{rcl} \bigvee U & = & (\bigvee{\{x\;|\;{\exists_{y}.\,(x,y)\in U}\}}, \bigvee{\{y\;|\;{\exists_{x}.\,(x,y)\in U}\}}). \end{array}$$ Hence <span>$\mathbf{OMSupGal}$</span> is also a dagger kernel category with dagger biproducts. Foulis semigroups and dagger kernel categories {#FoulisDagKerSec} ============================================== In this section we shall relate dagger kernel categories and Foulis semigroups. Postponing the formal definition, we first illustrate that these Foulis semigroups arise quite naturally in the context of kernel dagger categories. In every category <span>$\mathbf{D}$</span> the homset ${\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(X)} = {\ensuremath{\mathbf{D}}}(X, X)$ of endomaps $f\colon X\rightarrow X$ is a monoid (or semigroup with unit), with obvious composition operation ${\mathrel{\circ}}$ and identity map ${\ensuremath{\mathrm{id}_{X}}}$ as unit element. If <span>$\mathbf{D}$</span> is a dagger category, there is automatically an involution $(-)^\dag$ on this monoid. If it is moreover a dagger kernel category, every endomap $s\in{\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(X)}$ yields a self-adjoint idempotent, namely the effect of its kernel: $$\label{DagKerSaiEqn} \begin{array}{rcccl} {[\,s\,]} & \smash{\stackrel{\textrm{def}}{=}} & {\mathfrak{E}(\ker(s))} & = & \ker(s) {\mathrel{\circ}}\ker(s)^{\dag} \;\colon\; X\longrightarrow X \end{array}$$ with the special property that for $t\in{\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(X)}$, $$\begin{array}{rcl} s{\mathrel{\circ}}t = 0 & \Longleftrightarrow & {\exists_{r\in{\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(X)}}.\,t = {[\,s\,]} {\mathrel{\circ}}r}. \end{array}$$ Indeed, if $t={[\,s\,]}{\mathrel{\circ}}r$, then: $$s {\mathrel{\circ}}t = s {\mathrel{\circ}}\ker(s) {\mathrel{\circ}}\ker(s)^{\dag} {\mathrel{\circ}}r = 0 {\mathrel{\circ}}\ker(s)^{\dag} {\mathrel{\circ}}r = 0.$$ Conversely, if $s{\mathrel{\circ}}t = 0$, then there is a map $f$ in <span>$\mathbf{D}$</span> with $\ker(s) {\mathrel{\circ}}f = t$. Hence $t$ satisfies: $${[\,s\,]} {\mathrel{\circ}}t = \ker(s) {\mathrel{\circ}}\ker(s)^{\dag} {\mathrel{\circ}}\ker(s) {\mathrel{\circ}}f = \ker(s) {\mathrel{\circ}}f = t.$$ In the 1960s this structure of an involutive monoid $\langle{\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(X)}, {\mathrel{\circ}}, {\ensuremath{\mathrm{id}_{}}}, \dag\rangle$ with operation ${[\,-\,]}\colon {\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(X)} \rightarrow {\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(X)}$ was introduced by Foulis @Foulis60 [@Foulis62; @Foulis63] and has since been studied under the name 'Baer \*-semigroup', and later as 'Foulis semigroup', see @Kalmbach83 [Chapter 5, §§18] for a brief overview. \[FoulisDef\] A Foulis semigroup consists of a monoid (semigroup with unit) $(S, \cdot, 1)$ together with two endomaps $(-)^{\dag} \colon S\rightarrow S$ and ${[\,-\,]} \colon S\rightarrow S$ satisfying: (1) $1^{\dag} = 1$ and $(s\cdot t)^{\dag} = t^{\dag}\cdot s^{\dag}$ and $s^{\dag\dag} = s$, making $S$ an involutive monoid; (2) ${[\,s\,]}$ is a self-adjoint idempotent, *i.e.* satisfies ${[\,s\,]} \cdot {[\,s\,]} = {[\,s\,]} = {[\,s\,]}^{\dag}$; (3) $0 \;\smash{\stackrel{\textrm{def}}{=}}\; {[\,1\,]}$ is a zero element: $0 \cdot s = 0 = s\cdot 0$; (4) $s\cdot x = 0$ iff ${\exists_{y}.\,x = {[\,s\,]}\cdot y}$. Or, equivalently (see @Kalmbach83 [Chapter 5, §§18, Lemma 1]), 1. ${[\,0\,]} = 1$ and $s \cdot {[\,s\,]} = 0$ and $t = {[\,{[\,t^{\dag} \cdot s^{\dag}\,]}\cdot s\,]}\cdot t$. We form a category <span>$\mathbf{Fsg}$</span> of such Foulis semigroups with monoid homomorphisms that commute with $\dag$ and ${[\,-\,]}$ as morphisms. <span> **PROOF:** **ENDPROOF**</span> The constructions before this definition show that for each object $X\in{\ensuremath{\mathbf{D}}}$ of a (locally small) dagger kernel category <span>$\mathbf{D}$</span>, the homset ${\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(X)} = {\ensuremath{\mathbf{D}}}(X, X)$ of endomaps on $X$ is a Foulis semigroup. Functoriality of this construction is problematic: for an arbitrary map $f\colon X\rightarrow Y$ in <span>$\mathbf{D}$</span> there is a mapping ${\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(X)} \rightarrow {\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(Y)}$, namely $s\mapsto f {\mathrel{\circ}}s {\mathrel{\circ}}f^{\dag} \colon Y\rightarrow X\rightarrow X\rightarrow Y$, but it does not preserve the structure of Foulis semigroups, and thus only gives rise to presheaf. \[DagKer2FoulisProp\] For a dagger kernel category <span>$\mathbf{D}$</span>, each endo homset ${\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(X)}$, for $X\in{\ensuremath{\mathbf{D}}}$, is a Foulis semigroup. The mapping $X\mapsto {\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(X)}$ yields a presheaf ${\ensuremath{\mathbf{D}}} \rightarrow {{\ensuremath{\mathbf{Sets}}}\xspace}$. ${\square}$ The lack of functoriality in this construction is problematic. One possible way to address it is via another notion of morphism between Foulis semigroups, like Galois connections between orthomodular lattices in the category <span>$\mathbf{OMLatGal}$</span>. We shall not go deeper into this issue. Also the possible sheaf-theoretic aspects involved in this situation (see also @GravesS73) form a topic on its own that is not pursued here. We briefly consider some examples. For the dagger kernel category <span><span>$\mathbf{Hilb}$</span></span>of Hilbert spaces, the set $\mathcal{B}(H)$ of (bounded/continuous linear) endomaps on a Hilbert space $H$ forms a Foulis semigroup—but of course also a $C^*$-algebra. The associated (Foulis) map ${[\,-\,]}\colon \mathcal{B}(H)\rightarrow \mathcal{B}(H)$ maps $s\colon H\rightarrow H$ to ${[\,s\,]}\colon H\rightarrow H$ given by ${[\,s\,]}(x) = k(k^{\dag}(x))$, where $k$ is the kernel map ${\{x\;|\;s(x)=0\}} \hookrightarrow H$. For the category <span><span>$\mathbf{Rel}$</span></span>of sets and relations the endomaps on a set $X$ are the relations $R\subseteq X\times X$ on $X$. The associated ${[\,R\,]} \subseteq X\times X$ is ${\{(x,x)\;|\;\neg{\exists_{y}.\,R(x,y)}\}}$. An interesting situation arises when we apply the previous proposition to the dagger kernel category <span>$\mathbf{OMLatGal}$</span> of orthomodular lattices (with Galois connections between them). One gets that for each orthomodular lattice $X$ the endo-homset ${\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(X)} = {\ensuremath{\mathbf{OMLatGal}}}(X, X)$ forms a Foulis semigroup. This construction is more than 40 years old, see @Foulis60 or *e.g.* @BlythJ72 [Chapter II, Section 19] or @Kalmbach83 [Chapter 5, §§18], where it is described in terms of Galois connections. In the present setting it comes for free, from the structure of the category <span>$\mathbf{OMLatGal}$</span>. Hence we present it as a corollary, in particular of Proposition \[DagKer2FoulisProp\] and Theorem \[OMLatGalDagKerCatThm\]. \[OMLat2FoulisCor\] For each orthomodular lattice $X$ the set of (Galois) endomaps ${\mathcal{E}{\kern-.5ex}\textit{n}{\kern-.2ex}\textit{d}{\kern-.2ex}\textit{o}(X)} = {\ensuremath{\mathbf{OMLatGal}}}(X,X)$ is a Foulis semigroup with composition as monoid, dagger $(-)^{\dag}$ as involution, and self-adjoint idempotent ${[\,s\,]}\colon X\rightarrow X$, for $s\colon X\rightarrow X$, defined as in (\[DagKerSaiEqn\]). Equivalently, ${[\,s\,]}$ can be described via the Sasaki hook ${\mathrel{\supset}}$ or and-then operator ${\mathrel{\&}}$: $${[\,s\,]}_{*}(x) = {[\,s\,]}^{*}(x) = s^{*}(1) {\mathrel{\supset}}x^{\perp} = s^{*}(1)^{\perp} {\mathrel{\vee}}(s^{*}(1) {\mathrel{\wedge}}x^{\perp}) = (x{\mathrel{\&}}s^{*}(1))^{\perp}.$$ We recall from (\[DagKerSaiEqn\]) that the operation ${[\,-\,]}$ on endomaps $s\colon X\rightarrow X$ is defined as ${[\,s\,]} = \ker(s) {\mathrel{\circ}}\ker(s)^{\dag} \colon X\rightarrow X$. In <span>$\mathbf{OMLatGal}$</span> one has $\ker(s) = s^{*}(1)$—see Proposition \[DownsetIsKerProp\]—so that: $$\begin{array}[b]{rcl} {[\,s\,]}_{*}(x) & = & (\ker(s) {\mathrel{\circ}}\ker(s)^{\dag})_{*}(x) \\ & = & (\ker(s)_{*}(\ker(s)^{*}(x)^{\perp}) \\ & = & s^{*}(1)_{*}\big(s^{*}(1) {\mathrel{\wedge}}s^{*}(1)^{*}(x)^{\perp}\big) \\ & = & \big(s^{*}(1) {\mathrel{\wedge}}(s^{*}(1) {\mathrel{\wedge}}x^{\perp})^{\perp}\big)^{\perp} \qquad\mbox{by Lemma~\ref{DownsetLem}} \\ &= & s^{*}(1)^{\perp} {\mathrel{\vee}}(s^{*}(1) {\mathrel{\wedge}}x^{\perp}). \end{array}\eqno{{\square}}$$ <span> **PROOF:** **ENDPROOF**</span> From Foulis semigroups to dagger kernel categories -------------------------------------------------- Each involutive monoid $(S, \cdot, 1, \dag)$ forms a dagger category with one object, and morphisms given by elements of $S$. Requirement (4) in Definition \[FoulisDef\] says that this category has "semi" kernels, given by ${[\,-\,]}$. Hence it is natural to apply the Karoubi envelope to obtain proper kernels. It turns out that this indeed yields a dagger kernel category. For a Foulis semigroup as in Definition \[FoulisDef\], we thus write ${\mathcal{K}^{\dag}(S)}$ for the dagger Karoubi envelope applied to $S$ as one-object dagger category. Thus ${\mathcal{K}^{\dag}(S)}$ has self-adjoint idempotents $s\in S$ as objects, and morphisms $f\colon s\rightarrow t$ given by elements $f\in S$ with $f\cdot s = f = t\cdot f$. \[Foulis2DagKerThm\] This ${\mathcal{K}^{\dag}(S)}$ is a dagger kernel category. The mapping $S\mapsto {\mathcal{K}^{\dag}(S)}$ yields a functor ${\ensuremath{\mathbf{Fsg}}} \rightarrow {\ensuremath{\mathbf{DKC}}}$. The zero element $0 = {[\,1\,]} \in S$ is obviously a self-adjoint idempotent, and thus an object of ${\mathcal{K}^{\dag}(S)}$. It is a zero object because for each $s\in{\mathcal{K}^{\dag}(S)}$ there is precisely one map $f\colon s\rightarrow 0$, namely $0$, because $f = 0\cdot f = 0$. For an arbitrary map $f\colon s\rightarrow t$ in ${\mathcal{K}^{\dag}(S)}$ we claim that there is a dagger kernel of the form: $$\xymatrix{ s\cdot {[\,f\,]} \ar@{ |>->}[rr]^-{s\cdot {[\,f\,]}} & & s\ar[rr]^-{f} & & t }$$ This will be checked in a number of small steps. 1. $f\cdot (s\cdot {[\,f\,]}) = (f\cdot s) \cdot {[\,f\,]} = f\cdot {[\,f\,]} = 0$, by $(4')$ in Defintion \[FoulisDef\]; 2. By the previous point there is an element $y\in S$ with $s\cdot {[\,f\,]} = {[\,f\,]}\cdot y$. Hence: $${[\,f\,]}\cdot s\cdot {[\,f\,]} = {[\,f\,]}\cdot {[\,f\,]} \cdot y = {[\,f\,]}\cdot y = s\cdot {[\,f\,]}$$ This is equation is very useful. It yields first of all that $s\cdot {[\,f\,]}$ is idempotent: $$(s\cdot {[\,f\,]})\cdot (s\cdot {[\,f\,]}) = s\cdot ({[\,f\,]}\cdot s\cdot {[\,f\,]}) = s\cdot s\cdot {[\,f\,]} = s\cdot {[\,f\,]}.$$ This element is also self-adjoint: $$(s\cdot {[\,f\,]})^{\dag} = ({[\,f\,]}\cdot s\cdot {[\,f\,]})^{\dag} = {[\,f\,]}^{\dag} \cdot s^{\dag} \cdot {[\,f\,]}^{\dag} = {[\,f\,]}\cdot s\cdot {[\,f\,]} = s\cdot {[\,f\,]}.$$ Hence $s\cdot {[\,f\,]}\in S$ is a self-adjoint idempotent, and thus an object of ${\mathcal{K}^{\dag}(S)}$. 3. $s\cdot {[\,f\,]}\colon (s\cdot {[\,f\,]})\rightarrow s$ is also a dagger mono: $$\begin{array}{rcl} (s\cdot {[\,f\,]})^{\dag} \cdot (s\cdot {[\,f\,]}) & = & {[\,f\,]}^{\dag} \cdot s^{\dag} \cdot s \cdot {[\,f\,]} \\ & = & {[\,f\,]} \cdot s \cdot s \cdot {[\,f\,]} \\ & = & {[\,f\,]} \cdot s \cdot {[\,f\,]} \\ & = & s\cdot {[\,f\,]} \\ & =
{'source': 'arXiv_out/0912'}