[Merged by Bors] - refactor(AlgebraicGeometry): Introduce Scheme.toSpecΓ

[erdOne]

---

[github-actions]

PR summary eb1d5a5430

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Scheme.toSpecΓ_app_top
+ Scheme.toSpecΓ_naturality
+ Scheme.toSpecΓ_preimage_basicOpen
+ _root_.AlgebraicGeometry.Scheme.toSpecΓ
+ instance (X : Scheme.{u}) [IsAffine X] : IsIso (ΓSpec.adjunction.unit.app X) := @IsAffine.affine X _
+ toOpen_toSpecΓ_app
+ ΓSpec.adjunction_unit_app_app_top
+ ΓSpec.adjunction_unit_map_basicOpen
+ ΓSpec.adjunction_unit_naturality
+ ΓSpec.adjunction_unit_naturality_assoc
- adjunction_unit_app_app_top
- adjunction_unit_map_basicOpen
- adjunction_unit_naturality
- toOpen_unit_app_val_c_app
- toOpen_unit_app_val_c_app'

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[erdOne]

!bench

[leanprover-bot]

Here are the benchmark results for commit d568375.
The entire run failed.
Found no significant differences.

[erdOne]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6c86c0b.
There were no significant changes against commit 4261f99.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Build failed:

• Build

[jcommelin]

Let's try again

bors r+

[mathlib-bors]

Build failed:

• Lint style

[sgouezel]

bors r+

[mathlib-bors]

This PR was included in a batch that was canceled, it will be automatically retried

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

This PR was included in a batch that was canceled, it will be automatically retried

[mathlib-bors]

Build failed (retrying...):

• Build

[urkud]

The build error looks like category theory, removing from the queue for now.
bors r-
bors d+

[mathlib-bors]

✌️ 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.

[mathlib-bors]

Canceled.

[erdOne]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style