Fibración de Grothendieck

Una fibración de Grothendieck (o categoría fibrada) es un funtor $p\colon \mathbb {E} \to \mathbb {B}$ tal que para cualquier $E\in \mathbb {E}$ y cualquier $f\colon B\to p(E)$ existe un morfismo cartesiano $\phi \colon E'\to E$ tal que $p(\phi )=f$.

Definición formal

Sea $p\colon \mathbb {E} \to \mathbb {B}$ un funtor. Un morfismo $f\colon X\to Y$ entre objetos de $\mathbb {E}$ es cartesiano sobre el morfismo $u\colon I\to J$ si $p(f)=u$ y además para cualquier $g\colon Z\to Y$ tal que $p(g)=u\circ w$ existe un único $h\colon p(Z)\to J$ tal que $p(h)=w$ y $f\circ h=g$. Decimos que el funtor $p\colon \mathbb {E} \to \mathbb {B}$ es una fibración de Grothendieck si para cada morfismo de la forma $u\colon I\to p(Y)$ existe un morfismo cartesiano sobre él.

Ejemplo

Consideramos la categoría ${\mathsf {Pred}}$ cuyos objetos son pares determinados por un conjunto y un subconjunto suyo $X\subseteq I$. Podemos interpretar cada uno de los objetos de la categoría como un predicado sobre los elementos del conjunto $I$: el predicado que cumplen sólo aquellos elementos que pertenecen al subconjunto $X$. Un morfismo desde $X\subseteq I$ hacia $Y\subseteq J$ viene determinado por una función $u\colon I\to J$ tal que $u(X)\subseteq Y$; es decir, que puede restringirse a $u_{|X}\colon X\to Y$.

La proyección $\pi \colon {\mathsf {Pred}}\to {\mathsf {Set}}$ determinada por $\pi (X\subseteq I)=I$ es una fibración de Grothendieck. Para cada morfismo $u\colon I\to J$ y cada predicado $(Y\subseteq J)$ podemos construir el morfismo cartesiano $u^{\ast }(Y)\to Y$ determinado por un producto fibrado de la inclusión $Y\to J$ y $u\colon I\to J$. Este morfismo es cartesiano debido a la propiedad universal del producto fibrado.

Referencias

• Jacobs, Bart (1998). Categorical Logic and Type Theory (en inglés). Elsevier. 

• Datos: Q5446431