Esto es realmente sólo un comentario, pero es el camino demasiado largo. Ya que, en mi opinión, es de hecho muy lejos de una respuesta efectiva, yo la he hecho wiki de la comunidad - no creo que una reputación de bono para que sea apropiado. EDIT: al parecer, no sé cómo hacer que mi recuerdo es que había un cw casilla de verificación, pero no lo veo ahora) - si alguien sabe como hacer este cw, por favor.
Aquí es una manera de asignar una gavilla de un nombre que captura toda la estructura del nombre.
En primer lugar, la intuitiva versión. Cuando $\nu$ es un nombre y $p$ es una condición, tenemos una clase de $Elt^*_\nu(p)$ de los nombres dados por $$Elt^*_\nu(p)=\{\mu: p\Vdash \mu\in\nu\}$$ (donde el conjunto de soportes se utilizan un poco de forma abusiva).
Esta asignación es "sheafy" en el siguiente sentido. Poner el orden de la topología en $\mathbb{P}$, de manera tal que abrir los conjuntos son aquellos de la forma $$\mathbb{P}_p:=\{q\in\mathbb{P}: q\le p\}$$ for $p\in\mathbb{P}$. Then $p\mapsto Elt^*_\nu(p)$ , literalmente, es un paquete valorado en, bueno, está bien no es una gavilla, ya que es valorado en las clases, pero meh. En particular, la restricción = inclusión.
Así que esa es la idea. Ahora tenemos que solucionarlo. Por suerte, no es difícil (de ahí el "meh"):
Para los nombres de $\nu,\mu$ hay un nombre $\hat{\mu}$ tal que $(i)$ el rango de $\hat{\mu}$ (pensado como un conjunto normal) es menor que la de $\nu$ e $(ii)$ para cada condición de $q$ obligando a $\mu\in\nu$ también contamos $q\Vdash \mu=\hat{\mu}$.
Esto significa que con seguridad se puede restringir la atención a una pequeña clase - en particular, un conjunto de nombres y preservar la idea anterior. Específicamente se define el derecho de mapa de $Elt_\nu$ como $$Elt_\nu(p)=\{\mu\in V_{rk(\nu)}: p\Vdash\mu\in\nu\}.$$ This is now genuinely a sheaf, valued in names. Moreover, we can recover $\nu$ up to $\mathbb{1}$-forced equivalence from $Elt_\nu(p)$, so in a precise sense names are sheaves on $\mathbb{P}$ valorados en los nombres - como era de esperar recursiva noción.
Ahora vale la pena destacar que la construcción anterior satisface una cierta universalidad de la propiedad. Es decir, la fijación de un obligando noción $\mathbb{P}$, llamar a una clase de $\mathcal{C}$ del conjunto de valores de las poleas en $\mathbb{P}$ un nameslike clase si (jugando un poco con rapidez y soltura con la debida clases - si usted desea, estamos trabajando en NBG o MK en lugar de la vainilla ZFC):
Cada elemento de la imagen de una gavilla $S\in\mathcal{C}$ es una subclase (y necesariamente un conjunto) de $\mathcal{C}$.
Hay una función de clase $\rho:\mathcal{C}\rightarrow Ord$ o $S\in\mathcal{C}$ e $R\in im(S)$ tenemos $\rho(R)<\rho(S)$ (básicamente, esto garantiza tanto fundamento y establecer la semejanza).
- OK bien, esta es materialmente redundante (ninguna función puede tener un elemento de su imagen, de mayor rango que sí), pero es spiritualy no redundante: el panorama más general es considerar arbitraria de la clase de relación $R\subseteq \mathbb{P}\times V^2$ satisfacer ciertas propiedades, con $R(p,a,b)$ ser interpretado como $p\Vdash a\in b$. En principio, las estructuras adecuadas $V[G]_R$ (ver más abajo) puede ser infundada, o bien fundadas, sin embargo, el "taller" de $V$ sí. Esto parece potencialmente interesante para mí, pero innecesariamente general ahora, así que quiero que quede claro que estamos gobernando.
Dado cualquier nameslike clase $\mathcal{C}$ y cualquier $G$ que es $\mathbb{P}$-genérico más de $V$, se obtiene una clase de tamaño de $\in$estructura $V[G]_\mathcal{C}$ dada esencialmente por la toma de la extensional colapso de la estructura generada por el ajuste de $S_0\in S_1$ siempre $S_0\in S_1(p)$ para algunos $p\in G$. El punto ahora es:
En un preciso y sentido fuerte, $V[G]_\mathcal{C}$ siempre es un sub-cosa de $V[G]_{V^\mathbb{P}}$ (= $V[G]$ en el sentido usual de la palabra).
Formalizar y demostrar que esto no es difícil (aunque es un poco tedioso).
Todo eso es muy clásica, y aunque nunca he visto explícitamente estoy seguro de que es el folclore; el siguiente paso sería la levante para el contexto categorial. Los puntos clave que debe ser:
Cada Grothendieck topología $\tau$ a $\mathbb{P}$ da lugar, naturalmente, a una asociación para cada nombre de $\nu$ una gavilla $Elt_\nu^\tau$ a $(\mathbb{P},\tau)$ valorado en (de menor rango) de los nombres.
Tomando $\tau$ a ser el doble negación de la topología, obtenemos la construcción anterior (o algo equivalente).
Un análogo de la universalidad de la propiedad anterior deben tener.
A simple vista, parece que esta idea todavía funciona, pero no estoy lo suficientemente familiarizado con el tema a decir más al respecto.
