# Constructive proof of a classical result

In a document about constructive maths, I saw the following exercise : prove that $f^{-1}: \mathcal{P}(Y) \to \mathcal{P}(X)$ is injective if and only if $f$ is surjective.

There is an easy constructive proof of the "if $f$ is surjective part".

However the "if $f^{-1}$ is injective" part eludes me: Let $y\in Y$. Then $\{y\}\neq \emptyset$ so $f^{-1}(\{y\}) \neq f^{-1}(\emptyset)=\emptyset$.

But how can I conclude from $A\neq \emptyset$ that there is $x\in A$ constructively ? If I'm not mistaken, you can't (in the topos $\mathbf{Set}^2$, $(1, 0)$ has no global element though it's not the initial object - I don't know much about topos theory yet so I can't formalize this but heuristically this seems to indicate that there is no proof of $A\neq \emptyset \vdash \exists x, x\in A$)

So this route seems doomed. Obviously I can't use the contrapositive because I would only get "If $f^{-1}$ is injective then $f$ is not not surjective" (and I'm not even sure there's an easy constructive proof of the contrapositive)

I'm afraid I'm missing something obvious, but I'm not used to constructive reasoning at all so it would be of great help ! And also, can my argument about $\mathbf{Set}^2$ be formalized ?

• Since Daniel already has given the answer, allow me to make a personal remark. Marvel at how beautiful Daniel's one-line proof is! This is one of the reasons why I'm drawn to constructive mathematics: The requirement to not use the law of excluded middle forces one to invest more energy in finding proofs (and formulating definitions), and often this case the investment pays off. If you allow yourself classical logic, then it's hard to avoid the much clumsier proof which immediately presents itself ("assume $f$ is not surjective, then there is an $y$ not in the image, ...") – at least for me. – Ingo Blechschmidt Apr 28 '18 at 14:51

Suppose $f^{-1}$ is injective. Then $f^{-1}(\operatorname{im}(f)) = f^{-1}(Y) = X$; therefore, $\operatorname{im}(f) = Y$.

Note that in a general topos, surjectivity of a function $f : X \to Y$ does not in general imply that the corresponding map of global sections $f(1) : X(1) \to Y(1)$ is surjective. For example, if $\mathscr{F}$ and $\mathscr{G}$ are sheaves of sets on some topological space $X$, then surjectivity of $f : \mathscr{F} \to \mathscr{G}$ means: for each open $U \subseteq X$ and $y \in \mathscr{G}(U)$, there is an open cover $\{ V_i : i \in I \}$ of $U$ and sections $x_i \in \mathscr{F}(V_i)$ such that $f(V_i) (x_i) = y |_{V_i}$ for each $i \in I$.

In fact, the failure of global sections of a general surjective map to be surjective is studied in detail in sheaf cohomology theory.

However, you are correct in stating that for $A \in \mathcal{P}(X)$, then $A \ne \emptyset$ does not in general imply $\exists x \in X, x \in A$. For a counterexample, consider the topos of sheaves of sets on $\mathbb{R}$, $X := 1$, and $A$ is the section of $\mathcal{P}(X)(1) \simeq \operatorname{Sub}(X)$ corresponding to $\mathbb{R} \setminus \{ 0 \}$. Then it turns out $A = \emptyset$ corresponds to $\emptyset \in \Omega(1)$, so $A \ne \emptyset$ corresponds to $\mathbb{R} \in \Omega(1)$, whereas $\exists x \in X, x \in A$ corresponds to $\mathbb{R} \setminus \{ 0 \} \in \Omega(1)$.

In fact, in general, $A \ne \emptyset$ is equivalent to $\lnot \lnot (\exists x \in X, x \in A)$.

• You know. People always complained to me how odd is set theory without choice. I am going to save a link to this answer and refer them whenever this issue comes up next... :) – Asaf Karagila Apr 27 '18 at 18:45
• Indeed I was missing something obvious ! I knew that it was a bad idea to use the definition of injectivity with $x\neq y \implies f(x) \neq f(y)$ because negation behaves weirdly constructively (at least to someone used to classical thinking). By the way does this still hold true if we no longer use "$f^{-1}$ is injective" but $A\neq B\implies f^{-1}(A)\neq f^{-1}(B)$ ? Thank you also for your precisions concerning sheaves; if you have the time could you also answer to the specific point concerning $\mathbf{Set}^2$ ? Thank you ! – Max Apr 27 '18 at 18:50
• I think the inclusion map $\mathbb{R} \setminus \{ 0 \} \hookrightarrow \mathbb{R}$ in the topos $\mathbb{R}$ might satisfy the contrapositive of $f^{-1}$ being injective; however, this inclusion map is not surjective. (Haven't checked the details, though.) – Daniel Schepler Apr 27 '18 at 19:05
• Ah, yes, the proposition that $f : R \setminus \{ 0 \} \hookrightarrow \mathbb{R}$ is surjective must have truth value at least $\mathbb{R} \setminus \{ 0 \}$, and therefore $\forall A, B \in \mathcal{P}(\mathbb{R}), A \ne B \rightarrow f^{-1}(A) \ne f^{-1}(B)$ must also have truth value at least $\mathbb{R} \setminus \{ 0 \}$. On the other hand, $\forall A, B \in \mathcal{P}(\mathbb{R}), A \ne B \rightarrow f^{-1}(A) \ne f^{-1}(B)$ is also a stable proposition; therefore, its truth value must be exactly $\top = \mathbb{R}$. – Daniel Schepler Apr 27 '18 at 19:44
• So, this forms a counterexample to $(\forall A, B \in \mathcal{P}(Y), A \ne B \rightarrow f(A) \ne f(B)) \rightarrow f$ is surjective. – Daniel Schepler Apr 27 '18 at 19:46