Commit 2023-06-20 04:52 86c29aef

refactor(geometry/manifold/cont_mdiff_map): redefine as subtype not structure (#19147) 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.