[Merged by Bors] - feat(category_theory/sites/*): Cover-lifting functors on sites #9431

erdOne · 2021-09-28T11:42:43Z

This PR defines cover-liftings functors between sites, and proves that Ran F.op maps sheaves to sheaves for cover-lifting functors F.
This will probably be needed when we want to glue B-sheaves into sheaves.

By the way, is there a better name for Ran_is_sheaf? It sounds quite odd now.

into b-sheaves

into cocontinuous_functor_on_sites

…or_on_sites

src/category_theory/sites/cocontinuous.lean

justus-springer · 2021-09-28T17:56:08Z

src/category_theory/structured_arrow.lean

+Given a structured arrow `X ⟶ F(U)`, and an arrow `U ⟶ Y`, we can construct a morphism of
+structured arrow given by `(X ⟶ F(U)) ⟶ (X ⟶ F(U) ⟶ F(Y))`.
+-/
+def hom_mk' {F : C ⥤ D} {X : D} {Y : C}


Do we really need this definition? I think it looks a little out of place on its own...

I tried not to, but I couldn't find a better way to construct those kind of morphisms without using have everywhere.

src/category_theory/sites/cocontinuous.lean

Co-authored-by: Johan Commelin <johan@commelin.net>

b-mehta

Some comments from a brief read, I'll take a closer look once these (and Johan's) comments have been addressed.

src/category_theory/sites/cocontinuous.lean

src/category_theory/sites/sieves.lean

src/category_theory/sites/sheaf_of_types.lean

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

into cocontinuous_functor_on_sites

…anprover-community/mathlib into cocontinuous_functor_on_sites

into cocontinuous_functor_on_sites

src/category_theory/sites/sieves.lean

src/category_theory/sites/cover_lifting.lean

Co-authored-by: Johan Commelin <johan@commelin.net>

jcommelin · 2021-10-02T15:05:05Z

This is starting to look good. I have one question: how responsive is the file? You prove some things using tidy and simp. Are these snappy? If not, please replace tidy with the output of tidy? and simp with the output of squeeze_simp.

erdOne · 2021-10-02T15:32:19Z

It is indeed not that responsive, but replacing the simps to sorrys doesn't seem to change the running time at all, so I assume that the bottleneck is not at the simps.

Co-authored-by: Johan Commelin <johan@commelin.net>

src/category_theory/sites/sieves.lean

src/category_theory/sites/sheaf_of_types.lean

Co-authored-by: Justus Springer <50165510+justus-springer@users.noreply.github.com>

jcommelin

Thanks 🎉

bors merge

This PR defines cover-liftings functors between sites, and proves that `Ran F.op` maps sheaves to sheaves for cover-lifting functors `F`. This will probably be needed when we want to glue B-sheaves into sheaves. Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>

bors · 2021-10-04T09:48:04Z

Pull request successfully merged into master.

Build succeeded:

alreadydone · 2021-11-13T03:05:18Z

It would be an interesting project to define the structure sheaf on Spec using this PR. Endow the ring with a category structure and a Grothendieck topology, so that basic_open is a cover-lifting functor to opens (prime_spectrum R). This could avoid Reid Barton's trick to avoid axiom of choice in the first definitions in Schemes in Lean (no need to identify R[1/f] with R[1/g] when D(f)=D(g)), and the construction would end up similar to the second definition: without the implicit sheafification in Hartshorne's construction, we would need the generalized 00EJ (4.4 in paper) to prove the R[1/f] presheaf on the "ring site" is a sheaf, then transfer it to the structure sheaf using this PR.

However, this approach seems not applicable for the localization functor (see p.7), so I'm not in favor of it.

erdOne added 10 commits September 24, 2021 15:28

first commit

0ef5391

proved stacks#00XK

b539b7c

Merge branch 'master' of https://github.com/leanprover-community/mathlib

fbbe8ad

into b-sheaves

refactored stuff

9340249

refactored stuff

0297771

refactored proof

8247121

moved things to where they should be

7c7d9c9

Merge branch 'master' of https://github.com/leanprover-community/mathlib

7a6755e

into cocontinuous_functor_on_sites

added docs and stuff

ab6e03b

Merge branch 'cocontinuous_functors_on_sites' into cocontinuous_funct…

393ae1b

…or_on_sites

erdOne added the awaiting-review The author would like community review of the PR label Sep 28, 2021

justus-springer reviewed Sep 28, 2021

View reviewed changes

cleaned up proofs and added more comments

3f6e08b

erdOne changed the title ~~feat(category_theory/sites/*): Cocontinuous functor on sites~~ feat(category_theory/sites/*): Cocontinuous functors on sites Sep 29, 2021

jcommelin requested review from b-mehta and adamtopaz September 30, 2021 06:27

jcommelin reviewed Sep 30, 2021

View reviewed changes

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 30, 2021

erdOne and others added 5 commits September 30, 2021 14:36

Update src/category_theory/sites/cocontinuous.lean

32d8620

Co-authored-by: Johan Commelin <johan@commelin.net>

Update src/category_theory/sites/cocontinuous.lean

1e65a9a

Co-authored-by: Johan Commelin <johan@commelin.net>

Update src/category_theory/sites/cocontinuous.lean

d0016b9

Co-authored-by: Johan Commelin <johan@commelin.net>

Update cocontinuous.lean

6ee44da

Update cocontinuous.lean

ad2e5b9

b-mehta reviewed Oct 1, 2021

View reviewed changes

erdOne and others added 5 commits October 1, 2021 10:23

Update src/category_theory/sites/cocontinuous.lean

7fd6f27

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

Update src/category_theory/sites/cocontinuous.lean

13f0649

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

Update src/category_theory/sites/cocontinuous.lean

e3e3b4c

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

Update src/category_theory/sites/sieves.lean

8d5ccc9

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

Merge branch 'master' of https://github.com/leanprover-community/mathlib

f5e6a97

into cocontinuous_functor_on_sites

erdOne added 2 commits October 1, 2021 22:10

Merge branch 'cocontinuous_functor_on_sites' of https://github.com/le…

5aa5a17

…anprover-community/mathlib into cocontinuous_functor_on_sites

Merge branch 'master' of https://github.com/leanprover-community/mathlib

26f8ab3

into cocontinuous_functor_on_sites

jcommelin reviewed Oct 2, 2021

View reviewed changes

src/category_theory/sites/sieves.lean Outdated Show resolved Hide resolved

src/category_theory/sites/cover_lifting.lean Outdated Show resolved Hide resolved

Update src/category_theory/sites/sieves.lean

e458abd

Co-authored-by: Johan Commelin <johan@commelin.net>

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 2, 2021

erdOne and others added 2 commits October 2, 2021 23:32

Update src/category_theory/sites/cover_lifting.lean

7683bdf

Co-authored-by: Johan Commelin <johan@commelin.net>

unfolded tidys and simps; fixed docs

c9191f5

erdOne added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 2, 2021

justus-springer reviewed Oct 3, 2021

View reviewed changes

src/category_theory/sites/sieves.lean Outdated Show resolved Hide resolved

justus-springer reviewed Oct 3, 2021

View reviewed changes

erdOne and others added 7 commits October 3, 2021 21:34

Update src/category_theory/sites/sheaf_of_types.lean

57be0d8

Co-authored-by: Justus Springer <50165510+justus-springer@users.noreply.github.com>

Update src/category_theory/sites/sheaf_of_types.lean

5fb9052

Co-authored-by: Justus Springer <50165510+justus-springer@users.noreply.github.com>

Update src/category_theory/sites/sieves.lean

883daf6

Co-authored-by: Justus Springer <50165510+justus-springer@users.noreply.github.com>

fixed stuff

166ce6d

fixed stuff

f19ca1c

added some simp lemmas

6a9be44

moved variables

f20de68

jcommelin approved these changes Oct 4, 2021

View reviewed changes

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Oct 4, 2021

bors bot changed the title ~~feat(category_theory/sites/*): Cover-lifting functors on sites~~ [Merged by Bors] - feat(category_theory/sites/*): Cover-lifting functors on sites Oct 4, 2021

bors bot closed this Oct 4, 2021

bors bot deleted the cocontinuous_functor_on_sites branch October 4, 2021 09:48

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(category_theory/sites/*): Cover-lifting functors on sites #9431

[Merged by Bors] - feat(category_theory/sites/*): Cover-lifting functors on sites #9431

erdOne commented Sep 28, 2021 •

edited

justus-springer Sep 28, 2021

erdOne Sep 28, 2021

b-mehta left a comment

jcommelin commented Oct 2, 2021

erdOne commented Oct 2, 2021

jcommelin left a comment

bors bot commented Oct 4, 2021

alreadydone commented Nov 13, 2021 •

edited

[Merged by Bors] - feat(category_theory/sites/*): Cover-lifting functors on sites #9431

[Merged by Bors] - feat(category_theory/sites/*): Cover-lifting functors on sites #9431

Conversation

erdOne commented Sep 28, 2021 • edited

justus-springer Sep 28, 2021

Choose a reason for hiding this comment

erdOne Sep 28, 2021

Choose a reason for hiding this comment

b-mehta left a comment

Choose a reason for hiding this comment

jcommelin commented Oct 2, 2021

erdOne commented Oct 2, 2021

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Oct 4, 2021

alreadydone commented Nov 13, 2021 • edited

erdOne commented Sep 28, 2021 •

edited

alreadydone commented Nov 13, 2021 •

edited