7
$\begingroup$

Let $\mathcal{E}$ be an elementary topos. I know that the subobject classifier $\Omega$ of the topos is always a Heyting algebra.

I’m interested in versions of the converse — given any (let's say finite) Heyting algebra $L$, can one construct a topos $\mathcal{E}_L$ for which it serves as a subobject classifier? What are the details of this construction, if it can exist?

$\endgroup$
3
  • 1
    $\begingroup$ Minor nitpick, but "does not have to be elementary, though this would be nice" is kind of a funny thing to say, because elemenary toposes are the most general kind. $\endgroup$
    – N. Virgo
    Commented Jul 6 at 9:37
  • $\begingroup$ @N.Virgo That's true, I will edit the question accordingly in case it confuses anybody. Thanks for the catch! $\endgroup$
    – safsom
    Commented Jul 6 at 9:38
  • $\begingroup$ Do you mean for the global sections of $\Omega$ to be isomorphic to $L$, i.e. $\Omega(1) \simeq L$? $\endgroup$
    – Daniel Schepler
    Commented Jul 12 at 15:33

2 Answers 2

Reset to default
5
$\begingroup$

So I haven't actually checked this but I believe it should be true that if $L$ has small joins, or equivalently is a frame, then it is the (Heyting algebra of points of the) subobject classifier of the topos of sheaves on the locale $\text{Spec } L$. This is even some kind of left adjoint, I think. So this is a pretty natural class of examples.

$\endgroup$
5
  • $\begingroup$ Also I think every finite Heyting algebra is a frame, and if so this answers the question for finite Heyting algebras. I was very confused by the other answer claiming this is an open problem but I guess it's not clear what happens for an infinite Heyting algebra which is not a frame. $\endgroup$
    – Qiaochu Yuan
    Commented Jul 6 at 19:53
  • 2
    $\begingroup$ Your thinking is correct: every finite distributive lattice is a frame (the required joins are finute), and every finite distributive lattice is the reduct of a unique finite Heyting algebra. So every finite HA is the subobject classifier of some topos. But this doesn't help in the general case: infinite incomplete Heyting algebras are notoriously poorly understood in most ways. $\endgroup$
    – Z. A. K.
    Commented Jul 7 at 2:00
  • $\begingroup$ I don't think you even need $\operatorname{Spec} L$, assuming by that you mean some set of ideals of $L$. $L$ itself should already be a locale; and a subobject $U$ of $1 \in \operatorname{Sh}(L)$ will easily be seen to be $\{ x\in L \mid x \le \bigvee U \}$. So, it is then easy to check that $x \mapsto \{ y\in L \mid y \le x \}$ is an isomorphism of Heyting algebras $L \to \operatorname{Sub}_{\operatorname{Sh}(L)}(1)$ with inverse $\bigvee$. $\endgroup$
    – Daniel Schepler
    Commented Jul 12 at 16:48
  • $\begingroup$ @Daniel: by $\text{Spec } L$ I just mean $L$ viewed as an object in $\text{Loc} = \text{Frm}^{op}$, by analogy with writing $\text{Spec } A$ for $A$ a commutative ring to mean $A$ viewed as an object in $\text{Aff} = \text{CRing}^{op}$. $\endgroup$
    – Qiaochu Yuan
    Commented Jul 12 at 18:00
  • $\begingroup$ Oh, OK. It might also be worth noting that something equivalent to $\operatorname{Sh}(L)$ can be constructed as "$L$-valued sets" via the tripos-to-topos construction outlined in math.stackexchange.com/a/4506174/337888 . Essentially, an object is a set $X$ equipped with an $L$-valued partial equivalence relation $X\times X \to L$, and the morphisms $X\to Y$ are $L$-valued relations $X\times Y\to L$ satisfying the necessary conditions to represent a respectful function $X / {\sim}_X \to Y / {\sim}_Y$. $\endgroup$
    – Daniel Schepler
    Commented Jul 12 at 18:45
5
$\begingroup$

I believe the general problem (i.e. in the non-finite case) is still an open problem. In Pitts' 1992 On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic, it is written:

The results presented in this paper have had a rather long gestation period. Some ten or so years ago I tried to prove the negation of Theorem 1 in connection with the higher order analogue of Proposition 18- the question of whether any Heyting algebra can appear as the algebra of truth-values of an elementary topos. [...] It remains an open question whether every Heyting algebra can be the Lindenbaum algebra of a theory in intuitionistic higher order logic.

Some special cases are known. For instance, it is known (e.g. p. 332 of Johnstone's 1977 Topos theory) that the statement is true for every Boolean algebra (the construction therein is attributed to Freyd).

Recently, Kuznetsov gave a talk entitled On Boolean Topos Constructions by Freyd and Pataraia and their generalizations at TACL 2024, proposing a generalisation of this result, but suggesting the general problem is still open.

$\endgroup$
4
  • $\begingroup$ Am I misunderstanding the first paragraph on the second page of Kuznetsov's report that you linked? It seems to say that unpublished work of Pataraia solved the problem for general Heyting algebras. $\endgroup$
    – Andreas Blass
    Commented Jul 6 at 13:10
  • $\begingroup$ @AndreasBlass: oh, so it does... I can't find any other reference to The high order cylindric algebras and topoi. I wonder if it is possible to find any notes on the talk. It seems odd that Kuznetsov is talking about a special case of the problem if Pataraia already solved the general case. $\endgroup$
    – varkor
    Commented Jul 6 at 14:13
  • $\begingroup$ I found a talk abstract claiming Pataraia had a general construction, but this appears to be the only information that can be found online. $\endgroup$
    – varkor
    Commented Jul 6 at 14:31
  • 1
    $\begingroup$ This has been asked before in MO. From what I've heard, Pataraia had a construction which claimed to solve the problem, but this was never published, and he sadly passed away without it being possible for anyone to fully verify it. Johnstone presented part of those ideas here see also. Jibladze, Kuznetsov and Streicher have been actively working on the problem. $\endgroup$
    – Rodrigo Nicolau Almeida
    Commented Jul 12 at 7:59

You must log in to answer this question.

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