Smooth vector bundles

Stream: maths

[Heather Macbeth]

@Floris van Doorn and I have been working out a proposed definition of smooth vector bundles, and we would like to ask for comments. Our branch (still with many sorries) is branch#smooth-vector-bundle, and links go to declarations in that branch. We have tested it as far as the construction of the smooth manifold structure on a smooth vector bundle, and everything is designed to make this proof-of-concept and its variants work well.

"Smooth vector bundle" to be a Prop typeclass on top of "topological vector bundle"

Let E be a topological vector bundle, with model fibre F and base space B. We would like to consider E as carrying a charted space structure given by its trivializations -- these are charts to B × F. Then, by "composition", if B is itself a charted space over H (e.g. a smooth manifold), then E is also a charted space over H × F.

Now, we define "smooth vector bundle" as the Prop of having smooth transition functions. We introduce the structure groupoid on B × F consisting of smooth, fibrewise linear local homeomorphisms, show that our definition of "smooth vector bundle" implies has_groupoid for this groupoid, and show (by a "composition" of has_groupoid instances) that this means that a smooth vector bundle is a smooth manifold. This idea is at least implicit in @Sebastien Gouezel's docs for charted spaces, and I believe it was a use case he already envisaged.

Since smooth_vector_bundle is a Prop, it is easy to make variants and for many such variants to coexist -- vector bundles can be smooth vector bundles over several different base fields, they can also be C^k vector bundles, etc.

Refactor of topological vector and fiber bundles

The linter will complain about one step in the above construction: having a topological vector bundle naturally be a charted space over B × F. This is because when looking for that charted space instance, Lean would need to find the scalar field for the topological vector bundle itself.

We propose to solve this by introducing a data-carrying gadget (currently we call it fiber_bundle) which is mathematically the same as the current Prop typeclass is_topological_fiber_bundle, but which carries a fixed family of preferred trivializations and choice of trivialization at each basepoint, not just the Prop that a trivialization exists at each basepoint.

An analogy is that you can consider a topological manifold as being either a Prop -- the existence of a local homeomorphism to R^n at each point -- or as data -- a docs#charted_space modelled on R^n.

For vector bundles, one needs the data-carrying version, because of the subtlety in infinite dimension which came up in March. We are proposing moving this data to fiber_bundle, and then having is_vector_bundle be a Prop on top of that (consisting of assumptions that certain maps are linear and continuous).

This solves the dangerous instance problem for the B × F-charted space structure on a vector bundle: it is actually now a B × F-charted space structure on a fiber bundle, so Lean doesn't have to guess the scalar field.

Incidentally, it improves a couple of other minor annoyances with topological vector bundles:

• docs#topological_vector_bundle.continuous_proj doesn't require you to help Lean guess the field
• deduplication of docs#topological_fiber_bundle.trivialization and docs#topological_vector_bundle.trivialization

There is the question of whether the new fiber_bundle should coexist with is_[topological_]fiber_bundle, or replace it. We propose a full replacement but either way would work for our purposes.

[Sebastien Gouezel]

Thanks for doing this! Since the moment you have noticed that data was necessary to define vector bundles in general, I knew we would have to do something along these lines, and I'm really glad you are doing it. I would replace completely is_topological_fiber_bundle with the new construction: it is not surprising that the first implementation of this kind of notion hasn't found the right setting (just as what has happened for schemes, or the integral), so I think we shouldn't keep a technological debt based on this random first implementation, and we should just throw it away.

[Kevin Buzzard]

This attitude is what I think sets us apart from the other provers, in fact.

[Patrick Massot]

Kevin, I don't think this is true. I think the odd order project featured massive refactors.

[Kevin Buzzard]

Yes I'm sure you're right about the big projects in the other provers. But this is happening for us in general.

[Heather Macbeth]

Thanks for the prompt comments, Sébastien. OK ... if no one else objects, it will be out with the old fibre bundles, in with the new!

[Heather Macbeth]

In fact, we have another proposed change to the definition of fibre bundle, which I forgot to mention. (This is separate from the data/Prop decision.). Currently:
docs#is_topological_fiber_bundle
any topological space Z can be a fibre bundle: you provide a map proj : Z → B where B is the base space. So, for example, $S^3$ could be a fibre bundle over $S^2$. In our new definition:
https://github.com/leanprover-community/mathlib/blob/819ce68cbcab787cf901093b2bebc746fd60209f/src/topology/new_fiber_bundle.lean#L427
we're proposing that only spaces of the form bundle.total_space E (which is a type synonym for a sigma-type Σ (x : B), E x) can be fibre bundles. Thus the fibre structure is "baked in" definitionally.

This is already the choice made for vector bundles, so it has the advantage of consistency. There is, of course, a loss of expressivity. Does anyone object?

[Johan Commelin]

Is the reason that this choice was made for vector bundles documented somewhere?

[Heather Macbeth]

Yes, in fact I'm just trying to track down the previous Zulip discussions.

[Johan Commelin]

I feel like I'm not in a position to object. Because I haven't explored the design space at all. But intuitively, it seems like we should try to make it possible to let S³ be a fibre bundle over S².

[Heather Macbeth]

The most relevant discussion I found is in a previous version of the module docstring of topology/vector_bundle, written by @Nicolò Cavalleri and @Sebastien Gouezel in #4658.

Let B be the base space. In our formalism, a topological vector bundle is by definition the type
bundle.total_space E where E : B → Type* is a function associating to
x : B the fiber over x. This type bundle.total_space E is just a type synonym for
Σ (x : B), E x, with the interest that one can put another topology than on Σ (x : B), E x which has the disjoint union topology.
...
The point of this formalism is that it is unbundled in the sense that the total space of the bundle
is a type with a topology, with which one can work or put further structure, and still one can
perform operations on topological vector bundles (which are yet to be formalized).

[Heather Macbeth]

But some of the considerations mentioned in the same docstring turned out not to work (e.g., the idea to make topological_vector_bundle a Prop), so I can't tell whether the decision there should still guide us. And anyway, I found an opposite opinion from @Sebastien Gouezel and @Reid Barton from a year before that, saying that we shouldn't make this simplification :)

[Sebastien Gouezel]

The possibility to have S^3 as a fiber bundle over S^2 was indeed the motivation for the initial definition. But with the experience we have now, I am very strongly in favor of the change where we only allow sigma types. The reason is that you can register typeclasses on the fibers of a sigma type in a nice way (because the fibers are types themselves), while it is way less natural in a more general context (the fibers are some random sets of the form p^{-1} {x}). We were able to do it, at the expense of quite suffering, for fiber bundles, but when we started with more structure like vector bundles this just became a nightmare. While everything works very smoothly with sigma types.

[Sebastien Gouezel]

So I've changed my mind compared to my previous opposite opinion, thanks to time and experimentation.

[Heather Macbeth]

Sebastien Gouezel said:

The reason is that you can register typeclasses on the fibers of a sigma type in a nice way (because the fibers are types themselves), while it is way less natural in a more general context (the fibers are some random sets of the form p^{-1} {x}).

Thanks, this is clearly the important point, and I will make sure it features prominently in any new module docstring!

[Heather Macbeth]

Perhaps this is rather similar to the discussion of direct sums of vector spaces: we first built a good theory of the external direct sum and only much later started thinking about how to cleanly express internal direct sums.

[Scott Morrison]

Perhaps include that analogy in the doc-strings: it is thoroughly convincing to me. (I guess it's not even an analogy, but a "special case", if not formally.)

[Heather Macbeth]

We have opened the first PRs towards smooth vector bundles: #17291, #17302, #17305, #17359. Of these, #17359 is the biggest bottleneck: it is the first step in the proposed refactor of topological vector bundles.

[Heather Macbeth]

#17505 for the refactor of topological fiber and vector bundles.

[Floris van Doorn]

It took a while, but the vector bundle refactor is complete!

Smooth vector bundles were added to mathlib in #17611, #17680 and #18601, and since today the sphere eversion project also uses the new definition of smooth vector bundles.

There are still some minor pain points, but working with the new definition is a lot smoother (:smirk:) overall!

[Kevin Buzzard]

That's great! How far are we from being able to do linear algebra with vector bundles? Can I make the cotangent space of a manifold yet (I need to take the homs between two vector bundles).

[Sebastien Gouezel]

We can already do that, thanks to docs#bundle.continuous_linear_map.vector_bundle, but I don't think we have registered yet that this will be smooth. (But this should be pretty straightforward!)

[Sebastien Gouezel]

(Look at the number of typeclass arguments in this example, this is both frightening and unavoidable, I think -- especially if we want to state things in terms of semilinear maps with respect to possibly different fields)

[Patrick Massot]

https://github.com/leanprover-community/sphere-eversion/blob/7d35fe756cc7fd5fcbffde0e1d8cd6d5347ba2db/src/to_mathlib/geometry/manifold/vector_bundle/misc.lean#L403-L405

[Floris van Doorn]

I'll be PRing more material from sphere eversion to mathlib next week, so we'll have cotangent bundles there soon.

[Floris van Doorn]

Note: I currently only did the hom bundle as a smooth bundle for linear maps, not for arbitrary semilinear maps. I don't know how to generalize it: the base space has to be also modelled by a vector space over some field, and things don't type-check when using 2 or 3 different fields. Perhaps this could work if we generalize docs#smooth_vector_bundle to depend on 2 fields: the field over which the fiber F is a vector space, and the field over which EB (used to model the base space) is a vector field. I'm not sure if that is worth it though.

[Kevin Buzzard]

@Kyle Miller can you do anything about the frightening typeclass arguments once they're ported?

[Sebastien Gouezel]

Floris van Doorn said:

I'm not sure if that is worth it though.

I'm not sure either. Antilinear maps over complex bundles might be useful, though, so maybe we should do just one field but allowing semilinear maps over this one field.