Zulip Chat Archive

Stream: sphere eversion

Topic: Chapter 3 update

Patrick Massot (Jun 13 2022 at 17:14):

There are news about Chapter 3. I decided we should try to take a shortcut. Rather than going through the general vector bundle theory, I half defined a docs#basic_smooth_vector_bundle_core. Here "half" means I defined data but proved nothing. Hopefully that definition is correct (we won't know for sure until we actually prove the lemmas in that file). A basic smooth bundle is a vector bundle over a manifold which is trivial over each coordinate chart of the manifold. This is quite a bit simpler than a general vector bundle, but it is sufficient for all bundles we care about in this project. For instance this shortcut is already used to define the tangent bundle.

Assuming this definition of the 1-jet bundle, I was able to define many things that were blocking progress on Chapter 3. But I didn't prove anything. So there are currently 27 sorries in the project, all Prop, no missing data. So now is a very good time to contribute to the project.

Oliver Nash (Jun 13 2022 at 20:03):

Thanks Patrick! I look forward to starting squash them tomorrow :-)

Oliver Nash (Jun 15 2022 at 09:53):

I admit I started with easy ones but those 27 sorries have now become 23.

Last updated: Dec 20 2023 at 11:08 UTC