[Merged by Bors] - feat(topology/sheaves/skyscraper): define skyscraper presheaves and calculate stalks #15934

jjaassoonn · 2022-08-08T15:21:52Z

alreadydone

Will take a closer look later!

src/topology/sheaves/skyscraper.lean

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

src/topology/sheaves/skyscraper.lean

alreadydone · 2022-08-22T17:41:08Z

src/topology/sheaves/skyscraper.lean

+point, then the skyscraper sheaf `𝓕` with value `A` is defined by `U ↦ A` if `p₀ ∈ U` and
+`U ↦ *` if `p₀ ∉ A` where `*` is some terminal object.
+-/
+def skyscraper_sheaf : sheaf C X :=


You can probably get a shorter proof using Top.presheaf.is_sheaf_iff_is_sheaf_opens_le_cover. I might try to golf the other proofs later.

I think the universe level for Top.presheaf.is_sheaf_iff_is_sheaf_opens_le_cover is too small

Though, it might not be useful to keep skyscraper_presheaf universe level depending on three universe levels u, v, w, because to calculate stalks, universe level needs to be restricted anyway.

Oh yes, but I would try to generalize the universe there. It's also better to fix the universe level of Top.presheaf to the (identical) Type (max w v u).

You might also generalize universe for stalk by using has_limits_of_size C as assumption.

opens_le_cover generalized at #16214.

Yes. I think you are right. So I think it makes sense to define Godement resolution in terms of skyscraper (no matter the explicit description or pushforward definition) so that
$$\mathcal{F} \to \prod_{x}\mathrm{Sky}(\mathcal{F}_x) \to \prod_x\mathrm{Sky}(\mathcal I_x)$$
can be easily shown to be a monomorphism into an Injective sheaf. ($\mathcal{I}_x$ comes from enough invectiveness and $\mathcal{F}_x$)

Yeah, so let's figure out which definition is the easiest to work with to show monomorphism. I think you meant to write Sky(I_x) instead of I_x? It should be easy to show the pushforward of a mono is a mono, using the fact that a (pre)sheaf morphism is mono iff it's a mono on every open (this is stated in Stacks for Set-valued (pre)sheaves, but presumably holds more generally (also for functor categories)?).

As for the first map being mono, it's also enough to use the stalk-skyscraper adjunction. Two morphisms G→F agree after composing with the unit F→Sky_x(F_x) iff the corresponding morphisms G_x→F_x under the adjunction agree, so it suffices to use the fact that a sheaf morphism is determined by the induced morphisms on stalks. This doesn't work for presheaves though; I assume the original proof also doesn't?

An independent issue: I think the docstring here is problematic, because the skyscraper may have nonzero (non-terminal) stalks at points other than p0, so it may not be supported on a single point.

Yeah, so let's figure out which definition is the easiest to work with to show monomorphism. I think you meant to write Sky(I_x) instead of I_x? It should be easy to show the pushforward of a mono is a mono, using the fact that a (pre)sheaf morphism is mono iff it's a mono on every open (this is stated in Stacks for Set-valued (pre)sheaves, but presumably holds more generally (also for functor categories)?).

Sheaf(C, X) morphism is mono iff it’s a mono on every open holds for every concrete category C that preserves pullback, this is in the other PR containing the sky-stalk adjunction. Under this assumption every morphism in C is injective iff it’s mono. This is the maximal generality I could think of

An independent issue: I think the docstring here is problematic, because the skyscraper may have nonzero (non-terminal) stalks at points other than p0, so it may not be supported on a single point.

I thought supported don a single point p meant something like that F(U) is not zero if and only if p \in U. I have removed this phrase to clear confusion

Sheaf(C, X) morphism is mono iff it’s a mono on every open holds for every concrete category C that preserves pullback, this is in the other PR containing the sky-stalk adjunction.

I actually didn't find the exact statement in that PR, but I think you may use category_theory.nat_trans.mono_iff_mono_app combined with category_theory.Sheaf.hom.mono_iff_presheaf_mono that you introduced earlier.

src/topology/sheaves/skyscraper.lean

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

src/topology/sheaves/skyscraper.lean

src/category_theory/limits/shapes/terminal.lean

…verse (#16214) + Generalize universe levels in the sheaf condition `opens_le_cover` on topological spaces and its equivalence with the sheaf condition on sites, allowing three different universe parameters as in `Top.{w}`, `C : Type u` and `category.{v} C`. To be used in #15934. + Generalize universes for the sheaf condition `pairwise_intersection` on topological spaces. This sheaf condition also doesn't require any assumption on the category `C`, and its equivalence with `opens_le_cover` could also have universe levels at maximal generality; however, the proof `is_sheaf_opens_le_cover_iff_is_sheaf_pairwise_intersections` breaks due to the `small_category` restriction on [category_theory.functor.initial.is_limit_whisker_equiv](https://leanprover-community.github.io/mathlib_docs/category_theory/limits/final.html#category_theory.functor.initial.is_limit_whisker_equiv), which will take more work to fix, so we do not generalize the equivalence at this time. + Generalize universes for `Top.presheaf.pushforward`; pullback is not generalized because it would need `has_colimits_of_size`. `Top.sheaf.pushforward` is not yet generalized. + Fixate the universe level of [Top.presheaf](https://leanprover-community.github.io/mathlib_docs/topology/sheaves/presheaf.html#Top.presheaf) to be the same as [Top.sheaf](https://leanprover-community.github.io/mathlib_docs/topology/sheaves/sheaf.html#Top.sheaf).

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

alreadydone

Looks good to me, and I am happy with showing it's a sheaf in another PR.
I already approved this earlier, and I just pinged maintainers on Zulip yesterday; maybe you should instead request review from a maintainer?

riccardobrasca

LGTM.

What do you think about using a namespace? I think it would be nice to have sheaf.skyscraper, or something like that.

bors d+

src/category_theory/eq_to_hom.lean

src/topology/sheaves/skyscraper.lean

bors · 2022-09-26T09:47:47Z

✌️ jjaassoonn can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

jjaassoonn · 2022-09-26T10:09:46Z

LGTM.

What do you think about using a namespace? I think it would be nice to have sheaf.skyscraper, or something like that.

bors d+

I am not entirely sure about the namespace thing, because with a namespace like namespace skyscraper_presheaf, I still think it makes sense to add protected attribute to lemmas/defs, for example
skyscraper_presheaf.cocone_of_specializes after opening skyscraper_presheaf is just cocoon_of_specializes which is kind of confusing. @riccardobrasca

riccardobrasca · 2022-09-26T10:13:15Z

LGTM.
What do you think about using a namespace? I think it would be nice to have sheaf.skyscraper, or something like that.
bors d+

I am not entirely sure about the namespace thing, because with a namespace like namespace skyscraper_presheaf, I still think it makes sense to add protected attribute to lemmas/defs, for example skyscraper_presheaf.cocone_of_specializes after opening skyscraper_presheaf is just cocoon_of_specializes which is kind of confusing. @riccardobrasca

I totally agree, I was thinking more to a sheaf namespace. I really don't know, at some point we will hopefully have a lot of results about sheaves and friends, but I see that currently the category_theory namespace is used, as category_theory.presheaf_to_Sheaf.

jjaassoonn · 2022-09-26T10:26:17Z

LGTM.
What do you think about using a namespace? I think it would be nice to have sheaf.skyscraper, or something like that.
bors d+

I am not entirely sure about the namespace thing, because with a namespace like namespace skyscraper_presheaf, I still think it makes sense to add protected attribute to lemmas/defs, for example skyscraper_presheaf.cocone_of_specializes after opening skyscraper_presheaf is just cocoon_of_specializes which is kind of confusing. @riccardobrasca

I totally agree, I was thinking more to a sheaf namespace. I really don't know, at some point we will hopefully have a lot of results about sheaves and friends, but I see that currently the category_theory namespace is used, as category_theory.presheaf_to_Sheaf.

Put them under category_theory seems a little bit weird to me, there is a Sheaf namespace about grothendieck topologies which this does not apply. Maybe we keep the namespace as the current form and refactor it when proven necessary?

riccardobrasca · 2022-09-26T10:27:51Z

LGTM.
What do you think about using a namespace? I think it would be nice to have sheaf.skyscraper, or something like that.
bors d+

I am not entirely sure about the namespace thing, because with a namespace like namespace skyscraper_presheaf, I still think it makes sense to add protected attribute to lemmas/defs, for example skyscraper_presheaf.cocone_of_specializes after opening skyscraper_presheaf is just cocoon_of_specializes which is kind of confusing. @riccardobrasca

I totally agree, I was thinking more to a sheaf namespace. I really don't know, at some point we will hopefully have a lot of results about sheaves and friends, but I see that currently the category_theory namespace is used, as category_theory.presheaf_to_Sheaf.

Put them under category_theory seems a little bit weird to me, there is a Sheaf namespace about grothendieck topologies which this does not apply. Maybe we keep the namespace as the current form and refactor it when proven necessary?

OK, let's do that.

jjaassoonn · 2022-09-26T13:23:02Z

bors r+

…alculate stalks (#15934)

bors · 2022-09-26T17:06:45Z

Build failed (retrying...):

Build mathlib

…alculate stalks (#15934)

bors · 2022-09-26T21:59:38Z

Pull request successfully merged into master.

Build succeeded:

jjaassoonn added 2 commits August 8, 2022 16:20

initial

64b245e

move file

95a3663

jjaassoonn mentioned this pull request Aug 8, 2022

feat(topology/sheaves/*): sheaves have enough injectives under some condition #15742

Draft

11 tasks

jjaassoonn added this to In progress in Algebraic geometry via automation Aug 8, 2022

jjaassoonn added the t-algebraic-geometry Algebraic geometry label Aug 8, 2022

jjaassoonn added 4 commits August 10, 2022 19:56

need cache

3c964fd

make it better

085be8f

fix linter error

adfff44

fix

fb707bc

alreadydone reviewed Aug 22, 2022

View reviewed changes

src/topology/sheaves/skyscraper.lean Outdated Show resolved Hide resolved

src/topology/sheaves/skyscraper.lean Outdated Show resolved Hide resolved

jjaassoonn and others added 3 commits August 22, 2022 15:09

Apply suggestions from code review

4bea5b8

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

fix

938ddba

fix

15b66e8

alreadydone reviewed Aug 22, 2022

View reviewed changes

jjaassoonn and others added 10 commits August 22, 2022 20:20

Apply suggestions from code review

fb5cded

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

Update src/topology/sheaves/skyscraper.lean

1c10b5d

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

fix

c5efa5a

fix doc

d5156fd

fix

817c29e

missed one

431e3eb

fix

f5425b0

need cache

40242b2

fix

390c7e8

shorter

ee7d74f

alreadydone mentioned this pull request Aug 23, 2022

[Merged by Bors] - feat(topology/sheaves/sheaf_condition/opens_le_cover): generalize universe #16214

Closed

alreadydone reviewed Aug 23, 2022

View reviewed changes

src/topology/sheaves/skyscraper.lean Outdated Show resolved Hide resolved

alreadydone reviewed Aug 23, 2022

View reviewed changes

src/category_theory/limits/shapes/terminal.lean Outdated Show resolved Hide resolved

alreadydone reviewed Aug 23, 2022

View reviewed changes

src/category_theory/limits/shapes/terminal.lean Outdated Show resolved Hide resolved

Update src/topology/sheaves/skyscraper.lean

bbfc190

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Sep 5, 2022

jjaassoonn added 2 commits September 5, 2022 20:41

revert wrong commit first

b4b4c5c

move variables

617c119

jjaassoonn added the awaiting-CI The author would like to see what CI has to say before doing more work. label Sep 6, 2022

github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Sep 6, 2022

jjaassoonn requested a review from alreadydone September 23, 2022 04:18

alreadydone approved these changes Sep 23, 2022

View reviewed changes

jjaassoonn requested a review from riccardobrasca September 26, 2022 06:21

riccardobrasca approved these changes Sep 26, 2022

View reviewed changes

leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Sep 26, 2022

jjaassoonn and others added 2 commits September 26, 2022 11:02

need cache

5b247f3

Apply suggestions from code review

45ca106

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

jjaassoonn added 2 commits September 26, 2022 11:15

fix long line

d2145e6

fix and remove @[reducible]

0eef158

bors bot pushed a commit that referenced this pull request Sep 26, 2022

feat(topology/sheaves/skyscraper): define skyscraper presheaves and c…

31ea95a

…alculate stalks (#15934)

bors bot pushed a commit that referenced this pull request Sep 26, 2022

feat(topology/sheaves/skyscraper): define skyscraper presheaves and c…

f38b4df

…alculate stalks (#15934)

alreadydone mentioned this pull request Sep 26, 2022

[Merged by Bors] - feat(topology/sheaves/skyscraper): skyscraper presheaf is a sheaf #16649

Closed

1 task

bors bot changed the title ~~feat(topology/sheaves/skyscraper): define skyscraper presheaves and calculate stalks~~ [Merged by Bors] - feat(topology/sheaves/skyscraper): define skyscraper presheaves and calculate stalks Sep 26, 2022

bors bot closed this Sep 26, 2022

Algebraic geometry automation moved this from In progress to Done Sep 26, 2022

bors bot deleted the jjaassoonn/sky_def branch September 26, 2022 21:59

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(topology/sheaves/skyscraper): define skyscraper presheaves and calculate stalks #15934

[Merged by Bors] - feat(topology/sheaves/skyscraper): define skyscraper presheaves and calculate stalks #15934

jjaassoonn commented Aug 8, 2022

alreadydone left a comment

alreadydone Aug 22, 2022

jjaassoonn Aug 22, 2022

jjaassoonn Aug 22, 2022

alreadydone Aug 22, 2022

alreadydone Aug 23, 2022

jjaassoonn Aug 30, 2022 •

edited

alreadydone Aug 30, 2022

jjaassoonn Aug 30, 2022 •

edited

jjaassoonn Aug 30, 2022

alreadydone Sep 2, 2022

alreadydone left a comment

riccardobrasca left a comment

bors bot commented Sep 26, 2022

jjaassoonn commented Sep 26, 2022 •

edited

riccardobrasca commented Sep 26, 2022

jjaassoonn commented Sep 26, 2022

riccardobrasca commented Sep 26, 2022

jjaassoonn commented Sep 26, 2022

bors bot commented Sep 26, 2022

bors bot commented Sep 26, 2022

[Merged by Bors] - feat(topology/sheaves/skyscraper): define skyscraper presheaves and calculate stalks #15934

[Merged by Bors] - feat(topology/sheaves/skyscraper): define skyscraper presheaves and calculate stalks #15934

Conversation

jjaassoonn commented Aug 8, 2022

alreadydone left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jjaassoonn Aug 30, 2022 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jjaassoonn Aug 30, 2022 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

alreadydone left a comment

Choose a reason for hiding this comment

riccardobrasca left a comment

Choose a reason for hiding this comment

bors bot commented Sep 26, 2022

jjaassoonn commented Sep 26, 2022 • edited

riccardobrasca commented Sep 26, 2022

jjaassoonn commented Sep 26, 2022

riccardobrasca commented Sep 26, 2022

jjaassoonn commented Sep 26, 2022

bors bot commented Sep 26, 2022

bors bot commented Sep 26, 2022

jjaassoonn Aug 30, 2022 •

edited

jjaassoonn Aug 30, 2022 •

edited

jjaassoonn commented Sep 26, 2022 •

edited