Commit 2022-11-15 22:05 b8c810e2

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.