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 fascist 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. – Zhen Lin Aug 1 '15 at 4:20
  • Facist functor has no mathematical meaning. – marshal craft Aug 1 '15 at 4:38
  • 2
    @marshalcraft Yes it does. It is dual to free functor. Follow the link to see the origin of the term. – PyRulez Aug 1 '15 at 4:52
  • I did, I understand it is a joke. Mine was also. – marshal craft Aug 1 '15 at 4:57
  • 2
    @marshalcraft Actually, it does! Because of French people... 'Fascism' actually came from the romanian fasces, which was the symbol of the italian facist political group. In french, fasces are called "faisceaux" (which roughly means a bunch of line-shaped things glued together). So "fasciste", the french word for 'fascist', is the adjective reffering to "faisceaux". But "faisceau" is also the french word for a sheaf: so a fascist functor just is sheafy functor (i.e. a sheaf) ! [...] – Pece Aug 1 '15 at 7:17

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.

Your Answer


By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.