$\newcommand\FinSet{\mathit{FinSet}}\newcommand\FinBool{\mathit{FinBool}}\newcommand\FreeFinBool{\mathit{FreeFinBool}}\newcommand\Set{\mathit{Set}}\newcommand\Psh{\mathit{Psh}}$It's well-known that the topos of presheaves on the category $\FinSet$ of finite sets is the classifying topos for boolean algebra objects.

The argument goes like this: By Stone duality, the functor $n \mapsto 2^n$ is an equivalence of categories $\FinSet \simeq \FinBool^{\text{op}}$, where $\FinBool$ is the category of finite Boolean algebras, which are necessarily projective (so we may use $\FinBool$ and $\FreeFinBool$, which is dual to the category $\FinSet_{2^\bullet}$ of sets with cardinality a finite power of $2$, pretty much interchangeably). Since the theory of Boolean algebras is a finitary algebraic theory, finite-product-preserving functors $\FinBool^{\text{op}} \to \mathcal E$ are identified with Boolean algebra objects in $\mathcal E$, for any category $\mathcal E$ with finite products and split idempotents. If $\mathcal E = \Set$, then any finite-product-preserving functor $\FinBool \to \Set$ is automatically flat; the proof uses the fact that every finitely-presentable Boolean algebra is projective. So a geometric morphism $\Psh(\FinSet_{\neq \emptyset}) \to \Set$ is just a Boolean algebra. Then because $\Psh(\FinSet_{\neq \emptyset})$ is a presheaf topos and the theory of Boolean algebras is algebraic, this classifying topos identification extends to all Grothendieck toposes $\mathcal E$.

But what happens when we perturb the input a bit? For example, what happens when we consider presheaves on the category $\FinSet_\ast$ of finite pointed sets? The category $\FinSet_\ast^{op}$ is the idempotent completion of a Lawvere theory $\mathcal T = \FinSet_{\ast,2^\bullet}$ with half as many operations of each arity as the Lawvere theory for Boolean algebras ($2^{2^n - 1}$ instead of $2^{2^n}$). Indeed, by identifying the basepoint of a finite pointed set with $\top$, we can regard $\mathcal T$ as the Lawvere theory whose $n$-ary operations are all Boolean algebra homomorphisms $f: 2^n \to 2^1$ such that $f(\top,\dotsc,\top) = \top$ — i.e. if all inputs are true, the output must also be true. I believe that $\mathcal T$ is generated by the operations $\top, \wedge, \vee, \to$, but I'm not sure what a complete set of relations would be.

As a Lawvere theory, $\mathcal T$ may be rather messy. But we're considering something more refined: a finite-product-preserving functor $A: \mathcal T \to \Set$ is not automatically flat. Flatness is equivalent to requiring that $A$ is a filtered colimit of finitely-generated free algebras. In particular, every finitely-generated subalgebra of $A$ is a subalgebra of a finitely-generated free algebra. It follows that $A$ will satisfy any universal statement satisfied by all finitely-generated free $\mathcal T$-algebras — not just the algebraic ones. I think (but I'm not certain) that the converse is also true — so that $A$ is flat if and only if it satisfies the universal theory of free $\mathcal T$-algebras.


  1. What is an axiomatization of the algebraic theory of the logical connectives $\top, \wedge, \vee, \to$ (i.e. the algebraic theory of connectives $f$ such that $f(\top, \dotsc, \top) = \top$, i.e. the equational theory of the structures $\{\top,\bot\}^n$, in the language $(\top,\wedge,\vee,\to)$)?

  2. What is an axiomatization of the universal theory of these logical connectives (i.e.— I think — the theory classified by the presheaf topos $\Psh(\FinSet_\ast)$, i.e. the universal theory of the structures $\{\top,\bot\}^n$, in the language $(\top,\wedge,\vee,\to)$)?

  3. How do these theories compare to the theory of Boolean algebras — what are some examples of algebras or algebra homomomorphisms which don't come from Boolean algebras or homomorphisms thereof? Is there a form of Stone duality for these algebras, and how do the corresponding spaces compare to Stone spaces?

More fundamental than the presheaf toposes $\Psh(\FinSet)$ and $\Psh(\FinSet_\ast)$ are the presheaf toposes $\Psh(\FinSet^{\text{op}})$ and $\Psh(\FinSet_\ast^{\text{op}})$ which classify objects and pointed objects respectively. Unfortunately, these facts don't seem to shed much light on the less fundamental toposes I'm interested in here. For instance, it doesn't seem to be the case that the tensor product of the Lawvere theories $\FinSet^{\text{op}}_\ast$ and $\FinSet$ is $\FinSet_\ast$ — I believe that tensor product is just the terminal Lawvere theory (note that the "op"'s for the Lawvere theories are reversed from the "op"'s for the presheaf categories).

The operations $(\top,\wedge,\vee,\to)$ being considered here are almost the same as the operations of a Heyting algebra — the difference being that a Heyting algebra has a constant $\bot$ as well. So, based on the axioms for a Heyting algebra, here are some guesses:

Guess for (1): The following algebraic axioms, which are satisfied (thanks to Andreas Blass for catching a mistake in the comments below!), might be a complete set of algebraic axioms:

  • $(\top,\wedge,\vee)$ form an upper-bounded distributive lattice;

  • $x \to x = \top$;

  • $x \wedge (x \to y) = x \wedge y$; $y \wedge (x \to y) = y$;

  • $x \to (y \wedge z) = (x \to y) \wedge (x \to z)$;

  • $(x \vee y) \to z = (x \to z) \wedge (y \to z)$.

As pointed out by მამუკა ჯიბლაძე in the comments below, we also need the following axiom which goes beyond the Heyting axioms, and is equivalent to the interval $[y,\top]$ being a Boolean algebra with $(-) \to y$ for negation:

  • $x \vee (x \to y) = \top$
  • 2
    $\begingroup$ I would have an answer ready but became confused by your $\mathrm{FinSet}_{2^\bullet}$. Conventional duality goes between just $\mathrm{FinSet}$ and $\mathrm{FinBool}$, through the powerset functor and the atoms functor. Through this duality $\mathrm{FinSet}_*$ is dual to the slice $\mathrm{FinBool}/2$, so I would guess the theory classifies Boolean-algebras-with-an-ultrafilter, or dually pointed Stone spaces. More precisely, this would be the category of points of the classifying topos. $\endgroup$ – მამუკა ჯიბლაძე Jan 26 at 5:57
  • 2
    $\begingroup$ I believe it classifies what I said: either Boolean algebras equipped with a homomorphism to the 2-element Boolean algebra, or, dually, pointed Stone locales. $\endgroup$ – მამუკა ჯიბლაძე Jan 26 at 8:03
  • 2
    $\begingroup$ I also do not see it. What might help is that actually $\mathrm{FinSet}_*$ is monadic over $\mathrm{FinSet}$. Also, the fact is that $\mathrm{FinSet}_*$ does contain a Boolean lattice $B:=\{\text{basepoint},\text{nonbasepoint}\}$ such that any Cartesian functor is uniquely determined by its value on it. This is not a Boolean algebra since negation is not ours, but nevertheless it is a distributive lattice with every element complemented, so the same will hold for any model of the corresponding Cartesian theory. $\endgroup$ – მამუკა ჯიბლაძე Jan 26 at 14:20
  • 2
    $\begingroup$ Accordingly, for your axioms you need to add that for any $b$ the interval $[b,\top]$ is a Boolean algebra. This amounts to $a\lor a\to b=\top$. Note that any filter in any Boolean algebra is a model. Conversely, for any model $M$ one gets a Boolean algebra $M\times M^\circ$ in which $M$ is an ultrafilter. $\endgroup$ – მამუკა ჯიბლაძე Jan 26 at 14:31
  • 2
    $\begingroup$ I believe I've seen a duality for these somewhere. Duals are locally compact zero-dimensional locales, and from this point of view it is more convenient to consider Boolean algebras without top rather than without bottom (clopens of a locally compact form such a thing). Passing from $M$ to $M\times M^\circ$ corresponds to the one-point compactification. Conversely, from pointed Stone spaces to locally compact zero-dimensionals one passes just by removing the basepoint. $\endgroup$ – მამუკა ჯიბლაძე Jan 26 at 14:37

I might be missing something, but I think you are overcomplicating things.

I clain that your topos classifies the theory $T$ of pairs $(B,\phi)$ where $B$ is a boolean algebra and $\phi : B \to \{0,1\}$ is a boolean algebra morphism.

Indeed, this theory is given by a finite limit sketch, so it is classified by the the category of presheaf on the opposite of the category of finitely presented $T$-models.

A $T$-model $(B,\phi)$ is finitely presented exactly when the boolean algebra $B$ is finite, hence the category of finitely presented $T$-model is equivalent to $FinSet_*$ by the duality between finite boolean algebra and finite sets.

The theory you describe in your "Guess" is an attempt at axiomatizing the properties fiber $\phi^{-1}(1)$ as an Heyting algebra. This is definitely possible as the negation induce a bijection between the two fiber $\phi^{-1}(0)$ and $\phi^{-1}(1)$ so you can reconstruct $B$ out of one of the fibers and you can express the fact that $B$ is a boolean algbera over $\{0,1\}$ in terms of these fibers.

  • $\begingroup$ Thanks! How does one axiomatize $T$ as a finite-limit sketch? In general, I know how to axiomatize coslice categories, but not slice categories. If we have a sort for $B$ and a sort $\Omega$ for $\{0,1\}$ and a morphism $\phi: B \to \Omega$, then we need axioms for $B$ and $\Omega$ to be Boolean algebras and $\phi$ to be a homomorphism, but we also need an axiom like $\forall x : \Omega (x = \top \vee x = \bot)$ and an axiom like $\bot \neq \top : \Omega$. If we don't have a sort for $\{0,1\}$ and instead add sorts for $\phi^{-1}(0)$ and $\phi^{-1}(1)$ we run into similar problems... $\endgroup$ – Tim Campion Jan 26 at 16:24
  • $\begingroup$ I mostly meant that the category of model is locally finitely presentable, so you know it is the category of models of a finite limite sketch. If you want an explicit axiomatization, you indeed need to take two basic type corresponding to the fiber. I agree it does not work with a sort corresponding to $\Omega$, but I don't see any problem when you use sort for the two fibers. $\endgroup$ – Simon Henry Jan 26 at 16:28
  • 1
    $\begingroup$ Isn't this the same thing as a not necessarily unital boolean ring? $\endgroup$ – Benjamin Steinberg Jan 26 at 16:39
  • 2
    $\begingroup$ If you have a nonunital boolean ring $R$ you can adjoin an identity to get a unital boolean ring $B$ with $R$ as an ideal in $B$ and $B/R$ isomorphic to $\{0,1\}$ and conversely, the kernel of a unital boolean ring homomorphism is a boolean ring (without unit potentially). So they are the same thing. My question was rhetorical. $\endgroup$ – Benjamin Steinberg Jan 26 at 16:47
  • 2
    $\begingroup$ @TimCampion : What you need is two sort for $\phi^{-1}(0)$ and $\phi^{-1}(1)$ and no sort for B itself. As soon as a you put a sort of B you need to use stronger logic to express that B is the union of the two fibers. But of course you can axiomatize everything in terms of only one of the fiber as they are isomorphic. $\endgroup$ – Simon Henry Jan 26 at 17:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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