Fibración de Grothendieck
Una fibración de Grothendieck (o categoría fibrada) es un funtor tal que para cualquier y cualquier existe un morfismo cartesiano tal que .
Definición formal[editar]
Sea un funtor. Un morfismo entre objetos de es cartesiano sobre el morfismo si y además para cualquier tal que existe un único tal que y . Decimos que el funtor es una fibración de Grothendieck si para cada morfismo de la forma existe un morfismo cartesiano sobre él.
Ejemplo[editar]
Consideramos la categoría cuyos objetos son pares determinados por un conjunto y un subconjunto suyo . Podemos interpretar cada uno de los objetos de la categoría como un predicado sobre los elementos del conjunto : el predicado que cumplen sólo aquellos elementos que pertenecen al subconjunto . Un morfismo desde hacia viene determinado por una función tal que ; es decir, que puede restringirse a .
La proyección determinada por es una fibración de Grothendieck. Para cada morfismo y cada predicado podemos construir el morfismo cartesiano determinado por un producto fibrado de la inclusión y . Este morfismo es cartesiano debido a la propiedad universal del producto fibrado.
Referencias[editar]
- Jacobs, Bart (1998). Categorical Logic and Type Theory (en inglés). Elsevier.