# 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`

.