mathlib

b8c810e2 - refactor(topology/{fiber,vector}_bundle): make `vector_bundle` a mixin (#17505)

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](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Smooth.20vector.20bundles/near/306023372) 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`. Co-authored-by: Floris van Doorn [fpvdoorn@gmail.com](mailto:fpvdoorn@gmail.com)