Commit 2022-04-05 21:26 a8413617

refactor(topology/vector_bundle): redefine (#13175) The definition of topological vector bundle in #4658 was (inadvertently) a nonstandard definition, which agreed in finite dimension with the usual definition but not in infinite dimension. Specifically, it omitted the compatibility condition that for a vector bundle over B with model fibre F, the transition function B → F ≃L[R] F associated to any pair of trivializations be continuous, with respect to to the norm topology on F →L[R] F. (The transition function is automatically continuous with respect to the topology of pointwise convergence, which is why this works in finite dimension. The discrepancy between these conditions in infinite dimension turns out to be a classic gotcha.) We refactor to add this compatibility condition to the definition of topological vector bundle, and to verify this condition in the existing examples of topological vector bundles (construction via a cocycle, direct sum of vector bundles, tangent bundle).