Commit 2022-11-09 00:14 433802f7View on Github →
Currently, in mathlib, there is a structure
topological_vector_bundle.trivialization which extends another structure
topological_fibre_bundle.trivialization by a linearity hypothesis. We change this to a single structure
trivialization (no namespace), together with a mixin class
trivialization.is_linear. This is the first step in the planned vector bundle refactor: it will allow all the data of a vector bundle to be held at the level of fibre bundles, so that there can be a non-"dangerous instance"
charted_space instance associated to a vector bundle.
The analogous change is made for
The most awkward aspect of this refactor is that one would want the linearity of trivializations associated to a vector bundle to be "automatic", which effectively means that one wants a
trivialization.is_linear instance to be found by typeclass inference for trivializations in the
trivialization_atlas of a vector bundle. For this to work, the property of belonging to the trivialization atlas also needs to be made into a Prop typeclass. We call this typeclass