-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(geometry/manifold/sheaf/basic): sheaf of functions satisfying a local_invariant_prop
#19146
Conversation
import geometry.manifold.local_invariant_properties | ||
import topology.sheaves.local_predicate | ||
|
||
/-! # Generic construction of a sheaf from a `local_invariant_prop` on a manifold -/ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you expand this docstring, by describing the main definition and what it constructs?
Do I understand correctly that this is not universe-polymorphic (i.e., M
and M'
need to be in the same universe). Isn't that a problem for concrete applications?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I wrote a module docstring and I opened
https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2319146.20sheaves.20on.20manifolds
to solicit help with the universe issue.
…tructure (#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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
bors d+
✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
bors r+ |
…`local_invariant_prop` (#19146) Define `structure_groupoid.local_invariant_prop.sheaf`, the sheaf-of-types of functions `f : M → M'` (for charted spaces `M`, `M'`) satisfying some local property in the sense of `structure_groupoid.local_invariant_prop` (for example continuity, differentiability, smoothness).
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. If you want to switch to GitHub's built-in merge queue, visit their help page. |
local_invariant_prop
local_invariant_prop
In leanprover-community/mathlib#19146, we defined `StructureGroupoid.LocalInvariantProp.sheaf`, the sheaf-of-types of functions `f : M → M'` (for charted spaces `M`, `M'`) satisfying some local property in the sense of `StructureGroupoid.LocalInvariantProp` (for example continuity, differentiability, smoothness). In this PR, in the case of smoothness, we upgrade this to a sheaf of groups if `M'` is a Lie group, a sheaf of abelian groups if `M'` is an abelian Lie group, and a sheaf of rings if `M'` is a "smooth ring". Co-authored-by: Adam Topaz <github@adamtopaz.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Define
structure_groupoid.local_invariant_prop.sheaf
, the sheaf-of-types of functionsf : M → M'
(for charted spacesM
,M'
) satisfying some local property in the sense ofstructure_groupoid.local_invariant_prop
(for example continuity, differentiability, smoothness).