Looking for proof of monicity of co-product insertions

Question

Let C be a category satisfying the following axioms:

1. C contains an initial element, designated $0$;
2. C contains a terminal element, designated $1$;
3. $0$ and $1$ are not isomorphic;
4. $1$ is a separator in C; i.e. $((f_0, f_1:X \rightarrow Y) \wedge (\forall x:1\rightarrow X \; [f_0 \circ x = f_1 \circ x])) \Rightarrow (f_0 = f_1)$;
5. for any objects $A_0$, $A_1$ in C, their co-product $A_0 \oplus A_1$ is an object of C.

I'm looking for a proof of (or counterexample for) the following assertion:

All the canonical insertions of any binary co-product in C are monic.

Thanks!

PS: This question is derived from an exercise (2.12, p. 33) in Lawvere and Rosebrugh's Sets for Mathematics (2003). The original wording of the exercise is:

Prove on the basis of the axioms for $\cal{S}$ [i.e. Set] so far introduced that if $i_0:A_0 \rightarrow A, i_1:A_1 \rightarrow A$ is a sum in $\cal{S}$, then $i_0$ is a monomapping.

The five axioms I listed are those "so far introduced", as I understand them (except for the first one, which simply states that $\cal{S}$ is a category), and the definition given for "sums" is exactly the definition for co-products. The reason for leaving open the possibility that the assertion is false is that I may have misunderstood some aspect of the question, or of the axioms. In this case, a counterexample would help me see where I'm going wrong.

Answer 1

I must say I do not understand Beroal's completion/simplification of the comment. Let me allow to restate the argument.

Let $\iota_A \colon A \rightarrow A \sqcup B$ be a coproduct injection.

---

Observation: If we had any morphism $r \colon B \rightarrow A$, then we could apply the universal property of the coproduct to the morphisms $id_A \colon A \rightarrow A$ and $r \colon B \rightarrow A$ to obtain a morphism $h \colon A \sqcup B \rightarrow A$ that commutes with the identity $id_A$, and thus makes the injection $\iota_A$ a split monomorphism.

---

We have to show that for every pair of distinct morphisms $f \neq g \colon X \rightarrow A$ they precomposition with $\iota_A$ gives different morphisms --- that is: $\iota_A \circ f \neq \iota_A \circ g$. So, let us take such $f$ and $g$. Because the terminal object $1$ is a separator of the category and $f \neq g$, there exists $x \colon 1 \rightarrow A$. Therefore we have a morphism $r = f \circ x \circ ! \colon B \rightarrow A$, where $!$ is the unique morphism to the terminal object, what by the above observation completes the proof.

---

Zhen, my comment to your former answer about extensive categories, was just like a shoot to a fly with a cannon. Here is a simpler and more accurate argument, which consists of three relatively easy to prove facts:

• it suffices for a category to be distributive to have monic coproduct injections
• every cartesian closed category with coproducts is distributive
• every topos is cartesian closed and has coproducts

Answer 2

This is Mockup's proof, completed/simplified.

Definition. An object $A$ is inhabited if there exists an element of $A$.

Lemma 0. For every inhabited $A$ and every object $B$ there exists a constant morphism of type $B\to A$. Proof. It is $e\circ u$, where $e$ is that element of $A$, $u:B\to 1$. Qed.

Lemma 1. Suppose that an object $A$ is not inhabited. Every morphism $f$ from $A$ is a monomorphism. Proof. Suppose $e_0, e_1$ are elements of $A$. This contradicts that $A$ is not inhabited, then $e_0=e_1$. Then $f$ is an injective morphism. Then by Exercise 2.7 $f$ is a monomorphism. Qed.

Your question. Proof. Using the axiom of excluding middle, $A$ is inhabited or $A$ is not inhabited. If $A$ is not inhabited, then $\iota_0:A\to A+B$ is a monomorphism by Lemma 1. Suppose $A$ is inhabited, then there exists $c:B\to A$ by Lemma 0. $[id(A),c]\circ\iota_0 = id(A)$ by algebraic properties of the coproduct, then $\iota_0$ is a split monomorphism, then it is a monomorphism. Qed.

Square brackets denote sum of morphisms. Sum of morphisms is extracted from universal property of a coproduct, as well as the algebraic properties which I referred to. Moreover, a coproduct may be defined algebraically. Unfortunately, this seems to be omitted in your textbook.

Answer 3

I hope it's OK to post yet another proof.

---

Let $i_0:A_0 \rightarrow A, i_1:A_1 \rightarrow A$ be a sum in $\cal{S}$. To prove that $i_0$ is monic, the following simple lemma is useful. It follows directly from the definition of separator in the trivial case where there are no morphisms from the separator to some other object:

Lemma: Let $G$ be a separator in some category $\cal{C}$, and suppose for some object $X$ in $\cal{C}$ there are no morphisms $G \to X$. Then, for any object $Y\;$ in $\cal{C}$ there can be at most one morphism $X \to Y.\;\;$

Now, to prove that $i_0$ is monic, we consider two cases.

Case $0$: there are no morphisms $1 \to A_0$. In this case, if $\; \exists f:X \to A_0$, then there can be no morphisms $1 \to X$ either (otherwise, a morphism $1 \to A_0$ could be constructed by composing a morphism $1 \to X$ with $f\;$). Since $1$ is a separator in $\cal{S}$, by the lemma above, $f\;$ is the only morphism $X \to A$. Therefore, $i_0$ is (vacuously) monic.

Case $1$: there is a morphism $a:1\to A_0$. Then we also have the morphism $a \; \circ \; !_{A_1}:A_1 \to A_0$ (where $!_{A_1}$ is the unique morphism $A_1 \to 1$), which, together with $1_{A_0}:A_0 \to A_0$, entails the existence of a unique morphism $u:A_0 \oplus A_1 \to A_0$ with $u \circ i_0 = 1_{A_0}$ and $u \circ i_1 = {a} \; \circ \; !_{A_1}$. This means that $u$ is a left inverse of $i_0$, which implies that $i_0$ is left-cancellable, or, equivalently, that $i_0$ is monic. $_\blacksquare$

---

While thinking about this problem, I realized that a very simple category (which Goldblatt calls $\mathbf{2}$), consisting of two objects, an initial $0$ and a terminal $1$, and three mandatory morphisms (the two identities, and $0 \to 1$) satisfies all the five axioms in the original problem statement (although vacuously so for axiom 4 and "most" of axiom 5). This explains to me why my intuitions based on my prior knowledge of standard set theory led me astray so often: there's a lot more to $\cal{S}$ than those axioms allow for.

This also relates to what I see as the only merit in my proof (and the reason I decided to post it even though other fine proofs had already been posted), namely that it reflects the bipartite structure that the five axioms impose on the category (and epitomized by the category $\mathbf{2}$ described above), in which objects are partitioned into two non-empty equivalence classes according to whether they are codomains to some morphism with domain $1$ or not.

---

Thanks to all who responded. This was an unexpectedly instructive exercise.