Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-02 15:55 cf6f27ee

View on Github →

refactor(topology/{fiber_bundle, vector_bundle}): make trivializations data rather than an existential (#13052) Previously, the construction topological_vector_bundle was a mixin requiring the existence of a suitable trivialization at each point. Change this to a class with data: a choice of trivialization at each point. This has no effect on the mathematics, but it is necessary for the forthcoming refactor in which a further condition is imposed on the mutual compatibility of the trivializations. Furthermore, attach to topological_vector_bundle and to two other constructions topological_fiber_prebundle, topological_vector_prebundle a further piece of data: an atlas of "good" trivializations. This is not really mathematically necessary, since you could always take the atlas of "good" trivializations to be simply the set of canonical trivializations at each point in the manifold. But sometimes one naturally has this larger "good" class and it's convenient to be able to access it. The charted_space definition in the manifolds library does something similar.

Estimated changes