mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(algebraic_geometry/prime_spectrum/basic): intersection of localisations

Open Multramate opened this issue 3 years ago • 5 comments

  • [x] depends on: #16905 [define maximal spectrum]
  • [x] depends on: #16920 [refactor height one spectrum]

Open in Gitpod

Multramate avatar Oct 08 '22 03:10 Multramate

If you add the maximal spectrum, I think it needs to come with a lot of API about its relation to the prime spectrum: at a minimum the inclusion map. Maybe also the characterisation of the image as the subset of closed points.

At a later stage, maybe the Zariski topology on the maximal spectrum should be added, and then of course the continuity of the inclusion map.

Yes, I plan to make a basic API right after this, but on a separate PR so as to not cloud this one - is that fine? I also plan to refactor them into a separate file in the same folder called maximal_spectrum.

Multramate avatar Oct 11 '22 00:10 Multramate

Is the content of this PR urgent? If not, then I would prefer that you swap the order of those two PRs.

jcommelin avatar Oct 11 '22 00:10 jcommelin

Is the content of this PR urgent? If not, then I would prefer that you swap the order of those two PRs.

I made a basic PR for the maximal spectrum, but I'm not sure if the Zariski topology definition is ideal here.

Multramate avatar Oct 11 '22 07:10 Multramate

To make this PR depend on the other PR, please edit the top post. It will contain instructions on how to add dependencies. While you are at it, the commit message in the top post is no longer accurate.

jcommelin avatar Oct 12 '22 06:10 jcommelin

This PR/issue depends on:

  • ~~leanprover-community/mathlib#16905~~
  • ~~leanprover-community/mathlib#16920~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Oct 13 '22 15:10 mathlib-dependent-issues-bot

Thanks! maintainer merge

erdOne avatar Oct 17 '22 08:10 erdOne

🚀 Pull request has been placed on the maintainer queue by erdOne.

github-actions[bot] avatar Oct 17 '22 08:10 github-actions[bot]

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Oct 17 '22 13:10 bors[bot]