2
$\begingroup$

Below I describe an internal intersection arrow in a topos. My main question is, is there a corresponding idea of an internal union arrow, and if so what is the definition of it ?

Pointers to literature would also be helpful. I did see that

https://ncatlab.org/toddtrimble/published/An+elementary+approach+to+elementary+topos+theory

refers to an internal join arrow (which is probably what I want), but Todd Trimble does not seem to elaborate about it.

I learnt about internal intersection arrows from Exercise 13.9 of Elementary Categories, Elementary Toposes (by Colin Mclarty), but I am also unsure of their exact nature. I paraphrase this exercise below, in the hope that somebody can tell me exactly how internal intersection arrows are defined too (feel free to use the Mitchell–Bénabou language if it helps):

For an object $A,$ in a topos with subobject classifier $\Omega,$ we write $x \in^A p$ to denote that that pair $\langle p,x \rangle$ is a member of the subobject classified by the exponential evaluation arrow $\Omega ^A \times A\overset{e}{\rightarrow} \Omega.$ Mclarty asks us to define an internal intersection arrow

$$ \Omega ^{\Omega ^A} \overset{\cap}{\rightarrow} \Omega ^A $$

and he tells us that $\cap$ is the exponential transpose of the arrow

$$ \Omega ^{\Omega ^A} \times A \overset{}{\rightarrow} \Omega$$

which takes a pair $\langle s, x \rangle$ to true if and only if for every

$$p \in^{\Omega ^A} s$$

we have $x \in^A p.$

$\endgroup$
  • $\begingroup$ If you're comfortable with the Mitchell-Benabou language, then I'm not sure what more there is to do; it's just defined in the internal language like it would be set-theoretically. So I'm guessing you'd actually prefer a pure arrows version? $\endgroup$ – Malice Vidrine Feb 6 at 23:01
  • $\begingroup$ I think I've used the Mitchell-Benabou language to get at the internal intersection arrow, but I'm not sure, so I would appreciate seeing a pure arrow version. But the main thing I'm hoping for is some sort of description of the internal union arrow. $\endgroup$ – Richard Southwell Feb 6 at 23:34
  • $\begingroup$ It is probably described in Goldblatt's Topoi. $\endgroup$ – Berci Feb 6 at 23:45
  • $\begingroup$ Maybe, but I have looked at bit, and not seen it yet. $\endgroup$ – Richard Southwell Feb 6 at 23:52
3
$\begingroup$

There is, indeed, a union arrow, and it is more or less what you might expect.

For an object $A$, we can form the subobject $$\pi_{1,2}^*(\in^{\Omega^A})\wedge\pi_{2,3}^*(\in^{A})\hookrightarrow\Omega^{\Omega^A}\times\Omega^A\times A\qquad (1)$$ by taking the meet of the subobjects obtained by pulling back $\in^{\Omega^A}$ and $\in^A$ along the relevant product projections. Then $$\exists_{\pi_{1,3}}(\pi_{1,2}^*(\in^{\Omega^A})\wedge\pi_{2,3}^*(\in^{A}))\hookrightarrow\Omega^{\Omega^A}\times A\qquad (2)$$ is the image of the composition of the inclusion in (1) with the projection $\pi_{1,3}:\Omega^{\Omega^A}\times\Omega^A\times A\to\Omega^{\Omega^A}\times A$. Intuitively, (2) is the extension of the predicate $\exists P(a\in P\wedge P\in X)$; i.e. all the $\langle a,X\rangle$ in the image of the map that deletes the middle term from $\langle a,P,X\rangle$ with $a\in P\in X$.

The subobject in (2) has a classifying map; call it $U:\Omega^{\Omega^A}\times A\to \Omega$. Then, as with the intersection map, the union map $\bigvee:\Omega^{\Omega^A}\to\Omega^A$ is obtained by taking the exponential transpose of $U$.

The only difference between this map and the intersection map is whether you're using the left or right adjoint to $\pi_{1,3}^*:\mathrm{Sub}(\Omega^{\Omega^A}\times A)\to\mathrm{Sub}(\Omega^{\Omega^A}\times\Omega^A\times A)$ in going from (1) to (2); they each give a different subobject of $\Omega^{\Omega^A}\times A$, and so a different classifying arrow to take the transpose of in the last step.

Hopefully this makes the construction a little clearer.

| cite | improve this answer | |
$\endgroup$

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.