Fibre Bundle

A fibre bundle is a Bundle where every Fibre is Isomorphic in some coherent way to a standard fibre.

More concretely, let $p:E\to B$ be a Bundle in a Category $\mathcal{C}$ with a Terminal Object $1:\mathcal{C}$. We say that $p$ is a fibre bundle if for every Global Element $b:\mathcal{C}(1,B)$, the pullback of $p$ along $b$ is isomorphic to $F$.

More generally, let $\mathcal{E}\to\mathcal{B}$ be a Cartesian Fibration over a category with a Terminal Object. An object $E:\mathcal{E}_{B}$ is a fibre bundle with standard fibre $F:\mathcal{E}_{1}$ if for every Global Element $b:\mathcal{B}(1,B)$, there is a Cartesian Morphism $f_{b}:{{F}\to_{b}{E}}$.

Properties

• An object $E\rightarrowtriangle B$ is a fibre bundle with standard fibre $F$ if and only if for all Global Elements $b:{{}(1,B)}$, the base change $b^{*}(E)\rightarrowtriangle 1$ is Vertically Isomorphic to $F$.

  For the forward direction, suppose that the base change $b^{*}(E)\rightarrowtriangle 1$ is vertically isomorphic to $F$. Every invertible map is cartesian, the projection $\pi^{*}:{{}_{b}(b^{*}(E),E)}$ is cartesian, and cartesian maps are closed under composition, so there is a cartesian map ${{}_{b}(F,E)}$.

  Conversely, suppose that there is a cartesian morphism $f_{b}:{{}_{b}(F,E)}$ for every global element $b$. The map $\pi^{*}:{{}_{b}(b^{*}(E),E)}$ is cartesian, so we must have a vertical isomorphism $F\cong_{mathrm{id}{ifx..lse\par i}}b^{*}(E)$.

Questions

• There is a striking similarity with fibre bundles and Indexed Polynomial Functors; if we draw the trivial let $F\rightarrowtriangle 1$, we get a diagram

  $1\leftarrowtriangle F\xrightarrow{f_{b}}E\rightarrowtriangle B$

  where the middle leg consists of a ${{1}\to{B}}$ indexed family of maps rather than a single map. Perhaps this has something to do with the Double Category of Bridges?