Commit 2020-09-04 11:49 7c9a86d4

refactor(geometry/manifold): use a sigma type for the total space of the tangent bundle (#3966) Redefine the total space of the tangent bundle to be a sigma type instead of a product type. Before

have p : tangent_bundle I M := sorry,
rcases p with ⟨x, v⟩,
-- x: M
-- v: E

After

have p : tangent_bundle I M := sorry,
rcases p with ⟨x, v⟩,
-- x: M
-- v: tangent_space I x

This seems more natural, and is probably needed to do Riemannian manifolds right. The drawback is that we can not abuse identifications any more between the tangent bundle to a vector space and a product space (but we can still identify the tangent space with the vector space itself, which is the most important thing).