Let $\mathcal C$ be a cartesian category with a subobject classifier $\Omega$.
(i) For every object A of $\mathcal C$, the preorder $\text{Sub}(A)$ is cartesian closed; and in fact $\Omega$ has the structure of an internal Heyting semilattice in $\mathcal C$.
(ii) If $\mathcal C$ has finite unions of subobjects which are stable under pullback, then $\Omega$ is an internal Heyting algebra in $\mathcal C$.
I would like to understand better what this means.
My understanding of "internal stuff" has always been: "if you know how to write a definition (or theory) down as diagrams, put those diagrams in the category you say has that internal thing".
I don't think this is how Johnstone is thinking about it.
Q. 1: Is there a better way to do so?
Otherwise; any recommendations on how to think of internal Heyting algebras/semilattices in particular?
Q. 2: I assume that Heyting semilattice means cartesian closed poset. (As opposed to bicartesian closed poset in the case of a Heyting algebra.)
Q. 3: More generally do you have any recommendations on how to think of this statement?
The proof (what I've seen thus far) makes sense. But then I'm not sure I'll be able to see how it is a proof of the statement.
A reference to a more friendly proof of this lemma is also welcome.
Thanks in advance!
Best Answer
To answer question 1: The category of Heyting algebras is canonically equivalent to a variety of algebras. The signature of this variety would be nullary operations $\bot, \top$ and binary operations $\wedge, \vee, \rightarrow$. The equational identities would be the combination of the usual equational identities defining a bound lattice (i.e. idempotence, commutativity, associativity of $\wedge$ and $\vee$, the absorption laws, etc.) with these identities for $\rightarrow$: $$(x \rightarrow x) = \top\\ x \wedge (x \rightarrow y) = x \wedge y\\ y \wedge (x \rightarrow y) = y \\ (x \rightarrow (y \wedge z)) = (x \rightarrow y) \wedge (x \rightarrow z).$$ From here, it would be straightforward to write out the appropriate commutative diagrams in the definition of an internal Heyting algebra object of a category with finite limits. Similarly, I would presume a Heyting semilattice would be the restriction to the signature of $\top, \wedge, \rightarrow$ and the identities only involving those operations, leading to a similar definition of an internal Heyting semilattice object.
As for the basic idea behind the proof, let us look at the situation in the first part. Here, obviously each subobject poset of an object $X$ has a top object $\operatorname{id}_X : X \to X$; and using pullbacks, this subobject poset also has meets (intersections). Now, to move towards the definition of a relative complement object, let us first note that for $f, g : X \to Y$ and $C$ a subobject of $X$, we have $C$ is contained in the equalizer of $f$ and $g$ if and only if $f \circ \operatorname{inc}_C = g \circ \operatorname{inc}_C$. Now, let us see what happens if we apply this in the special case that $f$ and $g$ are the characteristic maps of subobjects $A$ and $B$. We get that $C \subseteq \operatorname{eq}(\chi_A, \chi_B)$ if and only if $\chi_A \circ \operatorname{inc}_C = \chi_B \circ \operatorname{inc}_C$. However, by the naturality of the isomorphism $\operatorname{Hom}({-}, \Omega) \simeq \operatorname{Sub}$, we see that $\chi_A \circ \operatorname{inc}_C$ is the characteristic function of $A \cap C$ as a subobject of $C$; and likewise, $\chi_B \circ \operatorname{inc}_C$ is the characteristic function of $B \cap C$. Therefore, $C \subseteq \operatorname{eq}(\chi_A, \chi_B)$ if and only if $A \cap C = B \cap C$. As a corollary of this, we see that $C \cap A \subseteq B$ if and only if $C \cap A = C \cap A \cap B$, if and only if $C \subseteq \operatorname{eq}(\chi_A, \chi_{A\cap B})$. Thus, the subobject poset is indeed a Heyting semilattice with relative complement operation defined by $(A \Rightarrow B) := \operatorname{eq}(\chi_A, \chi_{A\cap B})$.
Furthermore, it is easy to see that top object, intersections, and this relative complement operation respect pullbacks $f^* : \operatorname{Sub}(Y) \to \operatorname{Sub}(X)$, so each $f^*$ is a morphism of Heyting semilattices. From this, you can define a structure of internal Heyting semilattice on $\Omega$: for example, the internal relative complement operation $\Omega \times \Omega \to \Omega$ is constructed via the Yoneda lemma from the morphism of functors $\operatorname{Sub}({-}) \times \operatorname{Sub}({-}) \to \operatorname{Sub}({-}), (A, B) \mapsto (A \Rightarrow B)$, where the domain is isomorphic to the functor $\operatorname{Hom}({-}, \Omega \times \Omega)$ and the codomain is isomorphic to $\operatorname{Hom}({-}, \Omega)$.
The second part is very similar: By assumption each subobject posets also has a bottom object (a union of an empty family) and joins (binary unions), so this preorder is in fact a Heyting algebra. Furthermore, by assumption, each pullback $f^* : \operatorname{Sub}(Y) \to \operatorname{Sub}(X)$ also preserves bottom and joins, so it is a morphism of Heyting algebras. By a similar argument, then, this induces a structure of internal Heyting algebra on $\Omega$.
So, as a possible answer to question 3: In this case at least, it is useful to think of an internal Heyting algebra structure on an object $X$ as being equivalent to an "enrichment" of the functor $\operatorname{Hom}({-}, X) : \mathcal{C}^{\operatorname{op}} \to \mathsf{Set}$ to a functor $\mathcal{C}^{\operatorname{op}} \to \mathsf{HeytAlg}$.