Commit 2022-11-09 00:14 433802f7
View on Github →refactor(topology/vector_bundle/basic): deduplicate trivialization
(#17359)
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 pretrivialization
.
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 mem_trivialization_atlas
.