Fibración de Grothendieck

Una fibración de Grothendieck (o categoria fibrada) és un funtor $p:𝔼\to 𝔹$ tal que per a qualsevol $E\in 𝔼$ i qualsevol $f:B\to p(E)$ existix un morfismo cartesiano $\varphi :E^{\prime }\to E$ tal que $p(\varphi )=f$.

Definició formal

Siga $p:𝔼\to 𝔹$ un funtor. Un morfismo $f:X\to Y$ entre objectes de $𝔼$ és cartesiano sobre el morfismo $u:I\to J$ si $p(f)=u$ i ademés per a qualsevol $g:Z\to Y$ tal que $p(g)=u\circ w$ existix un únic $h:p(Z)\to J$ tal que $p(h)=w$ i $f\circ h=g$. Diem que el funtor $p:𝔼\to 𝔹$ és una fibración de Grothendieck si per a cada morfismo de la forma $u:I\to p(Y)$ existix un morfismo cartesiano sobre ell.

Eixemple

Considerem la categoria $𝖯𝗋𝖾𝖽$ els objectes de la qual són parells determinats per un conjunt i un subconjunt seu $X\subseteq I$. Podem interpretar cada u dels objectes de la categoria com un predicat sobre els elements del conjunt $I$: el predicat que complixen només aquells elements que pertanyen al subconjunt $X$. Un morfismo des de $X\subseteq I$ cap a $Y\subseteq J$ ve determinat per una funció $u:I\to J$ tal que $u(X)\subseteq Y$; és dir, que pot restringir-se a $u_{|X}:X\to Y$.

La proyecció $\pi :𝖯𝗋𝖾𝖽\to 𝖲𝖾𝗍$ determinada per $\pi (X\subseteq I)=I$ és una fibración de Grothendieck. Per a cada morfismo $u:I\to J$ i cada predicat $(Y\subseteq J)$ podem construir el morfismo cartesiano $u^{\ast }(Y)\to Y$ determinat per un producte fibrado de l'inclusió $Y\to J$ i $u:I\to J$. Este morfismo és cartesiano per la propietat universal del producte fibrado.

Referències

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