# In the category of sets epimorphisms are surjective - Constructive Proof?

The statement that surjective maps are epimorphisms in the category of sets can be shown in a constructive way.

Is it possible to show that every epimorphism in the category of sets is surjective without reverting to a proof by contradiction / negation?

-
Given the epimorphism $f$ define $g:Y\to\lbrace 0,1\rbrace$ by $g(y)=1$ if $y\in f(X)$ and $g(y)=0$ else. For the constant function $h(y)=1$ you have $g\circ f=h\circ f$ so that $g=h$. Hence, every $y\in Y$ belongs to $f(X)$ and $g$ is surjective. –  Jochen Wengenroth Aug 18 '14 at 10:24
@JochenWengenroth: Why is $y\in f(X)$ decidable? –  Emil Jeřábek Aug 18 '14 at 10:44
I think that depend on what you mean by "constructive". if it is "topos valid"/without excluded middle then it is indeed true : consider two maps from $Y$ to the object obtained from $Y$ be identifying any two points which are in the image of $X$. –  Simon Henry Aug 18 '14 at 11:22
@AndreasCaicedo, I do not understand why you have removed tag "set-theory". As for me, the question is exactly about set theory (moreover, it is formulated in such a way, that it is about the standard set theory). –  Michal R. Przybylek Aug 18 '14 at 19:50

Theorem: Every epi is surjective.

Proof. Let $h : A \to B$ be an epimorphism. We define maps $f, g : B \to \mathcal{P}(B)$ by \begin{align*} f(b) &= \{b\} \cap \mathrm{im}(h)\\ g(b) &= \{b\} \end{align*} where we recall that $\mathrm{im}(h) = \{b \in B \mid \exists a \in A \,.\, h(a) = b\}$.

For every $a \in A$ we have $f(h(a)) = \{h(a)\} = g(h(a))$, therefore $f = g$ as $h$ is epi. Now, for every $y \in B$ we have $\{y\} = g(y) = f(y) = \{y\} \cap \mathrm{im}(h)$, therefore $y \in \mathrm{im}(h)$. QED.

-
Is this really different from the argument in my comment? –  Jochen Wengenroth Aug 19 '14 at 7:43
It is not really different, but I would say that it is less mysterious. –  Andrej Bauer Aug 19 '14 at 8:31
Thanks for the many answers; I liked this one best: I'm actually not working in Set but rather in Enriched Categories so this should be a proof that might translate to my setting. –  Garlef Wegart Aug 19 '14 at 10:36
@GarlefWegart So what are you really trying to prove? That every epimorphism is a extremal epimorphism? Or regular? Or split? –  Zhen Lin Aug 19 '14 at 16:46
@JochenWengenroth This proof would be the same as the one in your comment if classical logic were available. As Emil pointed out in the comment after yours, your formulation assumes that every $y$ is either in $f(X)$ or not, so that the two cases in your definition of $g$ cover every $y$. Andrej's answer avoids that case distinction, so it is valid even in constructive logic. The price for that is that, unlike your $g$ whose values are 0 or 1, his $f$ takes values not (constructively) known to be $\varnothing$ or $\{b\}$. –  Andreas Blass Aug 20 '14 at 3:02

The statement "a morphism is a surjection iff it is an epimorphism" holds in every topos, regardless of the law of excluded middle.

The precise proof depends on your notion of "surjection" (in a topos all reasonable internal notions of a surjection coincide --- in fact, due to the above statement, one may define a surjection as an epimorphism).

Perhaps the most obvious notion is: a morphism $s \colon A \rightarrow B$ is a surjection if whenever $b \in B$ then $\underset{a\in A}\exists s(a) = b$ in the internal logic of the category. If a category is regular, then such surjections coincide with covers. And covers are another obvious notion for surjections: a morphism $s \colon A \rightarrow B$ is a surjection (i.e. cover) if in the image-factorisation $A \rightarrow s[A] \rightarrow B$ the monomorphism $s[A] \rightarrow B$ is iso.

Since every topos is a balanced category, in every topos covers coincide with epimorphisms.

-

Here's a proof in constructive set theory (probably just a rephrasing of the topos theoretic proof but you might find it useful).

Let $h : A \twoheadrightarrow B$ be an epimorphism. Define $$C := \{\{0\}\} \cup \bigcup_{b \in B}\{\{x \in \{0\} \;|\; \exists a \in A\; h(a)=b\}\}$$ (If the powerset axiom is available, one can alternatively use $C := \mathcal{P}(\{0\})$)

Define functions $f, g : B \rightarrow C$ as follows. $$f(b) := \{ x \in \{0\} \;|\; \exists a \in A\;h(a) = b \} \\ g(b) := \{0\}$$

We clearly have $f \circ h = g \circ h$, so since $h$ is an epimorphism, we get $f = g$. Now for any $b \in B$, we have that $f(b) = g(b)$. Therefore the set $\{x \in \{0\} \;|\; \exists a \in A \; h(a) = b \}$ is inhabited, and so there exists $a$ in $A$ such that $h(a) = b$.

-
Actually, you need the power-set axiom to write your first definition. The second one, just says that $C := \mathcal{P}(\{0\}) = \Omega$, where $\Omega$ is the set of internal truth-values. –  Michal R. Przybylek Aug 18 '14 at 13:49
Then, $f, g : B \rightarrow \Omega$ become predicates on $B$, where $f$ expresses the statement that $h$ is internally surjective, and $g := \top_B$. Therefore, $f = g$ says that "$h$ is internally injective" is true. –  Michal R. Przybylek Aug 18 '14 at 13:55
I claim that the first definition of C requires only bounded separation, strong collection and union (and pairing), so it's provably a set in CZF, for instance. I maybe should have been clearer that the first definition of C gives a different, in general strictly smaller set than the second. –  aws Aug 18 '14 at 14:48
Sorry, then I still don't understand your construction --- could you write it down in a bit more formal way? I don't claim that you're wrong, I just want to understand what exactly you are doing. I think your proof cannot be carried to a general predicative universe --- I claim that in any regular category the statement "epi iff surjection" is equivalent to "bimorphism iff iso" (i.e. to the statement that the category is balanced). Clearly, every topos is balanced (because $\Omega$ classifies morphism), (cont...) –  Michal R. Przybylek Aug 18 '14 at 17:47
(...) but I don't see any reason why every $\Pi \Sigma$-pretopos, or any other notion of a predicative universe should be balanced (of course, CZF is balanced, so technically your claim is correct, but I'd like to see the exact reason behind this fact). –  Michal R. Przybylek Aug 18 '14 at 17:48