Fibres and fibre bundles are an important mathematical structure that occurs across many branches of maths. Therefore there are many ways to approach this subject:
- Topology and Open Sets.
- Set Theory - On these pages we discuss how reversing a surjective map generates this structure.
- Type Theory - On these pages we look at this structure as a type family or a disjoint set of types indexed by another type.
- Category Theory
Fibre Bundle as Dependent Type
In type theory dependent types are where there is a family of types indexed by elements of another type.
More about this relation to type theory on the page here.
A fibre as a projection.
The simple case on the right is intended to show a projection of a three dimensional object onto a two dimensional surface. This is just a projection from a product space.
However a projection along a fibre is more general than that, locally it still looks like a product space, but globally it can look very different.
A standard example of this is a spiral, which can be projected onto a circle since any local section corresponds to a section of a circle. Locally a section of the spiral looks like a section of the circle, globally the circle and the spiral are different.
To reverse the direction of this projection we have to create a set (type) of points.
|A similar example is the Möbius band being mapped onto a cylinder.|
Fibrations of Graphs
theory: topological graph theory
|undirected graph:||covering projection|
|directed graph:||fibration (weaker form of covering projection)|
Here is an example for directed multigraphs.
Each node in the top graph maps to the bottom graph (fibration). The corresponding node always has the same number and colour of incoming arcs (but not necessarily outgoing arcs).
This gives some sort of local invariance.