Closed hrmacbeth closed 1 year ago
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).
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!
If we go with leanprover-community/mathlib4#2202 after the port, then we can have both (structure and generic code).
:v: 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.
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 https://github.com/leanprover-community/mathlib4/issues/2202 is different from subtype
.
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.
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.
bors d+
:v: 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.
bors r+
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.
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 manifoldsM
andM'
, 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 nowval
andproperty
rather thanto_fun
andcont_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 typescont_mdiff_map
. They then inherit algebraic structures for free, see #19094.