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.

  • $\begingroup$ The category of boolean algebras is a full reflective subcategory of the category of Heyting algebras, by a very standard argument. $\endgroup$
    – Zhen Lin
    Commented Aug 1, 2015 at 4:20

2 Answers 2


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.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .