[Merged by Bors] - feat: structure sheaf of a manifold #7332
Conversation
hrmacbeth
added
awaiting-review
There was a problem hiding this comment.
Just a few nitpicks: let's get this merged!
I also looked over the conversation at leanprover-community/mathlib#19094 and I note that there is nothing pending from there (except the declared-out-of-scope approach of "interpreting Lawvere theories in categories with finite products" to avoid repetition).
bors d+
| obstacle here is in the underlying category theory constructions, and there is WIP (as of June 2023) | ||
| to fix this. See | ||
| https://github.com/leanprover-community/mathlib/pull/19153 | ||
| and cross-references there. |
There was a problem hiding this comment.
It would be nice to give a bit more detail here.
I looked at leanprover-community/mathlib#19153 and there are some useful references but I didn't really feel this enhanced my understanding beyond "some parts of the category theory library are probably not sufficiently universe polymorphic".
There was a problem hiding this comment.
a7d51dd updates to what I think is the current status here. @semorrison Could you look at that diff to see whether it's an accurate description?
edit: ignore the incorrect year on that diff -- I have fixed it now!
|
✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
|
To fix the (this is to enable/work around the heuristics of
See: b69521d |
Co-authored-by: Oliver Nash <github@olivernash.org>
|
bors r+ |
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>
|
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. |
bors
bot
changed the title
In leanprover-community/mathlib#19146, we defined
StructureGroupoid.LocalInvariantProp.sheaf, the sheaf-of-types of functionsf : M → M'(for charted spacesM,M') satisfying some local property in the sense ofStructureGroupoid.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 ifM'is an abelian Lie group, and a sheaf of rings ifM'is a "smooth ring".Co-authored-by: Adam Topaz github@adamtopaz.com
This PR replaces the mathlib3 PR leanprover-community/mathlib#19094, which I will now close.
A few things had to be manually to-additivized (and had not needed to be in Lean 3), expert help welcome!fixed by Floris