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(topology/sheaves/stalks): Generalize from Type to algebraic categories #9357
Conversation
transitivity, | ||
swap, | ||
exact colimit.pre _ (open_nhds.map f x).op, | ||
exact colim.map (whisker_right (nat_trans.op (open_nhds.inclusion_map_iso f x).inv) F), |
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.
A slighter terser hack:
transitivity, | |
swap, | |
exact colimit.pre _ (open_nhds.map f x).op, | |
exact colim.map (whisker_right (nat_trans.op (open_nhds.inclusion_map_iso f x).inv) F), | |
refine _ ≫ colimit.pre _ (open_nhds.map f x).op, | |
exact colim.map (whisker_right (nat_trans.op (open_nhds.inclusion_map_iso f x).inv) F), |
I'll think some more about what's going on here.
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.
Haha... I had forgotten that I wrote this, and you're just moving it around now. :-) Stet, I guess.
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.
Refactoring 2-year-old hacks is outside the scope of this PR ;)
I never really deciphered what's going on here. Maybe I'm going to try as well, just for fun.
🎉 I'm really happy to see this generalization work! |
bors merge |
…gories (#9357) Previously, basic lemmas about stalks like `germ_exist` and `section_ext` were only available for `Type`-valued (pre)sheaves. This PR generalizes these to (pre)sheaves valued in any concrete category where the forgetful functor preserves filtered colimits, which includes most algebraic categories like `Group` and `CommRing`. For the statements about stalks maps, we additionally assume that the forgetful functor reflects isomorphisms and preserves limits.
Pull request successfully merged into master. Build succeeded:
|
Previously, basic lemmas about stalks like
germ_exist
andsection_ext
were only available forType
-valued (pre)sheaves. This PR generalizes these to (pre)sheaves valued in any concrete category where the forgetful functor preserves filtered colimits, which includes most algebraic categories likeGroup
andCommRing
. For the statements about stalks maps, we additionally assume that the forgetful functor reflects isomorphisms and preserves limits.The diff might be a little hard to read, as I moved some stuff around. Generally, the lower in the file, the more assumptions on the category on
C
are introduced.