trivialization of fiber bundles over intervals

Stream: maths

[Yury G. Kudryashov]

branch#local-equiv-piecewise has a proof of the fact that any topological fiber bundle over [a, b] is trivializable.

[Kevin Buzzard]

Oh nice! This is a key step towards proving an analogous result for simply connected spaces, right?

[Sebastien Gouezel]

contractible spaces rather, no?

[Kevin Buzzard]

probably -- I'm no topologist.

[Kevin Buzzard]

The ones with no pi_1. Do you know that in 2018 an undergraduate at Imperial, @Luca Gerolla , formalised the theory of fundamental groups of a pointed space. It was much harder than I had expected, but he is a smart kid and he battled through -- I remember Mario helping him a lot with things like f being continuous on [a,b] iff it was continuous on [a,c] and [c,b] with the two values at c coinciding. Here's a link to a very very old Lean file where pi_1 is defined. Do we have this in mathlib?

[Sebastien Gouezel]

You can have spaces with no pi_1 but still with nontrivial fiber bundles, since the nontriviality can come from higher homotopy groups. For instance, the tangent bundle to the 2-sphere is nontrivial.

[Sebastien Gouezel]

And I don't think we have the fundamental group in mathlib. There was a PR by Kenny a long time ago, but I think Reid said it wasn't done in the right generality (which is probably true, I don't know anything about this stuff).

[Yury G. Kudryashov]

My plan is to define the index of a continuous map $f : S^1\to S^1$ and have some sort of Rouché's Theorem.

[Yury G. Kudryashov]

(and an alternative proof of the fact that complex numbers are algebraically closed).

[Yury G. Kudryashov]

It seems that we'll need a refactor of fiber bundles in mathlib. I think that they should be done similarly to charted spaces, possibly extending [charted_space (B × F) Z]. This way we'll be able to bring has_groupoid from manifolds and speak about, e.g., vector bundles, C^r bundles etc.

[Yury G. Kudryashov]

But I'm not going to do it in the next few weeks. I have quite a few unfinished PRs, I'll try to get them finished&merged.

[Oliver Nash]

I have nothing to add for now except to say that I'm very excited at the prospect of fiber bundles arriving.

[Oliver Nash]

(or more precisely, being developed further)

[Sebastien Gouezel]

Yury G. Kudryashov said:

It seems that we'll need a refactor of fiber bundles in mathlib. I think that they should be done similarly to charted spaces, possibly extending [charted_space (B × F) Z]. This way we'll be able to bring has_groupoid from manifolds and speak about, e.g., vector bundles, C^r bundles etc.

There are two different things here.

From the topological point of view, saying that we have a fiber bundle, or a topological vector bundle, or whatever, is just Prop, on top of already existing typeclasses. Since there is no data in there, I don't think we should put any artifical data in the definition, it would just be calling for diamonds uselessly. I have just completed the PR #4658 by @Nicolò Cavalleri in which he implements topological vector bundles, and it seems to work pretty well.

On the other hand, when you want to deal with smoothness, then you definitely need data, and then it should be implemented with a charted_space instance, and expressed as the fact that the charts respect the groupoid of maps which are, say, smooth in one direction and linear in the other one. The formalism was designed to allow this kind of things, this is definitely desirable, and it hasn't been done yet.