Are there any free or cofree boolean algebras?

A boolean algebra is an algebra with the binary operations $$\wedge$$, $$\vee$$, an unary operation $$\neg$$, and constants $$0$$, and $$1$$, satisfying axioms. A heyting algebra is an algebra with the binary operations $$\wedge$$, $$\vee$$, $$\to$$, and constants $$0$$ and $$1$$ satisfying axioms.

They both form the evident categories, being types of algebras. There is a functor from the category of boolean algebras to the category of heyting algebras, where $$p \to q = \neg p \vee q$$, and all other operations the same.

My question is, taking this as a forgetful functor, which heyting algebras have free or cofree boolean algebras. In general, is there a free or cofree functor from the category of heyting algebras to the category of boolean algebras.

• The category of boolean algebras is a full reflective subcategory of the category of Heyting algebras, by a very standard argument. Commented Aug 1, 2015 at 4:20

I only just saw this question, while hunting for solid evidence that Lawvere ever spoke of "fascist functors" (unable to find anything yet, although Mac Lane in a 1950 paper spoke of "fascist groups", a joke term originally due to Reinhold Baer).

Anyway, to add to Pece's general argument that relative forgetful functors between categories monadic over $$Set$$ possess left adjoints, the forgetful functor from Boolean algebras to Heyting algebras also has a right adjoint. It takes a Heyting algebra $$H$$ to the Boolean algebra consisting of complemented elements in $$H$$. Full details are in the nLab.

As Zhen Lin said in the comments, there is a very general argument that answers your problem.

Denote $\omega$ for the category of finite ordinals with set-functions between them.

Definition 1. A Lawvere theory is a finite-product-preserving bijective-on-objects functor $\ell \colon \omega^\circ \to \mathcal T$.

A morphism $f$ from the Lawvere theory $\ell_1 \colon \omega^\circ \to \mathcal T_1$ to the Lawvere theory $\ell_2 \colon \omega^\circ \to \mathcal T_2$ is a finite-product-preserving functor $f \colon \mathcal T_1 \to \mathcal T_2$ such that $f \circ \ell_1 = \ell_2$.

Definition 2. A model for the Lawvere theory $\ell \colon \omega^\circ \to \mathcal T$ is a finite-product-preserving functor $\mathcal T \to \mathsf{Set}$. Together with natural transformations, models form a category $\operatorname{Mod}(\ell)$.

Now, if $f$ is a morphism from $\ell_1$ to $\ell_2$, one has a restriction functor from the models of $\ell_2$ to the models of $\ell_1$: $$\operatorname{Mod}(\ell_2) \to \operatorname{Mod}(\ell_1), \quad M \mapsto M\circ f$$

Fact. Let $\mathcal A,B$ be small categories with finite products and $j \colon \mathcal A \to \mathcal B$ a functor between them. If $F \colon \mathcal A \to \mathsf{Set}$ is finite-product-preserving, then so is its left kan extension $j_!F \colon \mathcal B \to \mathsf{Set}$.

Hence, the restriction functor described above admits a left adjoint $$\operatorname{Mod}(\ell_1) \to \operatorname{Mod}(\ell_2),\quad M \mapsto f_!M$$

If $\ell_1$ is the Lawvere theory of heyting algebras and $\ell_2$ the one of boolean algebras, there is a (inclusion) morphism $f \colon \ell_1 \to \ell_2$. The restriction functor is just the 'forgetful' functor you described. It then admits a left adjoint, meaning there is a free functor.

Edit. Also, see this section of the nLab page on Lawvere theories.