[Merged by Bors] - feat(algebraic_geometry/*): Proved Spec ⋙ Γ ≅ 𝟭 #9416

erdOne · 2021-09-27T16:51:11Z

Specialied algebraic_geometry.structure_sheaf.basic_open_iso into global sections, proving that the map structure_sheaf.to_open R ⊤ is an isomorphism in algebraic_geometry.is_iso_to_global.
Proved that the map R ⟶ Γ(Spec R) is natural, and presents the fact above as an natural isomorphism Spec.right_op ⋙ Γ ≅ 𝟭 _ in algebraic_geometry.Spec_Γ_identity.

depends on: [Merged by Bors] - chore(algebra/category/*): Added of_hom to all of the algebraic categories. #9454

tb65536 · 2021-09-28T05:18:52Z

Could you add a description to the PR, explaining in words what the result is?

src/algebraic_geometry/Spec.lean

src/algebraic_geometry/structure_sheaf.lean

src/algebraic_geometry/Spec.lean

src/algebraic_geometry/structure_sheaf.lean

Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

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

into global_sections_of_structure_sheaf

src/algebraic_geometry/structure_sheaf.lean

justus-springer · 2021-09-28T10:01:33Z

Thanks, looks good to me now.

src/algebraic_geometry/Spec.lean

src/algebraic_geometry/structure_sheaf.lean

src/algebraic_geometry/Spec.lean

src/algebraic_geometry/structure_sheaf.lean

Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

…egories. (#9454) As suggested in the comments of #9416.

into global_sections_of_structure_sheaf

github-actions · 2021-10-01T06:13:12Z

🎉 Great news! Looks like all the dependencies have been resolved:

~~[Merged by Bors] - chore(algebra/category/*): Added of_hom to all of the algebraic categories. #9454~~

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

src/algebra/category/CommRing/basic.lean

semorrison · 2021-10-01T06:21:36Z

Could you add a line or two to the module-doc at the top, summarising progress on this adjunction?

(Even just the text from the PR top comment would be great.)

src/algebraic_geometry/structure_sheaf.lean

src/algebra/category/CommRing/basic.lean

jcommelin · 2021-10-01T07:32:35Z

bors d+

bors · 2021-10-01T07:32:36Z

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

erdOne · 2021-10-01T07:33:49Z

bors r+

jcommelin · 2021-10-01T08:34:56Z

bors r-

bors d+

@erdOne, please merge this after CI gives you a green checkmark. Also, please remove awaiting-CI before you merge, otherwise bors will be unhappy.

bors · 2021-10-01T08:34:57Z

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

bors · 2021-10-01T08:34:58Z

Canceled.

erdOne · 2021-10-01T09:36:36Z

bors r+

- Specialied `algebraic_geometry.structure_sheaf.basic_open_iso` into global sections, proving that the map `structure_sheaf.to_open R ⊤` is an isomorphism in `algebraic_geometry.is_iso_to_global`. - Proved that the map `R ⟶ Γ(Spec R)` is natural, and presents the fact above as an natural isomorphism `Spec.right_op ⋙ Γ ≅ 𝟭 _` in `algebraic_geometry.Spec_Γ_identity`. Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>

bors · 2021-10-01T10:33:31Z

Build failed (retrying...):

Build mathlib

- Specialied `algebraic_geometry.structure_sheaf.basic_open_iso` into global sections, proving that the map `structure_sheaf.to_open R ⊤` is an isomorphism in `algebraic_geometry.is_iso_to_global`. - Proved that the map `R ⟶ Γ(Spec R)` is natural, and presents the fact above as an natural isomorphism `Spec.right_op ⋙ Γ ≅ 𝟭 _` in `algebraic_geometry.Spec_Γ_identity`. Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>

bors · 2021-10-01T10:38:42Z

Build failed (retrying...):

Build mathlib

- Specialied `algebraic_geometry.structure_sheaf.basic_open_iso` into global sections, proving that the map `structure_sheaf.to_open R ⊤` is an isomorphism in `algebraic_geometry.is_iso_to_global`. - Proved that the map `R ⟶ Γ(Spec R)` is natural, and presents the fact above as an natural isomorphism `Spec.right_op ⋙ Γ ≅ 𝟭 _` in `algebraic_geometry.Spec_Γ_identity`. Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>

bors · 2021-10-01T13:24:01Z

Pull request successfully merged into master.

Build succeeded:

proved Spec ⋙ Γ ≅ 𝟭

df060ad

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

justus-springer self-requested a review September 27, 2021 19:40

tb65536 reviewed Sep 28, 2021

View reviewed changes

jcommelin reviewed Sep 28, 2021

View reviewed changes

src/algebraic_geometry/Spec.lean Outdated Show resolved Hide resolved

src/algebraic_geometry/Spec.lean Outdated Show resolved Hide resolved

src/algebraic_geometry/Spec.lean Outdated Show resolved Hide resolved

src/algebraic_geometry/structure_sheaf.lean Outdated Show resolved Hide resolved

erdOne and others added 5 commits September 28, 2021 14:19

Update src/algebraic_geometry/Spec.lean

7228654

Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

Update Spec.lean

a20d7b1

Update src/algebraic_geometry/structure_sheaf.lean

6b38826

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

Update Spec.lean

93b38e9

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

84376b1

into global_sections_of_structure_sheaf

justus-springer reviewed Sep 28, 2021

View reviewed changes

src/algebraic_geometry/structure_sheaf.lean Outdated Show resolved Hide resolved

src/algebraic_geometry/structure_sheaf.lean Outdated Show resolved Hide resolved

Updated Spec.lean and structure_sheaf.lean

05270c7

justus-springer reviewed Sep 28, 2021

View reviewed changes

src/algebraic_geometry/structure_sheaf.lean Outdated Show resolved Hide resolved

Cleaned stuff up

9830ae4

tb65536 reviewed Sep 28, 2021

View reviewed changes

adamtopaz reviewed Sep 28, 2021

View reviewed changes

src/algebraic_geometry/structure_sheaf.lean Outdated Show resolved Hide resolved

erdOne and others added 5 commits September 29, 2021 01:04

Update src/algebraic_geometry/Spec.lean

3f27e33

Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

Update src/algebraic_geometry/Spec.lean

ffeebb9

Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

Update src/algebraic_geometry/structure_sheaf.lean

7477793

Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

Update src/algebraic_geometry/Spec.lean

c647500

Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

fixed stuff

64a0c66

erdOne mentioned this pull request Sep 29, 2021

[Merged by Bors] - chore(algebra/category/*): Added of_hom to all of the algebraic categories. #9454

Closed

github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Sep 29, 2021

bors bot pushed a commit that referenced this pull request Oct 1, 2021

chore(algebra/category/*): Added of_hom to all of the algebraic cat…

fbf7545

…egories. (#9454) As suggested in the comments of #9416.

bors bot pushed a commit that referenced this pull request Oct 1, 2021

chore(algebra/category/*): Added of_hom to all of the algebraic cat…

481c35d

…egories. (#9454) As suggested in the comments of #9416.

bors bot pushed a commit that referenced this pull request Oct 1, 2021

chore(algebra/category/*): Added of_hom to all of the algebraic cat…

b786443

…egories. (#9454) As suggested in the comments of #9416.

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 1, 2021

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

d4b3c9e

into global_sections_of_structure_sheaf

github-actions bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Oct 1, 2021

semorrison reviewed Oct 1, 2021

View reviewed changes

src/algebra/category/CommRing/basic.lean Outdated Show resolved Hide resolved

semorrison reviewed Oct 1, 2021

View reviewed changes

src/algebra/category/CommRing/basic.lean Outdated Show resolved Hide resolved

fixed stuff

c567426

semorrison reviewed Oct 1, 2021

View reviewed changes

src/algebraic_geometry/structure_sheaf.lean Show resolved Hide resolved

added some docs about current progress

1e38a75

jcommelin reviewed Oct 1, 2021

View reviewed changes

src/algebra/category/CommRing/basic.lean Outdated Show resolved Hide resolved

jcommelin added awaiting-CI The author would like to see what CI has to say before doing more work. ready-for-bors labels Oct 1, 2021

github-actions bot 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 Oct 1, 2021

erdOne removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Oct 1, 2021

bors bot changed the title ~~feat(algebraic_geometry/*): Proved Spec ⋙ Γ ≅ 𝟭~~ [Merged by Bors] - feat(algebraic_geometry/*): Proved Spec ⋙ Γ ≅ 𝟭 Oct 1, 2021

bors bot closed this Oct 1, 2021

bors bot deleted the global_sections_of_structure_sheaf branch October 1, 2021 13:24

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(algebraic_geometry/*): Proved Spec ⋙ Γ ≅ 𝟭 #9416

[Merged by Bors] - feat(algebraic_geometry/*): Proved Spec ⋙ Γ ≅ 𝟭 #9416

erdOne commented Sep 27, 2021 •

edited

tb65536 commented Sep 28, 2021

justus-springer commented Sep 28, 2021

github-actions bot commented Oct 1, 2021

semorrison commented Oct 1, 2021 •

edited

jcommelin commented Oct 1, 2021

bors bot commented Oct 1, 2021

erdOne commented Oct 1, 2021

jcommelin commented Oct 1, 2021

bors bot commented Oct 1, 2021

bors bot commented Oct 1, 2021

erdOne commented Oct 1, 2021

bors bot commented Oct 1, 2021

bors bot commented Oct 1, 2021

bors bot commented Oct 1, 2021

[Merged by Bors] - feat(algebraic_geometry/*): Proved Spec ⋙ Γ ≅ 𝟭 #9416

[Merged by Bors] - feat(algebraic_geometry/*): Proved Spec ⋙ Γ ≅ 𝟭 #9416

Conversation

erdOne commented Sep 27, 2021 • edited

tb65536 commented Sep 28, 2021

justus-springer commented Sep 28, 2021

github-actions bot commented Oct 1, 2021

semorrison commented Oct 1, 2021 • edited

jcommelin commented Oct 1, 2021

bors bot commented Oct 1, 2021

erdOne commented Oct 1, 2021

jcommelin commented Oct 1, 2021

bors bot commented Oct 1, 2021

bors bot commented Oct 1, 2021

erdOne commented Oct 1, 2021

bors bot commented Oct 1, 2021

bors bot commented Oct 1, 2021

bors bot commented Oct 1, 2021

erdOne commented Sep 27, 2021 •

edited

semorrison commented Oct 1, 2021 •

edited