Displayed category theory MOC

Cartesian fibration

Let 𝖀 β‡₯𝖑 be a displayed category. A cartesian lift of a morphism 𝑓 :π‘₯ →𝑦 at some 𝑦′ over 𝑦 consists of an object π‘“βˆ—π‘¦β€² βˆˆπ–‘π‘₯ and a cartesian morphism πœ‹βˆ—π‘¦β€²π‘“β€² :π‘“βˆ—π‘¦ →𝑓𝑦′. Such a cartesian lift is unique up to unique isomorphism.

Proof of uniqueness

One can show that if 𝑓′ :π‘₯β€² →𝑓𝑦′ is cartesian then there is a unique vertical isomorphism πœ‘ :π‘₯β€² β‰…π‘₯π‘“βˆ—π‘¦β€² such that (πœ‹π‘¦β€²π‘“)πœ‘ =𝑓′. This is done by feeding 𝑒 =π‘₯, π‘š =idπ‘₯, and β„Žβ€² =𝑓 into the definition of a cartesian morphism. Repeating this argument gives a vertical morphism in the opposite direction, and shows that the composition of these two must be the vertical identity morphism.

We say that 𝖀 β‡₯𝖑 is a cartesian fibration over 𝖑 iff there is a cartesian lift for every bottom-right corner. Often this notion is simply referred to as a fibration, since it coΓ―ncides with Grothendieck’s notion.

Functoriality

A cartesian fibration 𝖀 β‡₯𝖑 captures the notion of a 2-functorial family of categories fib⁑(𝖀) :𝖑𝐨𝐩――― β†’β„­π”žπ”±, taking

where π‘“βˆ— :𝖀𝑦 →𝖀π‘₯ is the base change functor taking

Functoriality of π‘“βˆ—

The diagram above commutes for 𝑣 =id′𝑦′ and π‘“βˆ—id′𝑦′ =idβ€²π‘₯β€². One can similarly show that π‘“βˆ—(𝑀𝑣) =(π‘“βˆ—π‘€)(π‘“βˆ—π‘£).

2-functoriality fib(𝖀) :𝖑𝐨𝐩――― β†’β„­π”žπ”±

The compositor for π‘₯,𝑦,𝑧 βˆˆπ–‘0 has components which are themselves natural isomorphisms, namely

𝛾𝑓,𝑔:π‘“βˆ—π‘”βˆ—β‡’(𝑔𝑓)βˆ—:𝖀𝑧→𝖀𝑦

for π‘₯𝑓→𝑦𝑔→𝑧 in 𝖑. These are constructed using the fact that the composite of cartesian morphisms is cartesian and the uniqueness of cartesian lifts: In the diagram

c|https://q.uiver.app/#q=WzAsMTIsWzIsNSwieCJdLFs0LDUsInkiXSxbNCwzLCJnXip6JyJdLFs0LDEsImdeKnonJyJdLFsyLDMsImZeKmdeKnonIl0sWzIsMSwiZl4qZ14qeicnIl0sWzYsNSwieiJdLFs2LDMsInonIl0sWzYsMSwieicnIl0sWzAsMiwiKGdmKV4qeiciXSxbMCwwLCIoZ2YpXip6JyciXSxbMCw0LCJ4Il0sWzIsMSwiIiwyLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibWFwcyB0byJ9fX1dLFswLDEsImYiLDJdLFs0LDAsIiIsMix7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1hcHMgdG8ifX19XSxbNCwyLCJcXHBpXipmIiwyXSxbNSwzLCJcXHBpXipmIl0sWzEsNiwiZyIsMl0sWzcsNiwiIiwxLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibWFwcyB0byJ9fX1dLFsyLDcsIlxccGleKiBnIiwyXSxbMyw4LCJcXHBpXipnIl0sWzgsNywidiJdLFszLDIsImdeKnYiLDFdLFs1LDQsImZeKmdeKiB2IiwyXSxbMTAsOSwiKGdmKV4qdiIsMl0sWzEwLDgsIlxccGleKihnZikiLDAseyJjdXJ2ZSI6LTJ9XSxbOSw3LCJcXHBpXiooZmcpIiwwLHsiY3VydmUiOi0yfV0sWzUsMTAsIihcXGdhbW1hX3tmLGd9KV97eicnfSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs0LDksIihcXGdhbW1hX3tmLGd9KV97eid9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzExLDAsIiIsMSx7ImxldmVsIjoyLCJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzksMTEsIiIsMSx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1hcHMgdG8ifX19XV0=

we see that both πœ‹βˆ—π‘§β€²(𝑓𝑔) and πœ‹βˆ—π‘”βˆ—π‘§β€²π‘“ are cartesian lifts of 𝑔𝑓, therefore they must be related by an isomorphism (𝛾𝑓,𝑔)𝑧′. Uniqueness arguments show that the entire diagram commutes, and we see that 𝛾𝑓,𝑔 is natural. Since 𝖑op――― is locally discrete, naturality of 𝛾 is free.

The unitor for π‘₯ βˆˆπ–‘0 is a natural isomorphism

𝜈:1𝖀π‘₯β‡’(1π‘₯)βˆ—:𝖀π‘₯→𝖀π‘₯.

This can be obtained quite directly from the diagram

c|https://q.uiver.app/#q=WzAsMTAsWzIsNSwieCJdLFs0LDUsIngiXSxbNCwzLCJ4JyJdLFsyLDMsIigxX3gpXip4JyJdLFs0LDEsIngnJyJdLFsyLDEsIigxX3gpXip4JyciXSxbNiwyXSxbMCwyLCJ4JyJdLFswLDQsIngiXSxbMCwwLCJ4JyciXSxbMiwxLCIiLDIseyJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJtYXBzIHRvIn19fV0sWzAsMSwiIiwyLHsibGV2ZWwiOjIsInN0eWxlIjp7ImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMywwLCIiLDIseyJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJtYXBzIHRvIn19fV0sWzMsMiwiXFxwaV97eCd9XioxX3giLDFdLFszLDEsIiIsMCx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dLFs0LDIsInYiXSxbNSwzLCIoMV94KV4qdiIsMl0sWzUsNCwiXFxwaV4qX3t4Jyd9MV94Il0sWzcsMiwiIiwxLHsiY3VydmUiOi0yLCJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFswLDgsIiIsMix7ImxldmVsIjoyLCJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzcsOCwiIiwyLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibWFwcyB0byJ9fX1dLFs5LDcsInYiLDJdLFs0LDksIiIsMix7ImN1cnZlIjoyLCJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFs3LDMsIlxcbnVfe3gnfSIsMSx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs5LDUsIlxcbnVfe3gnJ30iLDEseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0=

which constructs 𝜈π‘₯β€² using the cartesian lift of 1π‘₯ as the universal factoring of the displayed identity. The inverse is given by the cartesian lift itself, and we also witness naturality.

Let π‘Žπ‘“β†’π‘π‘”β†’π‘β„Žβ†’π‘‘ in 𝖑. Unwrapping the hexagon, the left hand side reads

π‘“βˆ—π‘”βˆ—β„Žβˆ—π›Ύπ‘“,π‘”βˆ˜β„Žβˆ—β‡β‡β‡β‡β‡β‡β‡β‡β‡β‡β‡’(𝑔𝑓)βˆ—β„Žβˆ—π›Ύπ‘”π‘“,β„Žβ‡β‡β‡β‡β‡β‡β‡β‡β‡’(β„Ž(𝑔𝑓))βˆ—π›Όβˆ—βŸΉ((β„Žπ‘”)𝑓)βˆ—:π–€π‘‘β†’π–€π‘Ž

where 𝛼 is the unique witness that β„Ž(𝑔𝑓) =(β„Žπ‘”)𝑓 in 𝖑; and the right hand side reads

π‘“βˆ—π‘”βˆ—β„Žβˆ—idβŸΉπ‘“βˆ—π‘”βˆ—β„Žβˆ—π‘“βˆ—βˆ˜π›Ύπ‘“,π‘”β‡β‡β‡β‡β‡β‡β‡β‡β‡β‡β‡’π‘“βˆ—(β„Žπ‘”)βˆ—π›Ύπ‘“,β„Žπ‘”β‡β‡β‡β‡β‡β‡β‡β‡β‡’((β„Žπ‘”)𝑓)βˆ—:π–€π‘‘β†’π–€π‘Ž.

Let 𝑑′ be an object over 𝑑. Then at 𝑑′ the left hand side is constructed by the diagram

c|https://q.uiver.app/#q=WzAsMTEsWzYsOCwiZCJdLFs2LDYsImQnIl0sWzQsOCwiYyJdLFsyLDgsImIiXSxbMCw4LCJhIl0sWzQsNCwiaF4qZCciXSxbMiwyLCJnXipoXipkJyJdLFswLDAsImZeKmdeKmheKmQnIl0sWzAsMiwiKGdmKV4qaF4qZCciXSxbMCw0LCIoaChnZikpXipkJyJdLFswLDYsIigoaGcpZileKmQnIl0sWzEsMCwiIiwyLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibWFwcyB0byJ9fX1dLFs0LDMsImYiLDJdLFszLDIsImciLDJdLFsyLDAsImgiLDJdLFs3LDYsIlxccGleKmYiXSxbNiw1LCJcXHBpXipnIl0sWzUsMSwiXFxwaV4qIGgiXSxbMTAsNCwiIiwyLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibWFwcyB0byJ9fX1dLFs5LDEwLCJcXGFscGhhXipfe2QnfSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs4LDksIihcXGdhbW1hX3tnZixofSlfe2QnfSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs3LDgsIihcXGdhbW1hX3tmLGd9KV97aF4qIGQnfSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFsxMCwxLCJcXHBpXiooKGhnKWYpIiwyXSxbOSwxLCJcXHBpXiooaChnZikpIiwwLHsibGFiZWxfcG9zaXRpb24iOjQwfV0sWzgsNSwiXFxwaV4qKGdmKSIsMl1d

and so it is the unique factorization of (πœ‹βˆ—β„Ž)(πœ‹βˆ—π‘”)(πœ‹βˆ—π‘“) via the cartesian morphism πœ‹βˆ—((β„Žπ‘”)𝑓). Similarly, the right hand side is constructed by the diagram

c|https://q.uiver.app/#q=WzAsMTIsWzYsOCwiZCJdLFs2LDYsImQnIl0sWzQsOCwiYyJdLFsyLDgsImIiXSxbMCw4LCJhIl0sWzQsNCwiaF4qZCciXSxbMiwyLCJnXipoXipkJyJdLFswLDAsImZeKmdeKmheKmQnIl0sWzAsMiwiZl4qZ14qaF4qZCciXSxbMCw0LCJmXiooaGcpXiogZCciXSxbMCw2LCIoKGhnKWYpXipkJyJdLFsyLDQsIihoZyleKmQnIl0sWzEsMCwiIiwwLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibWFwcyB0byJ9fX1dLFs0LDMsImYiLDJdLFszLDIsImciLDJdLFsyLDAsImgiLDJdLFs1LDEsIlxccGleKiBoIl0sWzYsNSwiXFxwaV4qZyJdLFs3LDYsIlxccGleKmYiXSxbNyw4LCIiLDIseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFs4LDksImZeKlxcZ2FtbWFfe2csZn0iLDJdLFs5LDEwLCJcXGdhbW1hX3tmLGhnfSIsMl0sWzEwLDQsIiIsMSx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1hcHMgdG8ifX19XSxbMTAsMSwiXFxwaV4qKChoZylmKSIsMl0sWzExLDEsIlxccGleKihoZykiLDIseyJsYWJlbF9wb3NpdGlvbiI6NDB9XSxbOSwxMSwiXFxwaV4qZiIsMl0sWzYsMTEsIihcXGdhbW1hX3tnLGh9KV97ZCd9Il0sWzgsNiwiXFxwaV4qZiJdXQ==

so it is must be the same unique factorization. Therefore the hexagon holds.

Now let π‘₯𝑓→𝑦 in 𝖑 and 𝑦′ be an object over 𝑦. The nontrivial path of the left of the unitality coherences reads

π‘“βˆ—πœˆβˆ˜π‘“βˆ—β‡β‡β‡β‡β‡β‡β‡β‡β‡’(1π‘₯)βˆ—π‘“βˆ—π›Ύπ‘₯,𝑓⇐⇐⇐⇐⇐⇐⇐⇒(𝑓1π‘₯)βˆ—πœŒβˆ—βŸΉπ‘“βˆ—:𝖀𝑦→𝖀π‘₯

where 𝜌 is the unique witness that 𝑓1π‘₯ =𝑓 in 𝖑. Then at 𝑦′ this path is constructed from

c|https://q.uiver.app/#q=WzAsOCxbMCw4LCJ4Il0sWzQsOCwieSJdLFswLDYsImZeKiB5JyJdLFs0LDYsInknIl0sWzAsNCwiKGZcXCwxX3gpXip5JyJdLFswLDIsIigxX3gpXiogZl4qIHknIl0sWzAsMCwiZl4qIHknIl0sWzIsMiwiZl4qIHknIl0sWzMsMSwiIiwwLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibWFwcyB0byJ9fX1dLFsyLDAsIiIsMix7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1hcHMgdG8ifX19XSxbMiwzLCJcXHBpXipmIl0sWzQsMiwiXFxyaG9eKl97eSd9IiwyXSxbNSw0LCIoXFxnYW1tYV97eCxmfSlfe3knfSIsMl0sWzYsNSwiXFxudV97Zl4qIHknfSIsMl0sWzQsMywiXFxwaV4qKGYgXFwsIDFfeCkiXSxbNywzLCJcXHBpXipmIl0sWzUsNywiXFxwaV4qMV95IiwyXSxbNiw3LCIiLDAseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFswLDEsImYiLDJdXQ==

so it uniquely factors πœ‹βˆ—π‘“ via the cartesian morphism πœ‹βˆ—π‘“, so it is equal to the trivial path. Similarly, the nontrivial path on the right of the unitality coherences reads

π‘“βˆ—π‘“βˆ—βˆ˜πœˆβ‡β‡β‡β‡β‡β‡β‡β‡β‡’π‘“βˆ—(1𝑦)βˆ—π›Ύπ‘“,𝑦⇐⇐⇐⇐⇐⇐⇒(1𝑦𝑓)βˆ—πœ†βˆ—βŸΉπ‘“βˆ—

where πœ† is the unique witness that 1𝑦 𝑓 =𝑓. Then at 𝑦′ this path is constructed from

c|https://q.uiver.app/#q=WzAsOSxbMCw4LCJ4Il0sWzQsOCwieSJdLFs0LDYsInknIl0sWzAsNiwiZl4qeSciXSxbMCw0LCIoMV95XFwsZileKnknIl0sWzAsMiwiZl4qICgxX3kpXiogeSciXSxbMCwwLCJmXip5JyJdLFsyLDQsIigxX3kpXip5JyJdLFsyLDIsInknIl0sWzAsMSwiZiIsMl0sWzMsMiwiXFxwaV4qZiJdLFsyLDEsIiIsMSx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1hcHMgdG8ifX19XSxbMywwLCIiLDEseyJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJtYXBzIHRvIn19fV0sWzQsMywiXFxsYW1iZGFeKl97eSd9IiwyXSxbNCwyLCJcXHBpXiooMV95IGYpIiwxLHsibGFiZWxfcG9zaXRpb24iOjQwfV0sWzcsMiwiXFxwaV4qMV95Il0sWzUsNywiXFxwaV4qZiJdLFs1LDQsIihcXGdhbW1hX3tmLHl9KV97eSd9IiwyXSxbNiw1LCJmXipcXG51X3t5J30iLDJdLFs4LDcsIlxcbnVfe3knfSJdLFs2LDgsIlxccGleKmYiXSxbMiw4LCIiLDAseyJjdXJ2ZSI6MywibGV2ZWwiOjIsInN0eWxlIjp7ImhlYWQiOnsibmFtZSI6Im5vbmUifX19XV0=

so it uniquely factors 1π‘¦β€²πœ‹βˆ—π‘“ via the cartesian morphism πœ‹βˆ—π‘“, so it is equal to the trivial path.

The Grothendieck construction goes the other way, from 2-functorial families of categories to cartesian fibrations.

See also

#state/develop | #lang/en | #SemBr