An Adjunction Between Boolean Algebras and a Subcategory of Stone Algebras

Inigo Incer

( Computing and Mathematical Sciences
California Institute of Technology
[email protected] )

Abstract

We consider Stone algebras with a distinguished element $e$ satisfying the identity $e\to x=\neg\neg x$ for all elements $x$ of the algebra. We provide an adjunction between the category of such algebras and that of Boolean algebras.

1 Introduction

The algebra of contracts [1, 2] has been an object of attention in computer science and engineering due to its capability to support compositional design. Given a Boolean algebra $B$ , its contract algebra $\mathbf{C}(B)$ has elements $(a,g)\in B^{2}$ such that $a\lor g=1_{B}$ . $\mathbf{C}(B)$ is a Stone algebra with operations $(a,g)\land(a^{\prime},g^{\prime})=(a\lor a^{\prime},g\land g^{\prime})$ , $(a,g)\lor(a^{\prime},g^{\prime})=(a\land a^{\prime},g\lor g^{\prime})$ , and $(a^{\prime},g^{\prime})\to(a,g)=((a\land\neg a^{\prime})\lor(g^{\prime}\land\neg g),\neg g^{\prime}\lor g)$ . The top and bottom elements of this algebra are, respectively, $1=(0_{B},1_{B})$ and $0=(1_{B},0_{B})$ . This note introduces a subcategory of Stone algebras with the property that the contract functor is the left adjoint of the functor that maps these algebras to their closures.

2 Augmented Stone Algebras

First we recall the definition of Stone algebras. Then we introduce the concept of an augmented Stone algebra.

Definition 2.1.

A Stone algebra $S$ is a Heyting algebra satisfying $\neg x\lor\mathrm{Clos}(x)=1_{S}$ for all $x\in S$ , where $\neg x=x\to 0$ and $\mathrm{Clos}(x)$ is the closure of $x$ : $\mathrm{Clos}(x)=\neg\neg x$ . We say that $x$ is closed if $\mathrm{Clos}(x)=x$ . We say $x$ is dense if $\mathrm{Clos}(x)=1_{S}$ .

Definition 2.2.

We say $(S,\land,\lor,\to,1,0,e)$ is an augmented Stone algebra if $(S,\land,\lor,\to,1,0)$ is a Stone algebra and $e\in S$ , called the closure element, satisfies $e\to x=\mathrm{Clos}(x)$ for all $x\in S$ .

Notation 2.3.

Let $\mathbf{Bool}$ be the category of Boolean algebras, and $\mathbf{augStone}$ that of augmented Stone algebras. We define $\mathrm{Clos}\colon\mathbf{augStone}\to\mathbf{Bool}$ as the functor that maps an extended Stone algebra to its Boolean algebra of closed elements.

Example 2.4.

Any Boolean algebra $B$ is an augmented Stone algebra with $e_{B}=1_{B}$ . $\mathbf{C}(B)$ is an augmented Stone algebra with $e=(1_{B},1_{B})$ .

Let us prove some elementary facts about augmented Stone algebras.

Proposition 2.5.

Let $S$ be an augmented Stone algebra.

(i)

$\mathrm{Clos}(e)=1$ .
(ii)

The closure element is unique.
(iii)

$y\to e$ is dense for all $y\in S$ .
(iv)

If $x\in S$ is closed, $x\to y=\neg x\lor y$ .

Proof.

(i)

$1=e\to e=\mathrm{Clos}(e)$ .
(ii)

Suppose $e$ and $e^{\prime}$ are closure elements. Then $e\to e^{\prime}=\mathrm{Clos}(e^{\prime})=1$ , whence $e\leq e^{\prime}$ . By the same reasoning, $e^{\prime}\leq e$ , and so $e=e^{\prime}$ .
(iii)

$\mathrm{Clos}(y\to e)=e\to(y\to e)=y\to(e\to e)=1$ .
(iv)

For $a\in S$ , we have $a\leq x\to y\Leftrightarrow a\land x\leq y\Leftrightarrow(a\land x)\lor\neg x\leq y\lor\neg x\Leftrightarrow(a\land x)\lor\neg x\lor(\neg x\land a)\leq y\lor\neg x\Leftrightarrow a\leq y\lor\neg x$ .∎

Proposition 2.6.

$\mathbf{C}$ is a functor $\mathbf{C}\colon\mathbf{Bool}\to\mathbf{augStone}$ .

Proof.

Given $B\in\mathbf{Obj}(\mathbf{Bool})$ , we know that $\mathbf{C}(B)\in\mathbf{Obj}(\mathbf{augStone})$ from Section 1 and Example 2.4. Given a map $f\in\hom_{\mathbf{Bool}}(B,B^{\prime})$ , we have $\mathbf{C}(f)(a,g)=(fa,fg)\in\mathbf{C}(B^{\prime})$ as $f(a)\lor f(g)=f(a\lor g)=1_{B^{\prime}}$ . Moreover, $\mathbf{C}(f)(1)=1$ , $\mathbf{C}(f)(0)=0$ , and $\mathbf{C}(f)(e)=e$ . We also have

	$\displaystyle\mathbf{C}(f)((a,g)\land(a^{\prime},g^{\prime}))$	$\displaystyle=\mathbf{C}(f)((a\lor a^{\prime},g\land g^{\prime}))=((f(a)\lor f(a^{\prime}),f(g)\land f(g^{\prime})))$
		$\displaystyle=\mathbf{C}(f)(a,g)\land\mathbf{C}(f)(a^{\prime},g^{\prime}),$
	$\displaystyle\mathbf{C}(f)((a,g)\lor(a^{\prime},g^{\prime}))$	$\displaystyle=\mathbf{C}(f)((a\land a^{\prime},g\lor g^{\prime}))=((f(a)\land f(a^{\prime}),f(g)\lor f(g^{\prime})))$
		$\displaystyle=\mathbf{C}(f)(a,g)\lor\mathbf{C}(f)(a^{\prime},g^{\prime}),$
and
	$\displaystyle\mathbf{C}(f)((a^{\prime},g^{\prime})\to(a,g))$	$\displaystyle=\mathbf{C}(f)(((g^{\prime}\to g)\to(a\land\neg a^{\prime}),g\to g^{\prime}))$
		$\displaystyle=(((fg^{\prime}\to fg)\to(fa\land\neg fa^{\prime}),fg\to fg^{\prime}))$
		$\displaystyle=\mathbf{C}(f)(a^{\prime},g^{\prime})\to\mathbf{C}(f)(a,g).\qed$

3 An adjunction between $\mathbf{Bool}$ and $\mathbf{augStone}$

Let $B\in\mathbf{Obj}(\mathbf{Bool})$ and $S\in\mathbf{Obj}(\mathbf{augStone})$ . For $(a,g)\in\mathbf{C}(B)$ , we let $\pi_{1}(a,g)=a$ and $\pi_{2}(a,g)=g$ , and for $x\in B$ , we let $\Delta x=(\neg x,x)$ .

Proposition 3.1.

Let $f\in\hom_{\mathbf{Bool}}(B,\mathrm{Clos}(S))$ . The assignment

\alpha_{B,S}\colon f\mapsto f\pi_{2}\land(f\pi_{1}\to e_{S})

is a set morphism $\alpha_{B,S}\colon\hom_{\mathbf{Bool}}(B,\mathrm{Clos}(S))\to\hom_{\mathbf{augStone}}(\mathbf{C}(B),S)$ .

Proof.

Let $f^{*}=\alpha_{B,S}f$ and $c,c^{\prime}\in\mathbf{C}(B)$ , where $c=(a,g)$ and $c^{\prime}=(a^{\prime},g^{\prime})$ .

•

$f^{*}(0)=f(0_{B})\land(f(1_{B})\to e_{S})=0_{S}$ .
•

$f^{*}(1)=f(1_{B})\land(f(0_{B})\to e_{S})=1_{S}$ .
•

$f^{*}(e)=f(1_{B})\land(f(1_{B})\to e_{S})=e_{S}$ .
•

$\begin{aligned} f^{*}&\left(c\land c^{\prime}\right)=f^{*}(a\lor a^{\prime},g\land g^{\prime})=f(g\land g^{\prime})\land(f(a\lor a^{\prime})\to e)\\ &=f(g)\land f(g^{\prime})\land(f(a)\to e)\land(f(a^{\prime})\to e)=f^{*}c\land f^{*}c^{\prime}.\end{aligned}$

•

$\begin{aligned} f^{*}&\left(c\lor c^{\prime}\right)=f^{*}(a\land a^{\prime},g\lor g^{\prime})=f(g\lor g^{\prime})\land(f(a\land a^{\prime})\to e)\\ &=\left(f(g)\land(f(a)\land f(a^{\prime})\to e)\right)\lor\left(f(g^{\prime})\land(f(a)\land f(a^{\prime})\to e)\right).\end{aligned}$
Since $a^{\prime}\lor g^{\prime}=1_{B}$ , we have $\neg a^{\prime}\leq g^{\prime}$ . Thus,

	$\displaystyle f^{*}\left(c\lor c^{\prime}\right)=$	$\displaystyle\left(f(g)\land(f(a)\land f(a^{\prime})\to e)\right)\lor$
		$\displaystyle\left(f(g^{\prime})\land(f(a)\land f(a^{\prime})\to e)\right)\lor\left(\neg f(a^{\prime})\land(f(a)\land f(a^{\prime})\to e)\right)$
	$\displaystyle=$	$\displaystyle\left(f(g)\land(f(a)\land f(a^{\prime})\to e)\right)\lor\left(f(g^{\prime})\land(f(a)\land f(a^{\prime})\to e)\right)$
		$\displaystyle\lor\neg f(a^{\prime}).$

The last equality follows from the fact that $\neg f(a^{\prime})\leq f(a)\land f(a^{\prime})\to e$ . We conclude that

f^{*}\left(c\lor c^{\prime}\right)=\left(f(g)\land(f(a)\to e)\right)\lor\left(f(g^{\prime})\land(f(a)\land f(a^{\prime})\to e)\right).

(1)

By applying an analogous procedure, we obtain

f^{*}\left(c\lor c^{\prime}\right)=\left(f(g)\land(f(a)\land f(a^{\prime})\to e)\right)\lor\left(f(g^{\prime})\land(f(a^{\prime})\to e)\right).

Conjoining this expression with (1) yields

	$\displaystyle f^{*}\left(c\lor c^{\prime}\right)$	$\displaystyle=\left(f(g)\land(f(a)\to e)\right)\lor\left(f(g^{\prime})\land(f(a^{\prime})\to e)\right)$
		$\displaystyle=f^{}c\lor f^{}c^{\prime}.$

•

$\begin{aligned} f^{*}&\left(c^{\prime}\to c\right)\\ &=f(g^{\prime}\to g)\land\left(f\left((a\land\neg a^{\prime})\lor\neg(g^{\prime}\to g)\right)\to e\right)\\ &=f(g^{\prime}\to g)\land\left(\neg f(a\land\neg a^{\prime})\land f(g^{\prime}\to g)\lor e\right)\\ &=f(g^{\prime}\to g)\land\left(f(a\land\neg a^{\prime})\to e\right)\\ &=f(g^{\prime}\to g)\land f(\neg a^{\prime}\to g)\land\left(f(a\land\neg a^{\prime})\to e\right)\end{aligned}$

The last equality follows from the fact that $\neg a^{\prime}\leq g^{\prime}$ . We have

	$\displaystyle f^{*}$	$\displaystyle\left(c^{\prime}\to c\right)$
		$\displaystyle=(f(g^{\prime})\land e\to f(g)\land(f(a)\to e))\land(\neg f(a^{\prime})\to f(g)\land(f(a)\to e)),$
which holds because $f(g^{\prime}\to g)=f(g^{\prime})\land(e\to f(g)\land(f(a)\to e))$ . We finally obtain
	$\displaystyle f^{*}$	$\displaystyle\left(c^{\prime}\to c\right)=(\neg f(a^{\prime})\lor f(g^{\prime})\land e)\to(f(g)\land(f(a)\to e))$
		$\displaystyle=f(g^{\prime})\land(f(a^{\prime})\to e)\to(f(g)\land(f(a)\to e))$
		$\displaystyle=f^{}c^{\prime}\to f^{}c.\qed$

Proposition 3.2.

Let $f^{*}\in\hom_{\mathbf{augStone}}(\mathbf{C}(B),S)$ . The assignment

\beta_{B,S}\colon f^{*}\mapsto f^{*}\Delta

is a set morphism $\beta_{B,S}\colon\hom_{\mathbf{augStone}}(\mathbf{C}(B),S)\to\hom_{\mathbf{Bool}}(B,\mathrm{Clos}(S))$ . Moreover, $\alpha_{B,S}$ and $\beta_{B,S}$ are inverses.

Proof.

Let $b,b^{\prime}\in B$ and set $f=\beta_{B,S}f^{*}$ . We have $f(0_{B})=f^{*}\Delta 0_{B}=f^{*}0=0$ . Now we study the Boolean operations: $f(b\land b^{\prime})=f^{*}(\neg(b\land b^{\prime}),b\land b^{\prime})=f^{*}b\land f^{*}b^{\prime}=fb\land fb^{\prime}$ . $f(b\lor b^{\prime})=f^{*}(\neg(b\lor b^{\prime}),b\lor b^{\prime})=f^{*}b\lor f^{*}b^{\prime}=fb\lor fb^{\prime}$ . $f(\neg b)=f^{*}(\neg(b\to 0_{B}),b\to 0_{B})=f^{*}((\neg b,b)\to 0)=fb\to 0=\neg fb$ . Regarding the second part, let $(a,g)\in\mathbf{C}(B)$ . We have $(\alpha_{B,S}\beta_{B,S}f^{*})(a,g)=(\alpha_{B,S}f^{*}\Delta)(a,g)=(f^{*}\Delta\pi_{2}\land(f^{*}\Delta\pi_{1}\to e_{S}))(a,g)=f^{*}(\neg g,g)\land(f^{*}(\neg a,a)\to e_{S})=f^{*}\left((\neg g,g)\land((\neg a,a)\to e)\right)=f^{*}\left((\neg g,g)\land((a,1))\right)=f^{*}(a,g)$ and $(\beta_{B,S}\alpha_{B,S}f)(b)=(f\pi_{2}\Delta\land(f\pi_{1}\Delta\to e_{S}))(b)=f(b)\land(f(\neg b)\to e_{S})=f(b)\land(f(b)\lor e_{S})=f(b)$ . ∎

Corollary 3.3.

$\mathbf{C}$ is fully faithful.

Proof.

Let $B$ be a Boolean algebra. The maps $\Delta\colon B\to\mathrm{Clos}(\mathbf{C}(B))$ and $\pi_{2}\colon\mathrm{Clos}(\mathbf{C}(B))\to B$ form an isomorphism in $\mathbf{Bool}$ . Therefore,

\hom_{\mathbf{Bool}}(B,B)\cong\hom_{\mathbf{Bool}}(B,\mathrm{Clos}(\mathbf{C}(B)))\cong\hom_{\mathbf{augStone}}(\mathbf{C}(B),\mathbf{C}(B)),

where the second isomorphism follows from Proposition 3.2. ∎

Theorem 3.4.

$\mathbf{C}$ is the left adjoint of $\mathrm{Clos}$ .

Proof.

Given $B\in\mathbf{Obj}(\mathbf{Bool})$ and $S\in\mathbf{Obj}(\mathbf{augStone})$ , Propositions 3.1 and 3.2 show that $\alpha_{B,S}\colon\hom_{\mathbf{Bool}}(B,\mathrm{Clos}(S))\to\hom_{\mathbf{augStone}}(\mathbf{C}(B),S)$ and $\beta_{B,S}\colon\hom_{\mathbf{augStone}}(\mathbf{C}(B),S)\to\hom_{\mathbf{Bool}}(B,\mathrm{Clos}(S))$ are inverses. It remains to show this isomorphism is natural in both arguments. Let $\rho\in\hom_{\mathbf{Bool}}(B^{\prime},B)$ and $\sigma\in\hom_{\mathbf{augStone}}(S,S^{\prime})$ . We want to show that the following diagram commutes:

Let $f\in\hom_{\mathbf{Bool}}(B,\mathrm{Clos}(S))$ and $(a^{\prime},g^{\prime})\in\mathbf{C}(B^{\prime})$ . We have

	$\displaystyle\left(\alpha_{B^{\prime},S^{\prime}}(\sigma f\rho)\right)(a^{\prime},g^{\prime})$	$\displaystyle=(\sigma f\rho\pi_{2}\land(\sigma f\rho\pi_{1}\to e_{S^{\prime}}))(a^{\prime},g^{\prime})$
		$\displaystyle=\sigma f\rho(g^{\prime})\land(\sigma f\rho(a^{\prime})\to e_{S^{\prime}})$
		$\displaystyle=\sigma\left(f\rho(g^{\prime})\land(f\rho(a^{\prime})\to e_{S})\right)$
		$\displaystyle=\sigma\left(f\pi_{2}\land(f\pi_{1}\to e_{S})\right)(\rho(a^{\prime}),\rho(g^{\prime}))$
		$\displaystyle=\sigma\alpha_{B,S}(f)\mathbf{C}(\rho)(a^{\prime},g^{\prime}).$

Let $f^{*}\in\hom_{\mathbf{augStone}}(\mathbf{C}(B),S)$ and $b^{\prime}\in B^{\prime}$ . We have

	$\displaystyle\beta_{B^{\prime},S^{\prime}}\left(\sigma f^{*}\mathbf{C}(\rho)\right)(b^{\prime})$	$\displaystyle=\sigma f^{*}\mathbf{C}(\rho)\Delta(b^{\prime})$
		$\displaystyle=\sigma f^{*}(\neg\rho b^{\prime},\rho b^{\prime})$
		$\displaystyle=\sigma f^{*}\Delta(\rho b^{\prime})$
		$\displaystyle=(\sigma\beta_{B,S}(f^{*})\Delta\rho)(b^{\prime}).\qed$

Funding details

This work was supported by NSF and ASEE through an eFellows postdoctoral fellowship.

References

[1] Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.-B., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T. A., and Larsen, K. G. Contracts for system design. Foundations and Trends ${}^{\text{\scriptsize{\textregistered}}}$ in Electronic Design Automation 12, 2-3 (2018), 124–400.
[2] Incer, I. The Algebra of Contracts. PhD thesis, EECS Department, University of California, Berkeley, May 2022.

An Adjunction Between Boolean Algebras and a Subcategory of Stone Algebras

Abstract

1 Introduction

2 Augmented Stone Algebras

Definition 2.1.

Definition 2.2.

Notation 2.3.

Example 2.4.

Proposition 2.5.

Proof.

Proposition 2.6.

Proof.

3 An adjunction between 𝐁𝐨𝐨𝐥\mathbf{Bool} and 𝐚𝐮𝐠𝐒𝐭𝐨𝐧𝐞\mathbf{augStone}

Proposition 3.1.

Proof.

Proposition 3.2.

Proof.

Corollary 3.3.

Proof.

Theorem 3.4.

Proof.

Funding details

References

3 An adjunction between $\mathbf{Bool}$ and $\mathbf{augStone}$