Skip to content
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(AlgebraicGeometry/ProjectiveSpectrum/Scheme): calculate stalk of toSpec map #13896

Closed
wants to merge 2 commits into from

Conversation

jjaassoonn
Copy link
Collaborator

@jjaassoonn jjaassoonn commented Jun 17, 2024

In this PR, we show the newly defined map of locally ringed spacetoSpec agree with the ProjIsoSpecTopComponent.toSpec and calculate the stalk map.

Co-authored-by: Andrew Yang [email protected]


Open in Gitpod

Copy link

github-actions bot commented Jun 17, 2024

PR summary c84f58d6d6

Import changes

No significant changes to the import graph


Declarations diff

+ mk_mem_toSpec_base_apply
+ toOpen_toSpec_val_c_app
+ toSpec_base_apply_eq
+ toSpec_base_apply_eq_comap
+ toSpec_preimage_basicOpen
+ toStalk_stalkMap_toSpec

You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

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

@erdOne
Copy link
Member

erdOne commented Jun 17, 2024

Thanks!
LGTM but I did a significant portion of these so I'll wait for someone else to review.

@joelriou
Copy link
Collaborator

Thanks!

bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 18, 2024

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

@jjaassoonn
Copy link
Collaborator Author

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jun 18, 2024
… `toSpec` map (#13896)

In this PR, we show the newly defined map of locally ringed space`toSpec` agree with the `ProjIsoSpecTopComponent.toSpec` and calculate the stalk map.

Co-authored-by: Andrew Yang <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 18, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Jun 18, 2024
… `toSpec` map (#13896)

In this PR, we show the newly defined map of locally ringed space`toSpec` agree with the `ProjIsoSpecTopComponent.toSpec` and calculate the stalk map.

Co-authored-by: Andrew Yang <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 18, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): calculate stalk of toSpec map [Merged by Bors] - feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): calculate stalk of toSpec map Jun 18, 2024
@mathlib-bors mathlib-bors bot closed this Jun 18, 2024
@mathlib-bors mathlib-bors bot deleted the zjj/proj/toSpec_apply branch June 18, 2024 14:41
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
… `toSpec` map (#13896)

In this PR, we show the newly defined map of locally ringed space`toSpec` agree with the `ProjIsoSpecTopComponent.toSpec` and calculate the stalk map.

Co-authored-by: Andrew Yang <[email protected]>
grunweg pushed a commit that referenced this pull request Jun 20, 2024
… `toSpec` map (#13896)

In this PR, we show the newly defined map of locally ringed space`toSpec` agree with the `ProjIsoSpecTopComponent.toSpec` and calculate the stalk map.

Co-authored-by: Andrew Yang <[email protected]>
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
… `toSpec` map (#13896)

In this PR, we show the newly defined map of locally ringed space`toSpec` agree with the `ProjIsoSpecTopComponent.toSpec` and calculate the stalk map.

Co-authored-by: Andrew Yang <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants