Zulip Chat Archive

Stream: maths

Topic: trivialization of fiber bundles over intervals


view this post on Zulip Yury G. Kudryashov (Mar 09 2021 at 13:56):

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

view this post on Zulip Kevin Buzzard (Mar 09 2021 at 14:28):

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

view this post on Zulip Sebastien Gouezel (Mar 09 2021 at 14:36):

contractible spaces rather, no?

view this post on Zulip Kevin Buzzard (Mar 09 2021 at 16:01):

probably -- I'm no topologist.

view this post on Zulip Kevin Buzzard (Mar 09 2021 at 16:06):

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?

view this post on Zulip Sebastien Gouezel (Mar 09 2021 at 16:10):

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.

view this post on Zulip Sebastien Gouezel (Mar 09 2021 at 16:11):

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).

view this post on Zulip Yury G. Kudryashov (Mar 09 2021 at 16:51):

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

view this post on Zulip Yury G. Kudryashov (Mar 09 2021 at 16:52):

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

view this post on Zulip Yury G. Kudryashov (Mar 09 2021 at 18:37):

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.

view this post on Zulip Yury G. Kudryashov (Mar 09 2021 at 18:38):

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.

view this post on Zulip Oliver Nash (Mar 09 2021 at 19:15):

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

view this post on Zulip Oliver Nash (Mar 09 2021 at 19:15):

(or more precisely, being developed further)

view this post on Zulip Sebastien Gouezel (Mar 09 2021 at 20:58):

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.


Last updated: May 09 2021 at 09:11 UTC