feat(data/equiv/local_equiv): define local equivalences

[sgouezel]

This files defines equivalences between subsets of given types.

An element e of local_equiv α β is made of two maps e.to_fun and e.inv_fun respectively
from α to β and from β to α (just like equivs), which are inverse to each other on the subsets
e.source and e.target of respectively α and β.

They are designed in particular to define charts on manifolds.

The main functionality is e.trans f, which composes the two local equivalences by restricting
the source and target to the maximal set where the composition makes sense.

More details on motivation and implementation in the header of the file.

I am not completely sure on where to put the file, as pequiv.lean is just in data. It seemed more natural to me to use data.equiv.

This is the first PR of a series adding manifolds to mathlib. A branch containing the forthcoming developments is available at https://github.com/sgouezel/mathlib/tree/manifold9, including the following files:

• src/topology/local_homeomorph: local homeomorphisms (just like local equivs, but with open source and target, and continuous functions between them).
• geometry/manifold/fiber_bundle: fiber bundles (where the fiber is a topological space, the base is a topological space, and local trivializations are formulated using local homeos). Useful to define the tangent bundle later on.
• geometry/manifold/manifold: define a manifold modelled on a general topological space (where the charts are given by local homeos). Define groupoids of local homeos, and specify what it means for a manifold to have this groupoid as structure groupoid.
  *geometry/manifold/smooth_manifold_with_boundary: as a particular case of manifolds, define smooth manifolds with boundary, where the model space is a normed vector space (or a nice subset of such a vector space, for instance a half space), where the coordinate changes are smooth.
  *geometry/manifold/basic_smooth_bundle: define a specific kind of smooth vector bundles over a smooth manifold (the bundle should be trivial in the charts of the manifold), and use this machinery to define the tangent bundle (applications to differential forms or riemannian metrics should be easy, but are not done yet), as a smooth manifold.
  *geometry/manifold/mderiv.lean: the differential of a map between manifolds, as a map between tangent spaces. Follows the API for derivatives (and is defeq to the standard derivative when the manifold is a vector space, as it should be -- to get this was an important guidance in the choice of definitions).

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[semorrison]

I like this "table" layout for ## Main definitions. Maybe we should add advice to use it to the doc guidelines!

[semorrison]

Looks lovely!

[PatrickMassot]

LGTM. It looks pretty similar to what I started in https://github.com/PatrickMassot/lean-differential-topology/blob/master/src/pequiv.lean (with the very same goal of defining manifolds) before I got sucked into perfectoid spaces. Let's hope it means this is a natural thing to do...

[jcommelin]

First of all, thanks a lot for this gigantic effort that you are undertaking.
One thing I regret is that you have to type .to_fun all the time. Maybe coercions are broken. That only makes it more sad... It reduces conciseness and readability in my eyes.

[sgouezel]

I agree.

I once had a working version with coercions, but it created all types of problems in manifolds (probably because there are outparams, and coercions can only fire if the type is known, i.e., if all outparams have already been resolved, but this is not possible if the coercion has not already fired up to make sense of the whole expression -- well, this is the impression I got). I ended up adding type annotations everywhere, and it reduced conciseness and readability even much more...

I have to say one gets used to to_fun and inv_fun (in fact, inv_fun is not bad because one writes e.inv_fun instead of e.symm, which is comparable).

[fpvandoorn]

This looks really good! I'm excited to get manifolds in mathlib.