mathlib

f7ebde7e - refactor(topology/vector_bundle/hom): fibres of hom-bundle carry strong topology (#19107)

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 Co-authored-by: Moritz Doll <moritz.doll@googlemail.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>