Chapter 3 update

Stream: sphere eversion

[Patrick Massot]

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]

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

[Oliver Nash]

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