5
$\begingroup$

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.

$\endgroup$
1
  • $\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

2
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

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