Construct VectorBundleCore from VectorBundle

Stream: Is there code for X?

[Jack McCarthy]

If I'm given a VectorBundle R F E, is it possible to construct a VectorBundleCore structure from it?

The reason I ask is because many of the theorems in Topology/VectorBundle are actually for VectorBundleCoreinstead of VectorBundle R F E, which makes `VectorBundle not very useful currently. Currently, I am trying to show that if I have a vector bundle, then it's fibres are AddCommGroup (and more generally, an IsTopologicalAddGroup). There is already VectorBundleCore.addCommGroupFiber which is almost what I want, but requires my type to be a VectorBundleCore. Any ideas on how to solve this?

[Sébastien Gouëzel]

It's the other way around: VectorBundleCore is a gadget to construct vector bundles, but not all vector bundles are coming from cores. For your question, by the very definition of a vector bundle the fibers are already AddCommGroup and IsTopologicalAddGroup. Do you have a #mwe so I can understand your question better?

[Jack McCarthy]

I think I just misunderstood my own code lol, apologies for the poorly-worded question