mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(algebraic_geometry/projective_spectrum/Scheme): the function from Spec to Proj restricted to basic open set.

Open jjaassoonn opened this issue 3 years ago • 2 comments

We want to have a homeomorphism between $\mathrm{Proj}|_{D(f)}$ to $\mathrm{Spec}{A^0_f}$, we have the forward direction already. This PR is the underlying function of backward direction. Continuity will be proved separately.

  • [x] depends on: #15261 missing lemma about sum of fraction is fraction of sum (with common denominator)
  • [x] depends on: #15264

Open in Gitpod

jjaassoonn avatar Jul 11 '22 20:07 jjaassoonn

If needed, I will split this PR further

jjaassoonn avatar Aug 15 '22 01:08 jjaassoonn

Sorry, the last comment (deleted) is meant for the other PR.

alreadydone avatar Aug 17 '22 07:08 alreadydone

With these golfs, I think it's good to go once #16083 is merged. Thanks!

Thank you so much for taking the time to golf all these long and poorly formatted proofs!

jjaassoonn avatar Aug 18 '22 14:08 jjaassoonn

No problem; it's fun to think about these proofs!

alreadydone avatar Aug 18 '22 14:08 alreadydone

This PR/issue depends on:

  • ~~leanprover-community/mathlib#15261~~
  • ~~leanprover-community/mathlib#15264~~
  • ~~leanprover-community/mathlib#16083~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Sep 21 '22 10:09 mathlib-dependent-issues-bot

Thanks :tada:

bors merge

jcommelin avatar Sep 26 '22 07:09 jcommelin

Build failed (retrying...):

bors[bot] avatar Sep 26 '22 09:09 bors[bot]

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Sep 26 '22 10:09 bors[bot]