(WIP) feat(AlgebraicGeometry): define Projective Space #26061
Conversation
PR summary 7e091d1f76Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 768 | 7 | erw |
| 3 | 1 | maxHeartBeats modifications |
Current commit 4772397bdb
Reference commit 7e091d1f76
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
|
||
| /- | ||
| TODO: | ||
| - `AlgebraicGeometry.ProjectiveSpace.SpecIso`: `ℙ(n; Spec R) ≅ Proj R[n]` |
There was a problem hiding this comment.
I would like to see some basic API in this PR for sanity check, in particular this thing should probably be in this PR.
There was a problem hiding this comment.
This is a bit hard at the moment, it's the main result in my personal branch and it takes 1000 lines. There's basically a lot of explicit maps between polynomial rings that are missing from the library, as the construction is by defining open covers on both sides, and using also isomorphisms on the intersections (i.e. pullbacks).
Does my personal branch work as the sanity check?
There was a problem hiding this comment.
Is this really the proof you want? I would have assumed that this should follow once you obtain the functor of points for Proj Z[n] (whose proof hopefully generalizes to Proj R[n] immediately)? Although that is indeed a lot of work.
There was a problem hiding this comment.
Or actually shouldn't you show that Proj is compatible with base change (so you should not need to talk about maps between polynomial rings)?
There was a problem hiding this comment.
These two alternative approaches are both out of scope for this PR which is to just get the basic definition in. Generalisations or not, I think we still ultimately want P(n; S) to exist.
Co-authored-by: Andrew Yang <[email protected]>
|
|
||
| /-- `ℙ(n; S)` is the projective `n`-space over a scheme `S`. | ||
| Note that `n` is an arbitrary index type (e.g. `ULift (Fin m)`). -/ | ||
| def ProjectiveSpace (n : Type u) (S : Scheme.{u}) : Scheme.{u} := |
There was a problem hiding this comment.
| def ProjectiveSpace (n : Type u) (S : Scheme.{u}) : Scheme.{u} := | |
| def ProjectiveSpace : Scheme.{u} := |
You already have these as variables right? Or is this done for readability? Because you have not written them down in the other definitions.
There was a problem hiding this comment.
It is for readability for the public-facing / main definitions
| def ProjectiveSpace (n : Type u) (S : Scheme.{u}) : Scheme.{u} := | ||
| pullback (terminal.from S) (terminal.from (Proj ℤ[n].{u})) | ||
|
|
||
| @[inherit_doc] scoped notation "ℙ("n"; "S")" => ProjectiveSpace n S |
There was a problem hiding this comment.
I would also introduce notation "ℙ("n")" for the case S = \mathbb{Z} (or rather for Proj ℤ[n].{u}).
There was a problem hiding this comment.
I think similar to the case for AffineSpace, these details are not meant to be public-facing.
Co-authored-by: Calle Sönne <[email protected]>
kckennylau
changed the title
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
4 participants
This defines the projective space over a scheme, indexed by an arbitrary type.
Zulip discussion: #maths > Projective Space
I am currently using this PR as a hub for future PR's that will be split from this PR, so it is currently WIP.