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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): fromSpec and toSpec compose to identity #9618

Closed
wants to merge 29 commits into from
Closed

[Merged by Bors] - feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): fromSpec and toSpec compose to identity #9618

wants to merge 29 commits into from

Conversation

jjaassoonn
Copy link
Collaborator

@jjaassoonn jjaassoonn commented Jan 10, 2024 •
edited by Parcly-Taxel

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Jan 10, 2024
@jjaassoonn jjaassoonn mentioned this pull request Jan 10, 2024
Closed
1 task
@erdOne
Copy link
Member

erdOne commented Jan 10, 2024

The proofs seem to be quite long. Is it possible to extract useful lemmas?

@jjaassoonn
Copy link
Collaborator Author

The proofs seem to be quite long. Is it possible to extract useful lemmas?

The length is mainly due to writing an element in some span as a sum of fractions and clear denominators. I will think about if any of these can be extracted out.

@jjaassoonn
Copy link
Collaborator Author

The proofs seem to be quite long. Is it possible to extract useful lemmas?

I golfed one lemma ToSpec.carrier_eq_span in #9601. Now #9601 is < 100 lines long which I think is an okay length. Could you please take a look at #9601?

@jjaassoonn jjaassoonn added the t-algebraic-geometry Algebraic geometry label Jan 14, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Feb 27, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

riccardobrasca
riccardobrasca approved these changes Mar 1, 2024
View reviewed changes
Copy link
Member

@riccardobrasca riccardobrasca left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

bors d+

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean Outdated Show resolved Hide resolved
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean Outdated Show resolved Hide resolved
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean Show resolved Hide resolved
@mathlib-bors
Copy link

mathlib-bors bot commented Mar 1, 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.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added delegated and removed awaiting-review The author would like community review of the PR labels Mar 1, 2024
@jjaassoonn @riccardobrasca
Apply suggestions from code review
085ebb5 
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
@jjaassoonn jjaassoonn added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Mar 1, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Mar 1, 2024
@jjaassoonn @Parcly-Taxel
feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): fromSpec and `to…
9907f0b 
…Spec` compose to identity (#9618)

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Mar 1, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Mar 1, 2024
@jjaassoonn @Parcly-Taxel
feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): fromSpec and `to…
c26b7f1 
…Spec` compose to identity (#9618)

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Mar 1, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): fromSpec and toSpec compose to identity [Merged by Bors] - feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): fromSpec and toSpec compose to identity Mar 1, 2024
@mathlib-bors mathlib-bors bot closed this Mar 1, 2024
@mathlib-bors mathlib-bors bot deleted the projConstruction/fromSpecToSpec branch March 1, 2024 17:47
@Ruben-VandeVelde Ruben-VandeVelde mentioned this pull request Mar 2, 2024
Closed
kbuzzard pushed a commit that referenced this pull request Mar 12, 2024
@jjaassoonn @Parcly-Taxel @kbuzzard
feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): fromSpec and `to…
aec44eb 
…Spec` compose to identity (#9618)

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@jjaassoonn @Parcly-Taxel @dagurtomas
feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): fromSpec and `to…
0aaf55a 
…Spec` compose to identity (#9618)

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
mathlib-bors bot pushed a commit that referenced this pull request Mar 24, 2024
@Ruben-VandeVelde
chore: add missing aliases for recently renamed lemmas (#11117)
f29c550 
From #9618, #10525 and #10614.
Louddy pushed a commit that referenced this pull request Mar 25, 2024
@Ruben-VandeVelde @Louddy
chore: add missing aliases for recently renamed lemmas (#11117)
bdcece4 
From #9618, #10525 and #10614.
utensil pushed a commit that referenced this pull request Mar 26, 2024
@jjaassoonn @Parcly-Taxel @utensil
feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): fromSpec and `to…
1da7636 
…Spec` compose to identity (#9618)

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
utensil pushed a commit that referenced this pull request Mar 26, 2024
@Ruben-VandeVelde @utensil
chore: add missing aliases for recently renamed lemmas (#11117)
8aa269e 
From #9618, #10525 and #10614.
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@jjaassoonn @Parcly-Taxel @Louddy
feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): fromSpec and `to…
d64bc7b 
…Spec` compose to identity (#9618)

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@Ruben-VandeVelde @Louddy
chore: add missing aliases for recently renamed lemmas (#11117)
0ffb1f2 
From #9618, #10525 and #10614.
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
@Ruben-VandeVelde @atarnoam
chore: add missing aliases for recently renamed lemmas (#11117)
6365344 
From #9618, #10525 and #10614.
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@Ruben-VandeVelde @uniwuni
chore: add missing aliases for recently renamed lemmas (#11117)
5ef344b 
From #9618, #10525 and #10614.
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@Ruben-VandeVelde @callesonne
chore: add missing aliases for recently renamed lemmas (#11117)
05a9d6a 
From #9618, #10525 and #10614.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@erdOne erdOne erdOne left review comments

@riccardobrasca riccardobrasca riccardobrasca approved these changes

Assignees

@riccardobrasca riccardobrasca

Labels
auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. delegated t-algebraic-geometry Algebraic geometry
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@jjaassoonn @erdOne @leanprover-community-mathlib4-bot @riccardobrasca @Parcly-Taxel