Boolean structures: from 2 to predicates to subsets, and back

Background: $\Newextarrow{\xleftrightarrow}{10,10}{0x2194}$
For the predicate/subset bijection, and the nullary and unary logical operations on $\bftwo$, see “$\bftwo$ as the Boolean subobject classifier”.
For the binary logical operations on $\bftwo$ (“the Boolean logical connectives”), see “Elementary Boolean geometry and logic”.

---

Inputs:
Inputs are two predicate/subset pairs, $\objA$ and $\objB$, on a given set $\setX\in\Set$, as shown below, embedded as the right squares in $2 \times 3$ diagrams.
Also shown are two noteworthy special cases, which will be used in the sequel.

$\begin{array}{} \objA\times\objX & \xrightarrow{} & \objA & \xrightarrow{} & \bfone \\ \llap{i_\objA \times\objX} \downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \llap{i_\objA} \downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \downarrow\rlap\radjtop \\ \objX\times\objX & \xrightarrow[\textstyle \pi_1]{} & \objX & \xrightarrow[\textstyle \objA]{} & \bftwo \\ \end{array}$

$\begin{array}{} \objX\times\objB & \xrightarrow{} & \objB & \xrightarrow{} & \bfone \\ \llap{\objX \times i_\objB} \downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \llap{i_\objB} \downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \downarrow\rlap\radjtop \\ \objX\times\objX & \xrightarrow[\textstyle \pi_2]{} & \objX & \xrightarrow[\textstyle \objB]{} & \bftwo \\ \end{array}$

$\begin{array}{} \radjtop\times\bftwo & \xrightarrow{} & \bfone \\ \llap{\radjtop\times\bftwo} \downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \downarrow\rlap\radjtop \\ \bftwo\times\bftwo & \xrightarrow[\textstyle \pi_1]{} & \bftwo \\ \end{array}$

$\begin{array}{} \bftwo\times\radjtop & \xrightarrow{} & \bfone \\ \llap{\bftwo\times\radjtop} \downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \downarrow\rlap\radjtop \\ \bftwo\times\bftwo & \xrightarrow[\textstyle \pi_2]{} & \bftwo \\ \end{array}$

---

Internal:

(Intersection of subsets) and (conjunction of predicates)
(the internal operations in $\Set$) $$\begin{array}{} &&& \eltx \in (\setA\cap\setB) & \xleftrightarrow{} & {\eltx\in\setA} \wedge {\eltx\in\setB} \\ \\ \begin{array}{l} \text{Intersection}\\ \text{of subsets}\\ \text{(internal)}\\ \end{array} &&& \boxed{\begin{array}{} \\ \setA \cap \setB\\ \\ \{ \eltx\in\setX \mid {{\eltx\in\setA} \wedge {\eltx\in\setB} \} }\\ \end{array} } & \longrightarrow & \boxed{ \begin{array}{} \pi_1^{-1}\objA \cap \pi_2^{-1}\objB \\ \setA\times\setX \cap \setX\times\setB\\ \setA \times \setB\\ \{ \langle\eltx,\elty\rangle \in \setX\times\setX \mid {{\eltx\in\setA} \wedge {\elty\in\setB} \} }\\ \end{array} } & \xrightarrow[]{} & \boxed { \begin{array}{} \pi_1^{-1}\radjtop \cap \pi_2^{-1}\radjtop \\ {\radjtop\times\bftwo} \cap {\bftwo\times\radjtop} \\ \radjtop\times\radjtop \\ \{ \langle \radjtop, \radjtop \rangle \} \\ \end{array} } & \xrightarrow[]{} & \bfone \\ &&& \Big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow\rlap\radjtop \\ & \eltx & \in & \setX & \xrightarrow[\textstyle \Delta]{} & \setX \times \setX & \xrightarrow[\textstyle \setA\times\setB]{} & \bftwo \times \bftwo & \xrightarrow[\textstyle \boxed{ \begin{array}{}\wedge\\ \pi_1\wedge\pi_2\\ \end{array} } ]{} & \bftwo & \ni & {{\setA_\eltx} \wedge {\setB_\eltx}} \\ &&& \Vert &&&& \Vert \\ &&& \setX && \xrightarrow[\textstyle \langle\functionA,\functionB\rangle]{} && \bftwo \times \bftwo \\ \begin{array}{l} \text{Conjunction}\\ \text{of predicates}\\ \text{(internal)}\\ \end{array} & \Bigg\Vert && \Bigg\Vert &&&&&& \Bigg\Vert && \Bigg\Vert \\ & \eltx & \in & \setX &&& \xrightarrow[\textstyle \; \boxed{\setA\wedge\setB} \; ]{} &&& \bftwo & \ni & {(\setA\wedge\setB)_\eltx} \\ \end{array}$$

---

External plus internal:

(Intersection of subsets) and (conjunction of predicates)
(the external operations on $\Set$, plus projections/evaluations to the internal Boolean algebra $\bftwo$) $$\begin{array}{lcccccccccccc} \text{Intersection of subsets (external)} && \langle\setA,\setB\rangle & \in & \Sub(\setX) \times \Sub(\setX) && \xrightarrow{\textstyle \boxed\cap} && \Sub(\setX) & \ni & \setA\cap\setB \\ && \wr && \Vert\wr &&&& \Vert\wr && \wr \\ && \langle\functionA,\functionB\rangle & \in & \hom \setX \Set \bftwo \times \hom \setX \Set \bftwo & \xrightarrow[\textstyle \times]{} & \hom {\setX\times\setX} \Set {\bftwo\times\bftwo} & \xrightarrow[\textstyle \hom \Delta \Set \wedge]{} & \hom \setX \Set \bftwo & \ni & \functionA \wedge \functionB \\ \text{Conjunction of predicates (external)} && \Vert && \Vert &&&& \Vert && \Vert \\ && \langle\functionA,\functionB\rangle & \in & \hom \setX \Set \bftwo \times \hom \setX \Set \bftwo && \xrightarrow[\textstyle \boxed\wedge]{} && \hom \setX \Set \bftwo & \ni & \functionA \wedge \functionB \\ && \mapsdownto && \Big\downarrow \rlap{\mkern-2.1em E_\eltx\times E_\eltx} &&&& \Big\downarrow \rlap{E_\eltx} && \mapsdownto \\ \text{Conjunction in $\bftwo$ (internal)} && \langle \functionA_\eltx,\functionB_\eltx \rangle & \in & \bftwo\times\bftwo && \xrightarrow[\textstyle \boxed\wedge]{} && \bftwo & \ni & \functionA_\eltx \wedge \functionB_\eltx \\ \end{array}$$

---

The above shows how, given a function in $\Set$ from $\bftwo\times\bftwo$ to $\bftwo$ (an internal binary operation on $\bftwo$),
that function generates binary operations on $\hom \objX \Set \bftwo$ and $\Sub(X)$, for arbitrary sets $\objX\in\Set$ (which in fact are natural with respect to $\setX\in\Set\op$),
a process we call extension.
The process may be reversed.
First, binary operations on $\hom \objX \Set \bftwo$ and $\Sub(X)$ are in bijection, using the predicate/subset bijection.
Second, any binary operation on $\hom \objX \Set \bftwo$ yields a binary operation on $\bftwo$,
by applying the operation to the specific predicates $\pi_1, \pi_2 : \bftwo\times\bftwo \to \bftwo$, a process we call restriction.
If we restrict to binary operations on $\hom \objX \Set \bftwo$ and $\Sub(X)$ which satisfy the categorical condition of naturality,
then these two processes are inverse to each other.
For example, evaluating (the construction of conjunction for predicates) on (the specific predicates $\pi_1, \pi_2 : \bftwo\times\bftwo \to \bftwo$), we have: $$\begin{array}{} \objA,\objB & \xmapsto{} & \objA,\objB,\objA,\objB & \xmapsto{} & \objA,\objB & \xmapsto{} & \objA\wedge\objB \\ \bftwo\times\bftwo && \xrightarrow{\textstyle \text{identity}} && \bftwo\times\bftwo \\ \Vert &&&& \Vert \\ \bftwo\times\bftwo & \xrightarrow[\textstyle \Delta]{} & \bftwo\times\bftwo\times\bftwo\times\bftwo & \xrightarrow[\textstyle \pi_1 \times \pi_2]{} & \bftwo\times\bftwo & \xrightarrow[\textstyle \wedge]{} & \bftwo \\ \Vert &&&&&& \Vert \\ \bftwo\times\bftwo &&& \xrightarrow[\textstyle \pi_1\wedge\pi_2]{} &&& \bftwo\times\bftwo \\ \end{array}$$ thus $\boxed{\pi_1\wedge\pi_2 = \wedge}$, thus extension followed by restricting gives the original function.
To prove the other direction, that first restricting, then extending, gives the original, is more complex.
A proof of that, in greater generality, is at my discussion of the identities-are-free (Yoneda) lemma.

---

Pullback preserves the Boolean structure,
e.g., given a function in $\Set$, $\functionf:\setX\to\setY$,
completing the diagram at left below in either of the two evident ways yields isomorphic results

$\begin{array}{} & \rightarrow & \functionf^{-1}\objBp \\ & \searrow && \searrow \\ && \functionf^{-1}\objB & \rightarrow & \objX\\ \\ & \objB\cap\objBp & \rightarrow & \objBp\\ && \searrow && \searrow & \Bigg\downarrow\rlap\functionf \\ &&& \objB & \rightarrow & \objY \\ \end{array} \mkern1em$ for we have $\mkern1em \begin{array}{} \eltx \in (\functionf^{-1}\objB \cap \functionf^{-1}\objB') & \xleftrightarrow{\textstyle \cap} & \eltx\in\functionf^{-1}\objB \wedge \eltx\in\functionf^{-1}\objB' \\ \\ \eltx\in\functionf^{-1}(\objB\cap\objB') && \updownarrow \rlap{\functionf^{-1}} \\ \llap{\functionf^{-1}} \updownarrow \\ \eltx\functionf \in \objB\cap\objB' & \xleftrightarrow[\textstyle \cap]{} & \eltx\functionf\in\objB \wedge \eltx\functionf \in \objB' \\ \end{array} \mkern1em$ or $\mkern1em \begin{array}{} (\functionf^{-1}\objB \wedge \functionf^{-1}\objB')_\eltx & \xlongequal{\textstyle \wedge} & (\functionf^{-1}\objB)_\eltx \wedge (\functionf^{-1}\objB')_\eltx \\ \\ \big(\functionf^{-1}(\objB\wedge\objB')\big)_\eltx && \Vert \rlap{\;\functionf^{-1}} \\ \llap{\functionf^{-1}} \Vert \\ (\objB\wedge\objB')_{\eltx\functionf} & \xlongequal[\textstyle \wedge]{} & \objB_{\eltx\functionf} \wedge {\objB'}_{\eltx\functionf} \\ \end{array}$.

---

Moving up several levels of generality and abstraction, there are the following bijections
(in the three examples of natural transformations, we show their components at $\setX\in\Set\op$):

Description		Bijections		Example
Internal subsets of $\bftwo\times\bftwo$		$\Sub(\bftwo\times\bftwo)$		$\{\langle \radjtop,\radjtop \rangle\} \subset \bftwo\times\bftwo$
predicate/subset bijection		$\Vert\wr$		$\wr$
Internal predicates on $\bftwo\times\bftwo$		$\hom {\bftwo\times\bftwo} \Set \bftwo$		$\bftwo\times\bftwo \xrightarrow{\textstyle\wedge} \bftwo$
Yoneda bijection		$\Vert\wr$		$\wr$
Natural transformations between indicated functors		$\hom {\hom - \Set {\bftwo\times\bftwo}} {[\Set\op,\Set]} {\hom - \Set \bftwo}$		$\hom \setX \Set {\bftwo\times\bftwo} \xrightarrow{\textstyle \hom \setX \Set \wedge} \hom \setX \Set \bftwo$
defn. of internal product in $\Set$		$\Vert\wr$		$\wr$
External operations on predicates		$\hom {{\hom - \Set \bftwo} \times {\hom - \Set \bftwo}} {[\Set\op,\Set]} {\hom - \Set \bftwo}$		${\hom \setX \Set \bftwo} \times {\hom \setX \Set \bftwo} \xrightarrow{\textstyle \wedge} {\hom \setX \Set \bftwo}$
predicate/subset bijection		$\Vert\wr$		$\wr$
External operations on subsets		$\hom {\Sub \times \Sub} {[\Set\op,\Set]} \Sub$		${\Sub(\setX)} \times {\Sub(\setX)} \xrightarrow{\textstyle\cap} {\Sub(\setX)}$