Fibración de Grothendieck

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

Definición formal

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

Ejemplo

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

La proyección ${\displaystyle \pi \colon {\mathsf {Pred}}\to {\mathsf {Set}}}$ determinada por ${\displaystyle \pi (X\subseteq I)=I}$ es una fibración de Grothendieck. Para cada morfismo ${\displaystyle u\colon I\to J}$ y cada predicado ${\displaystyle (Y\subseteq J)}$ podemos construir el morfismo cartesiano ${\displaystyle u^{\ast }(Y)\to Y}$ determinado por un producto fibrado de la inclusión ${\displaystyle Y\to J}$ y ${\displaystyle 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.