nLab Boolean category




A Boolean category is a coherent category (such as a topos or pretopos) in which every subobject has a complement, i.e., for any monomorphism AXA\hookrightarrow X there is a monomorphism BXB\hookrightarrow X such that ABA\cap B is initial and AB=XA\cup B = X. Therefore, the subobject lattice Sub(X)Sub(X) of any object XX is a Boolean algebra.


Any Boolean category is, in particular, a Heyting category and therefore supports a full first-order internal logic. However, unlike that of an arbitrary Heyting category, the internal logic of a Boolean category satisfies the principle of excluded middle; it is first-order classical logic.

In addition, every Boolean category 𝒞\mathcal{C} is a first order Boolean hyperdoctrine given by the subobject poset functor sub:𝒞 opBoolAlg\mathrm{sub}:\mathcal{C}^{op} \to BoolAlg.

categoryfunctorinternal logictheoryhyperdoctrinesubobject posetcoverageclassifying topos
finitely complete categorycartesian functorcartesian logicessentially algebraic theory
lextensive categorydisjunctive logic
regular categoryregular functorregular logicregular theoryregular hyperdoctrineinfimum-semilatticeregular coverageregular topos
coherent categorycoherent functorcoherent logiccoherent theorycoherent hyperdoctrinedistributive latticecoherent coveragecoherent topos
geometric categorygeometric functorgeometric logicgeometric theorygeometric hyperdoctrineframegeometric coverageGrothendieck topos
Heyting categoryHeyting functorintuitionistic first-order logicintuitionistic first-order theoryfirst-order hyperdoctrineHeyting algebra
De Morgan Heyting categoryintuitionistic first-order logic with weak excluded middleDe Morgan Heyting algebra
Boolean categoryclassical first-order logicclassical first-order theoryBoolean hyperdoctrineBoolean algebra
star-autonomous categorymultiplicative classical linear logic
symmetric monoidal closed categorymultiplicative intuitionistic linear logic
cartesian monoidal categoryfragment {&,}\{\&, \top\} of linear logic
cocartesian monoidal categoryfragment {,0}\{\oplus, 0\} of linear logic
cartesian closed categorysimply typed lambda calculus

Last revised on November 16, 2022 at 19:56:35. See the history of this page for a list of all contributions to it.