# Commit 2022-11-15 22:05 b8c810e2

View on Github →refactor(topology/{fiber,vector}_bundle): make `vector_bundle`

a mixin (#17505)
Previously, `is_fiber_bundle`

* was a propositional typeclass on a function `p : Z → B`

, stating the existence of local trivializations covering `Z`

. Then `vector_bundle`

* was a class with data on a type `E : X → Type*`

(with the projection from `Σ x : B, E x`

to `B`

playing the role of `p`

), giving a fixed atlas of fibrewise-linear local trivializations.
We change this definition so that
(i) the data is all held in `fiber_bundle`

, with `vector_bundle`

a mixin stating fibrewise-linearity
(ii) only sigma-types can be fiber bundles, not general topological spaces
This allows bundles to carry instances of typeclasses in which the scalar field, `R`

, does not appear as a parameter. Notably, we would like a vector bundle over `R`

with fibre `F`

over base `B`

to be a `charted_space (B × F)`

, with the trivializations providing the charts. This would be a dangerous instance for typeclass inference, because `R`

does not appear as a parameter in `charted_space (B × F)`

. But if the data of the trivializations is held in `fiber_bundle`

, then a *fibre* bundle with fibre `F`

over base `B`

can be a `charted_space (B × F)`

, and this is safe for typeclass inference.
We expect that this refector will also streamline constructions of fibre bundles with similar underlying structure (e.g., the same bundle being both a real and complex vector bundle).
Here is the relevant Zulip discussion.
*We take the opportunity to rename `topological_{fiber,vector}_bundle`

to `{fiber,vector}_bundle`

, since in the upcoming definition of smooth bundles, smoothness will be another mixin for `fiber_bundle`

.