Estoy leyendo Categoría Básica de la Teoría de Científicos de la computación por Benjamin C. Pierce y en exercice de la 1.4.6, él le pregunta qué el terminal de objetos en $Set^\to$.
Deje $C$ ser una categoría.
La categoría de $C^\to$ se define como una categoría de modo que:
- Una obra en $C^\to$ es una flecha en $C$
- Una flecha en $C^\to$ $f:A\to B$ $f':A'\to B'$es un par $(a,b)$, de modo que el siguiente diagrama conmuta $$\requieren{AMScd} \begin{CD} A @>{a}>> A'\\ @V{f}VV @V{f'}VV \\ B @>{b}>> B' \end{CD}$$
Creo que he solucionado de esta prueba (pero agradecería comentarios sobre las pruebas):
Teorema 1: Terminal de objetos en $Set^\to$ son isomorphisms cuyo codominio es un terminal de objeto en $Set$:
Lema 2: Dado un morfismos $f:A\to B$ y un isomorfismo $f':A'\to B'$, $\exists !(a:A\to A',b:B\to B'), f;b=a;f'$ es equivalente a $\exists !b:B\to B'$.
Prueba 2: Desde $f'$ es un isomorfismo, $\exists !(a:A\to A',b:B\to B'), f;b=a;f'$ es equivalente a $\exists !(a:A\to A',b:B\to B'), f;b;f'^{-1}=a$. Ahora podemos demostrar que $\exists !(a:A\to A',b:B\to B'), f;b;f'^{-1}=a$ es equivalente a $\exists !b:B\to B'$.
"$\Longrightarrow$": Supongamos $\exists !(a:A\to A',b:B\to B'), f;b;f'^{-1}=a$. La existencia de $b:B\to B'$ es trivial. Supongamos que hay dos función de $b_1:B\to B'$$b_2:B\to B'$. Mediante el establecimiento $a_1:=f;b_1;f'^{-1}$$a_2:=f;b_2;f'^{-1}$, se contradice la hipótesis de la singularidad. Por lo $\exists !b:B\to B'$.
"$\Longleftarrow$": Supongamos $\exists !b$. La definición de $a:=f;b;f'^{-1}$, obtenemos la existencia de $(a:A\to A',b:B\to B')$. La singularidad de $b$ está dado por la hipótesis y la singularidad de $a$ para un determinado $b$ está garantizada por la ecuación, de modo $\exists !(a:A\to A',b:B\to B'), f;b=a;f'$.
Prueba 1:
"$\Longleftarrow$": Deje $f':A'\to B'$ ser un isomorfismo de modo que $B'$ es terminal en $Set$. Por definición, tenemos $\forall B \in Set, \exists !b:B\to B'$. Esto es equivalente a $\forall A,B\in Set, \forall f:A\to B, \exists !b:B\to B'$, lo que es, por el Lema 1, equivalente a $\forall A,B\in Set, \forall f:A\to B, \exists !(a:A\to A',b:B\to B'), f;b=a;f'$. Por lo $f'$ es terminal en $Set^\to$.
"$\Longrightarrow$": Deje $f':A'\to B'$ ser un terminal de objeto en $Set^\to$ (donde $A'$ $B'$ son objetos de $Set$).
Para demostrar que $f'$ es inyectiva, supongamos que no lo es. Podemos encontrar $x,y\in A'$, de modo que $x\not=y$ pero $f(x)=f(y)$. Y, a continuación, la función $$s:\left\{\begin{array}{ll} x\mapsto y\\ y\mapsto x\\ \lambda\mapsto \lambda \text{ for } \lambda\not\in\{x,y\} \end{array}\right.$$ that swaps $x$ and $s$ is a valid candidate for $$. Since $Id_A$ is a distinct valid candidate, $$ is not unique which is absurd so $f'$ es inyectiva. $$\requieren{AMScd} \begin{CD} {A'} @>{a:=Id_A\mid a := s}>> A'\\ @V{f'}VV @V{f'}VV \\ {B'} @>{b}>> B' \end{CD}$$
Para demostrar que $f'$ es surjective, supongamos que no lo es. Podemos encontrar $y\in B'$, de modo que $\forall x\in A', f(x)\not=y$.
- Si $B'$ contiene un elemento $z\in B'$, de modo que $z\not= y$, la función $$p:\left\{\begin{array}{ll} y\mapsto z\\ \lambda\mapsto \lambda \text{ for } \lambda\not=y \end{array}\right.$$ that sends all elements to themselves except $y$ which is sent to $z$ is a valid candidate for $b$. Since $Id_B$ is a distinct valid candidate, $b$ no es la única que es absurdo.
- Si $B'=\{y\}$, $\forall x\in A', f(x)\not = y$ tiene que ser vacuously verdad en lo $A'=\emptyset$. Configuración $A:=\{y\}$, $B:=\{y\}$ y $f:=Id_{\{y\}}$, no tenemos la existencia de $a$ lo cual es absurdo. $$\requieren{AMScd} \begin{CD} {A:=\{y\}} @>{a}>> A'=\emptyset\\ @V{f:=Id_{\{y\}}}VV @V{f'}VV \\ {B:=\{y\}} @>{b}>> B'=\{y\} \end{CD}$$
- Desde ambos casos, son absurdas, $f'$ es surjective.
Desde $f'$ es inyectiva y surjective, es bijective y por lo tanto es un isomorfismo en $Set$.
Para cualquier objeto $X$$Set$, podemos tomar $A:=X$, $B:=X$ y $f:=Id_X$. $$\requieren{AMScd} \begin{CD} A:=X @>{a}>> A'\\ @V{f:=Id_X}VV @V{f'}VV \\ B:=X @>{b}>> B' \end{CD}$$ Tenemos $\exists !(a:X\to A',b:X\to B'), f;b=a;f'$, lo que es, por el Lema 1, equivalente a $\exists !b:X\to B'$. Por lo $B'$ es terminal en $Set$.
He intentado generalizar esto para todas las categorías. Lema 1 parece ser general y no necesita ninguna modificación. En el Teorema 1, la parte que se vuelve difícil es probar que $f'$ es un isomorfismo. Supongo que debo demostrar que es monic y épica y, a continuación, encontrar una razón inversa (o de izquierda inversa) para probar que es un isomorfismo, pero yo no era capaz de hacer nada de eso.
Así que mi pregunta es: ¿hay una generalización del Teorema 1 para todas las categorías?
Si sí, entonces me gustaría saber exactamente la instrucción, y tal vez un toque en la dirección que debo tomar (incluyendo a la espera de saber más cosas, si es necesario) , pero no hay pruebas de que (a menos que sea un oculto prueba o vinculada a una prueba o prueba alguna de que no voy a ver hasta que yo quiera).
Si no, entonces me gustaría saber si hay una generalización de algunas categorías (asumo que debe haber algo para hacer con el álgebra categorías pero no he visto aún). También me gustaría ver un ejemplo en el que falla (oculto o vinculados y con juste un toque en la pregunta de si es un ejemplo, uno puede encontrar).
Gracias de antemano.
