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$
4
  • $\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$ Feb 6, 2020 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$ Feb 6, 2020 at 23:34
  • $\begingroup$ It is probably described in Goldblatt's Topoi. $\endgroup$
    – Berci
    Feb 6, 2020 at 23:45
  • $\begingroup$ Maybe, but I have looked at bit, and not seen it yet. $\endgroup$ Feb 6, 2020 at 23:52

1 Answer 1

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.

$\endgroup$

You must log in to answer this question.

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