# topos have colimits

Define an (elementary) topos to be a cartesian closed category with all finite limits and subobject classifiers. I'm looking for a proof of the fact that a topos also has all finite colimits.

I know that there is a proof by Paré using monad theory; but I do not know yet how a monad works, and I would like to see an explicit construction. For example, how can one construct an initial object from the axioms of a topos ? Or a coproduct ?

I have some vague ideas coming from the example where the topos is $\mathbf{Set}$, for example trying to construct $A\coprod B$ as a subset of $\Omega^{A\prod B}$, but I haven't managed to make any of them work.

• You should learn about monads. The concrete details are painful even in the case of the initial object: see here. – Zhen Lin Jul 26 '15 at 13:54
• Okay, I found indeed some ideas in here:ncatlab.org/nlab/show/Trimble+on+ETCS+III (I don't know how to do a link in comments), though not a complete formal proof. Indeed it seems painful. I'll wait to get to monads to come back to the problem; though I find it strange that the monad theory proof can not be translated into more elementary reasonable solution... – Sergio Jul 26 '15 at 19:07
• There is no reason to expect an elementary proof. Category theory may be abstract nonsense but it does simplify things sometimes. – Zhen Lin Jul 27 '15 at 0:27
• There is no reason not to expect an elementary proof. And I don't understand what your statement about category theory has to do with anything: the question is formulated in category theory language, so I certainly wouldn't expect a proof outside category theory. – Sergio Jul 29 '15 at 11:40

For each object $X$ the singleton subobjects $\{x\}:\Omega^X$ are minimal inhabited subobjects. Call the elements of the limit $\lim_X\Omega^{DX}$ inhabited if the disjunction $\bigvee_{d\in D_0}(\exists y: Dd.x_d(y))$ is valid--here $D_0$ is the finite set of objects of the diagram $D$. Now the colimit $\mathrm{colim}_x Dx$ is isomorphic to the subobject of minimal inhabited elements of $\lim_x\Omega^{Dx}$.

Edit: I assume that if you want to learn topos theory and do difficult things like defining colimits, you will figure out the details of the construction yourself. I will add some spoilers below just in case.

Thanks to their internal languages toposes are like parallel universes of mathematics whose logic can be constructive and which can contains things of different types than sets. So instead of $x\in y$ ($x$ is in $y$), I write $x:y$ ($x$ is of type $y$), instead of 'non empty' I say 'inhabited' and instead of 'true' I say 'valid'. It is a more accurate wording that sets the internal language of the topos apart from the external language of set theory.

The precise meaning of inhabited in toposes is subtle. Each morphism in a topos factors as a monomorphism following an epimorphism. For each object $X$ the unique morphism $!:X\to 1$ factors as the mono $\mathrm{supp}(X)\to 1$ after the epi $X\to\mathrm{supp}(X)$. The object $\mathrm{supp}(X)$ is the support of $X$. When the mono $\mathrm{supp}(X)\to 1$ is an isomorphism, $X$ is globally supported or inhabited.

For each object $X$ a morphism $\chi: X\to \Omega$ characterizes some subobject of $X$ and this subobject can also be inhabited. Parallel to the support construction, there is a morphism $(\chi\mapsto\exists x: X.\chi(x)):\Omega^X\to \Omega$, and when the subobject that $\chi$ characterizes is inhabited, $\exists x: X.\chi(x)=\top$, the greatest element of $\Omega$. Other ways to say this are that the proposition $\exists x: X.\chi(x)$ is valid and that $\chi$ is an inhabited subobject of $X$.

Minimal means the same thing here as it does everywhere. If $x$ is a minimal inhabited subobject and $y$ is a smaller inhabited subobject, then $y=x$.

• I'm sorry but I don't understand your answer. What does $d. x_{d}(y)$ mean, what is a valid disjunction, and how do you define a minimal inhabited subobject ? – Sergio Oct 21 '15 at 20:31
• If you don't know what a valid disjunction is, I suggest that you read an introduction to logic before trying to define colimits in toposes. – Wouter Stekelenburg Oct 21 '15 at 22:38
• Thanks for completing your answer, though I still don't get everything. For example, what does $DX$ mean, is it the diagram with all arrow the identity of X ? If so, trivially $\mathbb{colim}_{X} DX \simeq X$. And why is there a subscript ? – Sergio Oct 23 '15 at 19:22
• I'll try to complete your proof on my own though. I guess it indeed constructs $A\coprod B$ as a subset of $\Omega^{A\prod B}$ as I suspected when I posted the answer. – Sergio Oct 23 '15 at 19:24
• Actually, the coproduct $A+B$ is a subobject of $\Omega^A\times \Omega^B$ which consists of the pairs $(x,y)$ that satisfy $(\exists a: A.x(a))\vee(\exists b: B.x(b))$ and that minimal for this property. In the category of sets, that comes down to pairs $(x,y)$ where one of $x$ and $y$ is a singleton and the other is the emptyset. – Wouter Stekelenburg Oct 23 '15 at 20:31