Prueba constructiva de un resultado clásico

Question

En un documento sobre constructivo de las matemáticas, vi el siguiente ejercicio : probar que $f^{-1}: \mathcal{P}(Y) \to \mathcal{P}(X)$ es inyectiva si y sólo si $f$ es surjective.

Hay un fácil constructivo prueba de la "si $f$ es surjective parte".

Sin embargo, la "si $f^{-1}$ es inyectiva" parte me escapa: Vamos a $y\in Y$. A continuación,$\{y\}\neq \emptyset$$f^{-1}(\{y\}) \neq f^{-1}(\emptyset)=\emptyset$.

Pero, ¿cómo puedo concluir a partir de $A\neq \emptyset$ que no es: $x\in A$ constructivamente ? Si no me equivoco, usted no puede (en el topos $\mathbf{Set}^2$, $(1, 0)$ no tiene ningún elemento global, aunque no es el objeto inicial - no sé mucho acerca de la teoría de topos todavía, así que no se puede formalizar esto, pero de forma heurística esto parece indicar que no hay ninguna prueba de $A\neq \emptyset \vdash \exists x, x\in A$)

Por lo que esta ruta parece condenado. Obviamente no puedo usar el contrapositivo porque yo sólo se consigue "Si $f^{-1}$ es inyectiva, a continuación, $f$ no no surjective" (y ni siquiera estoy seguro de que hay un fácil constructivo prueba de la contrapositivo)

Me temo que me estoy perdiendo algo obvio, pero yo no estoy acostumbrado a constructivas razonamiento en todo lo que sería de gran ayuda ! Y también, puede que mi argumento acerca de la $\mathbf{Set}^2$ formalizarse ?

Answer 1

Supongamos $f^{-1}$ es inyectiva. A continuación,$f^{-1}(\operatorname{im}(f)) = f^{-1}(Y) = X$; por lo tanto, $\operatorname{im}(f) = Y$.

Tenga en cuenta que en general topos, surjectivity de una función de $f : X \to Y$ no, en general, implica que el correspondiente mapa de global secciones $f(1) : X(1) \to Y(1)$ es surjective. Por ejemplo, si $\mathscr{F}$ $\mathscr{G}$ son poleas de los conjuntos en algún espacio topológico $X$, luego surjectivity de $f : \mathscr{F} \to \mathscr{G}$ significa que: para cada una de las $U \subseteq X$$y \in \mathscr{G}(U)$, existe un abierto de la cubierta $\{ V_i : i \in I \}$ $U$ y secciones $x_i \in \mathscr{F}(V_i)$ tal que $f(V_i) (x_i) = y |_{V_i}$ por cada $i \in I$.

De hecho, el fracaso del mundial de secciones de un general surjective mapa surjective es estudiado en detalle en gavilla cohomology de la teoría.

---

Sin embargo, usted está en lo correcto al afirmar que para$A \in \mathcal{P}(X)$, $A \ne \emptyset$ no, en general, implican $\exists x \in X, x \in A$. Para un contraejemplo, considerar el topos de las poleas de los conjuntos en $\mathbb{R}$, $X := 1$, y $A$ es la sección de la $\mathcal{P}(X)(1) \simeq \operatorname{Sub}(X)$ correspondiente a $\mathbb{R} \setminus \{ 0 \}$. Luego resulta que $A = \emptyset$ corresponde a $\emptyset \in \Omega(1)$, lo $A \ne \emptyset$ corresponde a $\mathbb{R} \in \Omega(1)$, mientras que el $\exists x \in X, x \in A$ corresponde a $\mathbb{R} \setminus \{ 0 \} \in \Omega(1)$.

De hecho, en general, $A \ne \emptyset$ es equivalente a $\lnot \lnot (\exists x \in X, x \in A)$.

Answer 2

Yo no sé acerca de topos y elementos iniciales. Aquí es un peatón prueba de su reclamación:

Se supone tácitamente que nos da un mapa de $f:\>X\to Y$. Deje $f(X)=Y'$. Para cada una de las $y\in Y'$ el conjunto $f^{-1}\bigl(\{y\}\bigr)=:X_y$ es no vacío, y los juegos $X_y$, $y\in Y'$, forma una partición de $X$ en distintos subconjuntos no vacíos.

Suponga $f$ es surjective. A continuación,$Y'=Y$. Tomar dos conjuntos diferentes $B_1$, $B_2\in{\cal P}(Y)$ y asumir, por ejemplo, que el $y\in B_2\setminus B_1$. Hay un $x$$f(x)=y$. Uno ha $x\in f^{-1}(B_2)$, pero $x\notin f^{-1}(B_1)$. Esto demuestra que $f^{-1}$ es inyectiva.

Suponga $f$ no es surjective. Luego hay un $y_0\in Y\setminus Y'$. De ello se deduce que para cualquier $B\subset Y'$ tenemos $B\cup\{y_0\}\ne B$, pero $f^{-1}(B\cup\{y_0\})=f^{-1}(B)$.