En la categoría de conjuntos, de los límites y colimits pueden ser de hormigón descritos, respectivamente, como subobjetos de productos y cocientes de co-productos.
Parece que estas descripciones tienen sentido en cualquier primaria topos. Me preguntaba si realmente describir los límites correspondientes y colimits, y la forma de ver esto.
Voy a estar usando la definición de una escuela primaria topos como un finitely completa cartesiana cerrada categoría con un subobjeto clasificador como esta definición se ajusta más bien con el tipo teórico de las nociones. Mientras voy a formular la sintaxis y las reglas de límites, no tiene sentido preguntar qué son concretamente desde que son parte de la supuesta estructura. Se puede demostrar que son isomorfos a otras cosas que se definen en términos de la estructura, si quieres.
De pasar, finito productos y cartesiana de cierre significa que nuestro lenguaje interno contiene un tipo simple cálculo lambda con los productos. No voy a explicar esa estructura. Finito integridad significa también hemos ecualizadores para que voy a usar el siguiente tipo de formación, la introducción y la eliminación de las reglas: $$\frac{\Gamma, x:A \vdash M(x) : B \qquad \Gamma, x:A \vdash N(x) : B}{\Gamma \vdash \{ x \in A\ |\ M(x) =_B N(x)\}}$$ $$\frac{\Gamma \vdash E : \qquad \Gamma \vdash M(E)\equiv N(E)}{\Gamma \vdash \iota_{M,N}(E) : \{x\in A\ |\ M(x) =_B N(x)\}}\qquad \frac{\Gamma \vdash E : \{ x\in A\ |\ M(x)=_B N(x)\}}{\Gamma \vdash \pi_{M,N}(E) : A}$$ $$\frac{\Gamma \vdash E : \{ x\in A\ |\ M(x) =_B N(x)\}}{\Gamma \vdash M(\pi_{M,N}(E)) \equiv N(\pi_{M,N}(E))}$$ $$\frac{\Gamma \vdash E :\{ x\in A\ |\ M(x)=_B N(x)\}}{\Gamma \vdash \iota_{M,N}(\pi_{M,N}(E)) \equiv E}\qquad \frac{\Gamma \vdash E : \qquad \Gamma \vdash M(E) \equiv N(E)}{\Gamma \vdash \pi_{M,N}(\iota_{M,N}(E)) \equiv E}$$
Aquí $\Gamma \vdash M \equiv N$ $M$ $N$ son definitionally igual. Cuando dos cosas son definitionally iguales, entonces tratamos exactamente el mismo en todas partes (es decir, la definición de la igualdad es una congruencia en nuestro tipo de teoría). Para nuestros propósitos, cada definición de la igualdad tenemos que comprobar de que seremos capaces de comprobar por la reducción de ambos lados a una forma normal y, a continuación, la comprobación sintáctica de igualdad (hasta alfa de equivalencia, es decir, modulo para cambiar el nombre de las variables vinculadas). La reducción de las reglas del cálculo lambda que necesitamos venir desde el triángulo de las identidades para la adjunctions la definición cartesiana de cierre. También, los subíndices en $\iota$ $\pi$ generalmente puede deducir de su contexto, así que voy a estar suelto con ellos, el uso de algo para sugerir el ecualizador adecuado.
La existencia de un subobjeto clasificador (y ecualizadores) implica inmediatamente que todos los monomorphisms son regulares, por lo que voy a hacer un poco de trampa y se supone que también. A continuación, un subobjeto clasificador, sólo significa que por cada ecualizador tenemos una (única) características de morfismos. Formalmente, tenemos un tipo de $\Omega$ y un punto de $\top : \Omega$ y, con el corto la mano $E_{A,B}(M,N)$$\{ x \in A\ |\ M(x)=_B N(x)\}$, $$\frac{\Gamma \vdash \{ x\in A\ |\ M(x) =_B N(x)\}}{\Gamma, x: \vdash \chi_{E_{A,B}(M,N)}(x) : \Omega} \quad \frac{\Gamma \vdash E : \{ x\in A\ |\ M(x) =_B N(x)\}}{\Gamma \vdash \chi_{E_{A,B}(M,N)}(\pi_{M,N}(E))\equiv \top}\quad \frac{\Gamma \vdash E : \{ x\in A\ |\ \chi_{E_{A,B}(M,N)}(x) =_\Omega \top\}}{\Gamma \vdash M(\pi_{\chi}(E))\equiv N(\pi_{\chi}(E))}$$
Lo anterior implica que cada ecualizador $\{ x\in A\ |\ M(x)=_B N(x)\}$ es isomorfo a un ecualizador de la forma$\{ x\in A\ |\ P(x) =_\Omega \top\}$, lo que voy a abreviar como $\{ x\in A\ |\ P(x)\}$. Hay otras maneras de formular todo esto, y no he usado el totalmente elaborado de forma incluso de las normas previstas.
Que era un montón de instalación para siquiera empezar a responder la pregunta. Tiempo para construir el arsenal. Para cualquier tipo de $A$, $= : A\times A \to \Omega$ través $\chi_{E_{A\times A,A}(\pi_1,\pi_2)}$. Esto le da a los únicos a través de $\{M\}\equiv(\lambda x.x =_A M) : \Omega^A$. Un paso fundamental es que tenemos dos valores de tipo $\Omega^\Omega$, es decir,$\lambda x.x$$\lambda x.\top$. La categoría completa se derrumba si estos son iguales. Definimos el objeto inicial $0_A$ través $\{ t \in A\ |\ (\lambda x.x) =_{\Omega^\Omega} (\lambda x.\top)\}$. Esto nos permite definir los $\bot \equiv \chi_{0_1}(\langle\rangle) : \Omega$$\emptyset_A \equiv (\lambda x.\bot) : \Omega^A$. (Un inciso, si lo desea, puede definir $\in_A \equiv (\lambda\langle x,p \rangle.p(x)) : A\times\Omega^A \to \Omega$.)
Desarrollarse el álgebra de Heyting estructura de $\Omega$ un poco más, tenemos: $$\begin{align} \land \equiv (\lambda p.p = \langle\top,\top\rangle) \qquad &\Rightarrow \equiv (\lambda\langle x,y \rangle. x\land y = x) \\ \lor \equiv (\lambda p.p \neq \langle\bot,\bot\rangle) \qquad &\lnot \equiv (\lambda x. x\Rightarrow\bot) \end{align}$$
(No estoy muy seguro de estas definiciones. Estoy tratando de falda de la necesidad de hablar de monomorphisms y el Sub functor. Ver Toposes, Triples y Teorías para más estándar y autorizado de la cuenta.)
También tenemos los cuantificadores $$ \forall_A \equiv (\lambda p. p = \lambda x.\la parte superior) : \Omega^A\a\Omega \qquad \exists_A \equiv (\lambda p. p\neq \emptyset_A) : \Omega^A\a\Omega \\ \existe!_A \equiv (\lambda p. \exists_A (\lambda x. p = \{x\})) : \Omega^A\a\Omega$$ which leads to the image, $\text{im}(f) \equiv \{ y \in B\ |\ \exists_A(\lambda x. y = f(x)) \}$ and the direct image $f_* \equiv \lambda p.\lambda y.\exists_A(\lambda x.p(x)\de la tierra f(x) = y) : \Omega^A\a\Omega^B$ if $f : A\B$. $\existe!$ es la clave para ser capaz de ir de objetos de poder volver a la llanura de los objetos, ya que muestra que el singleton mapa es un ecualizador.
Para el subproducto, guiados por $C^{A+B}\cong C^A\times C^B$ y el conjunto teórico de intuiciones, hacemos las siguientes definiciones $$A+B \equiv \{ \langle p,q\rangle \en \Omega^A\times\Omega^B\ |\ (\existe!_A(p)\la tierra q = \emptyset_B) \lor (p = \emptyset_A \de la tierra \existe!_B(q))\} \\ \mathtt{inl} \equiv \lambda x.\iota(\langle\{x\},\emptyset_B\rangle) \qquad \mathtt{inr} \equiv \lambda y.\iota(\langle\emptyset_A,\{y\}\rangle) \\ f+g \equiv \lambda s.\iota_{A'+B'}((f_*\times g_*)(\pi_{A+B}(s)))\text{ donde } f:\'\text{ y }g : B\B' \\ \varepsilon \equiv (\lambda s.\iota_{\existe!_C}(\cup_C(\pi_{A+B}(s)))) : C+C \C\text{ donde }\cup_C \equiv \lambda\langle p,q \rangle.\lambda c.p(c)\lor p(c)$$
Finalmente, para obtener todos finito colimits necesitamos coequalizers o pushouts. Voy a hacer coequalizers. Que va desde el conjunto teórico de la intuición, la parte del objeto es relativamente fácil. Si queremos encontrar la coequalizer de $f,g : A \to B$, debemos en primer lugar definir la relación $$\sim \equiv (\lambda b_1.\lambda b_2.\exists_A(\lambda a. f(a) = b_1 \land g(a) = b_2)) : B \to \Omega^B$$ and its reflexive, symmetric, transitive closure $\sim^*$. How to do the transitive closure part I'll cover later. The reflexive and symmetric part is easy. $\sim^*$ coequalizes $f$ and $g$, and $p : B \a \text{im}(\sim^*)$ will be the coequalizer. Notice that the image corresponds to the set of equivalence classes. We need to show that given $h : B \a C$ which coequalizes $f$ and $g$, there's a unique arrow $\text{im}(\sim^*)\a C$. We'll use the same trick as before: if we can show that the image of $h_* \circ \pi: \text{im}(\sim^*)\a\Omega^C$ is always a singleton, then we can use the fact that the singleton map is an equalizer to get a map $\iota_{\existe!_C} : \text{im}(\sim^*)\a C$. For this to happen, $h$ needs to send every element of an equivalence class to a single element. Specifically, the formula is $$h_*(\lambda b.b_1\sim^* b) = \lambda c.\exists_B(\lambda b_2. b_1\sim^* b_2 \land h(b_2) = c)$$ It's easy enough to show that this is a singleton, in particular $\{h(b_1)\}$. This also shows that $h = \iota_{\existe!_C} \circ q$.
Todo lo que queda ahora es demostrar que podemos hacer la clausura transitiva de una relación. Sería sencillo si tuviéramos un números naturales objeto, pero no hemos asumido que. En lugar de ello, vamos a dividir el tipo de relaciones binarias hasta que nos quedamos con lo que queremos. Para empezar, podemos hacer el tipo de todos los reflexiva, simétrica, transitiva de la relación que contengan $\sim$. $$\begin{align} P_\sim(S) & \equiv \forall_B(\lambda b_1. \forall_B(\lambda b_2. b_1 \sim b_2 \Rightarrow S(\langle b_1, b_2 \rangle))) \\ & \land \forall_B(\lambda b. S(\langle b, b \rangle)) \\ & \land \forall_B(\lambda b_1. \forall_B(\lambda b_2. S(\langle b_1, b_2 \rangle) \Rightarrow S(\langle b_2, b_1 \rangle))) \\ & \land \forall_B(\lambda b_1. \forall_B(\lambda b_2. (\exists_B(\lambda b. S(\langle b_1, b \rangle) \land S(\langle b, b_2 \rangle)) \Rightarrow S(\langle b_1, b_2 \rangle))) \\ \\ T_\sim & \equiv \{ S \in \Omega^{B\times B}\ |\ P_\sim(S)\} \end{align}$$
$T_\sim$ es el tipo de todos los reflexiva, simétrica, transitiva relaciones que contengan $\sim$, incluyendo, por ejemplo,$B\times B$. A continuación, nos tallar hacia abajo a un mínimo elemento. $$M_{\sim} \equiv \{ S \in T_\sim\ |\ \forall_{T_{\sim}}(\lambda R. \forall_{B\times B}(\lambda\langle b_1, b_2 \rangle. \pi(S)(b_1, b_2) \Rightarrow \pi(R)(b_1, b_2)))\}$$
Si podemos mostrar a $M_{\sim} \cong 1$, luego que el empate iba a recoger $\sim^*$. Vamos a suponer que se hace y lo llaman un día. Hay muchas más pruebas de las obligaciones en el de arriba de este. Por ejemplo, el uso de $\iota$ o la comprobación de que las operaciones de co-productos de satisfacer todas las leyes, por ejemplo, $f+g$ es functorial.
He sido, en su mayoría haciendo esto ya que van junto con vagos recuerdos de la más estándar, categoría (es decir, no interno basado en el lenguaje) correr en Toposes, Triples y Teorías, que recomiendo la lectura de la toposes secciones. Deben empezar a partir de objetos de poder. Sin embargo, aunque no estoy 100% seguro acerca de algunas de las definiciones y me sorprendería si los hay no los errores, estoy razonablemente seguro de los trazos en particular para las partes más relevantes a su pregunta.
I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.
