Boolean algebra object structure on coproduct of terminal object

Question

I am asking for some clarification on this old question.

The context for my question is a cartesian closed category $ C $ with a binary coproduct and a terminal object $ I $. One of the answers claims that $ B = I + I $ is a "Boolean algebra object in $C$". I am not entirely sure what a boolean algebra object looks like, but I can guess.

We define top and bottom "elements" as the injections $ \iota_0, \iota_1: I \to B $. Also, because this is a distributive category, we define $ \lor, \land, \Rightarrow: B \times B \to B$ using the universal property of the coproduct.

Using the same universal property, we can show that the following diagram commutes (corresponding to $ a \lor a = a $):

However, there is also supposed to be a law corresponding to $ a \land \lnot a = 0 $. I think the diagram is supposed to look like this:

Is this the right diagram for this axiom, and does it indeed commute?

Answer 1

I am not entirely sure what a boolean algebra object

There are many ways to make this precise, but an intuitive one is: you can define an internal lattice in $\cal C$ as an object $L$ equipped with $\land,\lor$, each of which give $L$ the structure of an internal commutative semigroup, every element is idempotent, and the absorption laws are true. All these conditions are equations, you can easily turn them into diagrams to which you will require to commute. The way you phrase the complementation axiom $a\land \lnot a=0$ shows you're very familiar with this translation process. The only little mistake is assuming that $a$ (an "element" of $B$) is an arrow $a : I\to B$. This is false, and in fact a very strong assumption on the ambient category $\cal C$. Instead, the axiom $$ \forall a. a\land \lnot a=0 $$ $\require{AMScd}$translates into the commutativity of $$\begin{CD} B @>\Delta>> B\times B @>1\times\lnot >> B\times B \\ @V!VV @. @V\land VV\\ I @= I@>>in_0> B \end{CD}$$

Now, showing this, and all other properties, is a matter of diagram chasing: by the universal property of coproducts, two maps out of $B=I+I$ coincide if and only if they coincide when precomposed with the coproduct injections $in_0,in_1$.

Answer 2

I am not entirely sure what a boolean algebra object looks like, but I can guess.

The way to remove the guesswork in this case is to get a nice definition of a boolean algebra as an algebraic theory, i.e., a collection of operations on a carrier satisfying a collection of universally quantified equations. For example, the nlab provides a definition with 5 operations and 12 axioms. If you interpret this theory in Set, you get the usual notion of a boolean algebra but an algebraic theory can be interpreted in any cartesian closed category.

The process is mechanical:

1. Provide an object $B$ in $C$ to be the carrier
2. Provide for each operation $o$ of $n$ arguments a morphism $o : C(B^n, B)$
3. For each universally quantified equation $M = N$ with $n$ free variables, you interpret the terms as morphisms $M, N : C(B^n,B)$ and prove they are equal.

For example, your equation $a \wedge \neg a = \bot$ is an equation on one free variable $a$, and so is interpreted as an equation between morphisms $C(B,B)$: $$\wedge \circ (\textrm{id}, \neg) = \bot \circ !$$ where the operations used are

1. $\wedge : C(B^2,B)$
2. $\neg : C(B,B)$
3. $\bot : C(1,B)$

For more