[Merged by Bors] - refactor(geometry/manifold/cont_mdiff_map): redefine as subtype not structure

[hrmacbeth]

We have a long-running conversation in mathlib about whether function spaces should be implemented as subtypes or as structures. This PR proposes to change cont_mdiff_map, the type of smooth functions between manifolds M and M', from a "structure" implementation to a "subtype" implementation. It honestly seems pretty painless, even though this is a widely used type -- the only change for users is that the field names are now val and property rather than to_fun and cont_mdiff_to_fun.

The motivation is to make it possible to make certain constructions about function spaces generic, so that work for the space of smooth functions can be reused for (for example) the spaces of continuous or differentiable functions.

Notably, in #19146 we introduce a generic construction of a sheaf of functions on a manifold whose object over the open set U is the subtype of functions satisfying a "local invariant property". With this PR, when that construction is applied to the property "smoothness", the resulting sheaf has objects which are by definition the types cont_mdiff_map. They then inherit algebraic structures for free, see #19094.

---

[sgouezel]

I prefer structures in general, but you have a good point here. However, as far as I understand, there is a universe polymorphism issue in #19146, which means that the abstract point of view giving algebraic structures for free will not work in general, so that we will still need to do our constructions by hand. Do you think there is a hope to solve the universe polymorphism? (And then I will be fully convinced by this PR).

[hrmacbeth]

I think my phrase "for free" was ambiguous. I meant that, since we already have algebraic structures on cont_mdiff_map built by hand:
https://leanprover-community.github.io/mathlib_docs/geometry/manifold/algebra/smooth_functions.html
we get them for free on the objects in the sheaf I am building. Here (link to the source code in #19094) is a typical example. Thus, we can upgrade the sheaf-of-types to a sheaf-of-{groups, abelian groups, rings, commutative rings} without much work.

This means that the universe issue with the sheaf construction doesn't have an effect on the rest of the differential geometry library, because the sheaf construction is only used for other sheaf-y things. (It would still be worthwhile to try to fix, of course.)

I have the impression that you were thinking it would go the other way, that some category-theoretic construct would build the algebraic structures on cont_mdiff_map for free. I don't know how to do this!

[urkud]

If we go with leanprover-community/mathlib4#2202 after the port, then we can have both (structure and generic code).

[bors]

✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[hrmacbeth]

I'll wait for @sgouezel's comments before merging because I know he has also thought about this a lot.

Can someone remind me why we prefer structures to subtypes? It's not really clear to me how the BundledHom structure proposed in leanprover-community/mathlib4#2202 is different from subtype.

[urkud]

Having single Subtype.val/Subtype.mk for multiple types is painful in Lean 4 because simp and rw can use different lemmas. It is slightly less painful in Lean 3 but still subtype.val leaks through API here and there. Also, it's hard to extend subtypes and there is no easily readable syntax for the case of multiple properties.

[sgouezel]

I think I would be more happy if the sheaf construction did not output a subtype, but a custom structure. But this kind of refactor would have to happen after the port anyway, so bors d+ also for now.

[jcommelin]

bors d+

[bors]

✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

A downside to this spelling is that you don't have a mk or recursion principle with the right type any more. I suspect this change is going to make things harder in Lean4

[hrmacbeth]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests