ContMDiffFiberBundle

Stream: Is there code for X?

[Dominic Steinitz]

We have ContMDiffVectorBundle but I don't think there is even Mathlib.Geometry.Manifold.FiberBundle.

[Sébastien Gouëzel]

docs#VectorBundle

[Sébastien Gouëzel]

Oops, I misread, sorry. What definition are you thinking of?

[Sébastien Gouëzel]

We have docs#FiberBundle.chartedSpace which gives a manifold structure on fiber bundles.

[Dominic Steinitz]

I have used that - see here: #Geographic locality > London, England @ 💬 - what I'd like is the fiber equivalent of class ContMDiffVectorBundle - https://github.com/leanprover-community/mathlib4/blob/v4.19.0/Mathlib/Geometry/Manifold/VectorBundle/Basic.lean#L265

[Dominic Steinitz]

The fibres for the hopf fibration are not vector spaces - I know they are for the Mobius strip.

[Kevin Buzzard]

It's only recently that I learnt that differential geometers apparently think the Moebius strip is infinite, and not just a sheaf of $(-1,1)$'s over the circle.