Commit 2023-05-28 14:55 f7ebde7e

refactor(topology/vector_bundle/hom): fibres of hom-bundle carry strong topology (#19107) Currently, the "hom-bundle" between two vector bundles E₁ and E₂ has fibre over x which is a type synonym of E₁ x →SL[σ] E₂ x, but which carries a topology produced by the hom-bundle construction (using the identification by trivializations withe the model fibre F₁ →SL[σ] F₂). This was needed when this bundle was made (#14541) because at that time, F₁ →SL[σ] F₂ (continuous linear maps between normed spaces) carried a topology in mathlib but E₁ x →SL[σ] E₂ x (continuous linear maps between topological vector spaces) did not. As of #16053, continuous linear maps between topological vector spaces do carry a topology, the strong topology. So we can kill the old topology on the type synonym and just use the default one, which should avoid annoying issues later. A few minor changes are needed to make this go through:

• we revert #14377: the question is whether the "vector prebundle" construction, whose canonical use is for the hom-bundle, should or should not require a topology on the fibres. Now that in applications it could happen either way (fibres do or don't come with a topology), it will be more convenient to assume that they do carry a topology, and put the "artificial" topology on the fibres if they happen to not.
• some assumptions need to change from [add_comm_monoid] to [add_comm_group], this is mathematically harmless since they are also modules over a field.
• generalize the construction continuous_linear_equiv.arrow_congrSL from normed spaces to topological vector spaces