# Commit 2023-05-28 14:55 f7ebde7e

View on Github →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